Theorems · Theorem · category theory

CategoryTheory.Presheaf.IsSheaf.amalgamate_map

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y))
  (hx :
    ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
      CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) =
        CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op))
  (I : S.Arrow), CategoryTheory.CategoryStruct.comp (hP.amalgamate S x hx) (P.map I.f.op) = x I

Defined in

Mathlib.CategoryTheory.Sites.Sheaf

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category