Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Sheaf (J.over Z) A) (X_2 : (CategoryTheory.Over X)ᵒᵖ),
  ((J.overMapPullbackComp A f g).inv.app X_1).hom.app X_2 =
    X_1.obj.map ((CategoryTheory.Over.mapComp f g).inv.app (Opposite.unop X_2)).op

Defined in

Mathlib.CategoryTheory.Sites.Over

Cited by

3 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category