def TopCat.Presheaf.SatisfiesGluing {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} (F : Presheaf C X) : Prop

Gluing axiom: every compatible family (sᵢ ∈ F(Uᵢ)) of local sections admits a section on the union ⋃ Uᵢ whose restrictions agree with sᵢ.

def TopCat.Presheaf.SatisfiesLocality {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} (F : Presheaf C X) : Prop

Locality axiom: two sections of F over ⋃ Uᵢ that agree on every Uᵢ are equal.

theorem TopCat.Presheaf.isSheafUniqueGluing_iff_gluing_and_locality {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} (F : Presheaf C X) : F.IsSheafUniqueGluing ↔ F.SatisfiesGluing ∧ F.SatisfiesLocality

The "unique gluing" sheaf condition is equivalent to the conjunction of the gluing and locality axioms.

theorem TopCat.Presheaf.isSheaf_iff_gluing_and_locality {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} (F : Presheaf C X) [CategoryTheory.Limits.HasLimitsOfSize.{x, x, u_4, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, u_4, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] : F.IsSheaf ↔ F.SatisfiesGluing ∧ F.SatisfiesLocality

The standard IsSheaf condition (limit-based) is equivalent to gluing + locality in concrete categories with the appropriate limits.

theorem TopCat.Sheaf.satisfiesGluing {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} [CategoryTheory.Limits.HasLimitsOfSize.{x, x, u_4, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, u_4, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] (ℱ : Sheaf C X) : Presheaf.SatisfiesGluing ℱ.obj

A sheaf satisfies the gluing axiom.

theorem TopCat.Sheaf.satisfiesLocality {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : TopCat} [CategoryTheory.Limits.HasLimitsOfSize.{x, x, u_4, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, u_4, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] (ℱ : Sheaf C X) : Presheaf.SatisfiesLocality ℱ.obj

A sheaf satisfies the locality axiom.