# The sheaf condition in terms of unique gluings #

We provide an alternative formulation of the sheaf condition in terms of unique gluings.

We work with sheaves valued in a concrete category C admitting all limits, whose forgetful functor C ⥤ Type preserves limits and reflects isomorphisms. The usual categories of algebraic structures, such as MonCat, AddCommGrp, RingCat, CommRingCat etc. are all examples of this kind of category.

A presheaf F : presheaf C X satisfies the sheaf condition if and only if, for every compatible family of sections sf : Π i : ι, F.obj (op (U i)), there exists a unique gluing s : F.obj (op (supr U)).

Here, the family sf is called compatible, if for all i j : ι, the restrictions of sf i and sf j to U i ⊓ U j agree. A section s : F.obj (op (supr U)) is a gluing for the family sf, if s restricts to sf i on U i for all i : ι

We show that the sheaf condition in terms of unique gluings is equivalent to the definition in terms of pairwise intersections. Our approach is as follows: First, we show them to be equivalent for Type-valued presheaves. Then we use that composing a presheaf with a limit-preserving and isomorphism-reflecting functor leaves the sheaf condition invariant, as shown in Mathlib/Topology/Sheaves/Forget.lean.

def TopCat.Presheaf.IsCompatible {C : Type u} {X : TopCat} (F : ) {ι : Type x} (U : ) (sf : (i : ι) → .obj (F.obj (Opposite.op (U i)))) :

A family of sections sf is compatible, if the restrictions of sf i and sf j to U i ⊓ U j agree, for all i and j

Equations
• F.IsCompatible U sf = ∀ (i j : ι), (F.map ((U i).infLELeft (U j)).op) (sf i) = (F.map ((U i).infLERight (U j)).op) (sf j)
Instances For
def TopCat.Presheaf.IsGluing {C : Type u} {X : TopCat} (F : ) {ι : Type x} (U : ) (sf : (i : ι) → .obj (F.obj (Opposite.op (U i)))) (s : .obj (F.obj (Opposite.op (iSup U)))) :

A section s is a gluing for a family of sections sf if it restricts to sf i on U i, for all i

Equations
• F.IsGluing U sf s = ∀ (i : ι), (F.map .op) s = sf i
Instances For

The sheaf condition in terms of unique gluings. A presheaf F : presheaf C X satisfies this sheaf condition if and only if, for every compatible family of sections sf : Π i : ι, F.obj (op (U i)), there exists a unique gluing s : F.obj (op (supr U)).

We prove this to be equivalent to the usual one below in TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.objPairwiseOfFamily {X : TopCat} {F : } {ι : Type x} {U : } (sf : (i : ι) → F.obj (Opposite.op (U i))) (i : ) :
(.comp F).obj i

Given sections over a family of open sets, extend it to include sections over pairwise intersections of the open sets.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.Presheaf.IsCompatible.sectionPairwise {X : TopCat} {F : } {ι : Type x} {U : } {sf : (i : ι) → .obj (F.obj (Opposite.op (U i)))} (h : F.IsCompatible U sf) :
(.comp F).sections

Given a compatible family of sections over open sets, extend it to a section of the functor (Pairwise.diagram U).op ⋙ F.

Equations
• h.sectionPairwise =
Instances For
theorem TopCat.Presheaf.isGluing_iff_pairwise {X : TopCat} {F : } {ι : Type x} {U : } {sf : (i : ι) → .obj (F.obj (Opposite.op (U i)))} {s : .obj (F.obj (Opposite.op (iSup U)))} :
F.IsGluing U sf s ∀ (i : ), .app i s =
theorem TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types {X : TopCat} (F : ) :
F.IsSheaf F.IsSheafUniqueGluing

For type-valued presheaves, the sheaf condition in terms of unique gluings is equivalent to the usual sheaf condition.

theorem TopCat.Presheaf.isSheaf_of_isSheafUniqueGluing_types {X : TopCat} (F : ) (Fsh : F.IsSheafUniqueGluing) :
F.IsSheaf

The usual sheaf condition can be obtained from the sheaf condition in terms of unique gluings.

theorem TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing {C : Type u} [.ReflectsIsomorphisms] {X : TopCat} (F : ) :
F.IsSheaf F.IsSheafUniqueGluing

For presheaves valued in a concrete category, whose forgetful functor reflects isomorphisms and preserves limits, the sheaf condition in terms of unique gluings is equivalent to the usual one.

theorem TopCat.Sheaf.existsUnique_gluing {C : Type u} [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : ) {ι : Type v} (U : ) (sf : (i : ι) → .obj (F.val.obj (Opposite.op (U i)))) (h : TopCat.Presheaf.IsCompatible F.val U sf) :
∃! s : .obj (F.val.obj (Opposite.op (iSup U))), TopCat.Presheaf.IsGluing F.val U sf s

A more convenient way of obtaining a unique gluing of sections for a sheaf.

theorem TopCat.Sheaf.existsUnique_gluing' {C : Type u} [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : ) {ι : Type v} (U : ) (V : ) (iUV : (i : ι) → U i V) (hcover : V iSup U) (sf : (i : ι) → .obj (F.val.obj (Opposite.op (U i)))) (h : TopCat.Presheaf.IsCompatible F.val U sf) :
∃! s : .obj (F.val.obj ()), ∀ (i : ι), (F.val.map (iUV i).op) s = sf i

In this version of the lemma, the inclusion homs iUV can be specified directly by the user, which can be more convenient in practice.

theorem TopCat.Sheaf.eq_of_locally_eq {C : Type u} [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : ) {ι : Type v} (U : ) (s : .obj (F.val.obj (Opposite.op (iSup U)))) (t : .obj (F.val.obj (Opposite.op (iSup U)))) (h : ∀ (i : ι), (F.val.map .op) s = (F.val.map .op) t) :
s = t
theorem TopCat.Sheaf.eq_of_locally_eq' {C : Type u} [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : ) {ι : Type v} (U : ) (V : ) (iUV : (i : ι) → U i V) (hcover : V iSup U) (s : .obj (F.val.obj ())) (t : .obj (F.val.obj ())) (h : ∀ (i : ι), (F.val.map (iUV i).op) s = (F.val.map (iUV i).op) t) :
s = t

In this version of the lemma, the inclusion homs iUV can be specified directly by the user, which can be more convenient in practice.

theorem TopCat.Sheaf.eq_of_locally_eq₂ {C : Type u} [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : ) {U₁ : } {U₂ : } {V : } (i₁ : U₁ V) (i₂ : U₂ V) (hcover : V U₁ U₂) (s : .obj (F.val.obj ())) (t : .obj (F.val.obj ())) (h₁ : (F.val.map i₁.op) s = (F.val.map i₁.op) t) (h₂ : (F.val.map i₂.op) s = (F.val.map i₂.op) t) :
s = t
theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff {X : TopCat} (F : ) {U : } {V : } {W : } {UW : } {VW : } (e : W U V) (x : ((RingHom.comp (F.val.map .op) (RingHom.fst (F.val.obj ()) (F.val.obj ()))).eqLocus (RingHom.comp (F.val.map .op) (RingHom.snd (F.val.obj ()) (F.val.obj ()))))) (y : (F.val.obj ())) (h₁ : UW = U W) (h₂ : VW = V W) :
(F.val.map .op) ((F.objSupIsoProdEqLocus U V).inv x) = y (F.val.map .op) (x).1 = (F.val.map .op) y (F.val.map .op) (x).2 = (F.val.map .op) y