Theorems · Theorem · category theory

CategoryTheory.Presheaf.IsSheaf.hom_ext

∀ {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},
  CategoryTheory.Presheaf.IsSheaf J P →
    ∀ (S : J.Cover X) (e₁ e₂ : E ⟶ P.obj (Opposite.op X)),
      (∀ (I : S.Arrow),
          CategoryTheory.CategoryStruct.comp e₁ (P.map I.f.op) = CategoryTheory.CategoryStruct.comp e₂ (P.map I.f.op)) →
        e₁ = e₂

Defined in

Mathlib.CategoryTheory.Sites.Sheaf

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category