# Documentation

Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

# 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, AddCommGroupCat, 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 equalizers. 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

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

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

Instances For
def TopCat.Presheaf.piOpensIsoSectionsFamily {X : TopCat} (F : ) {ι : Type x} (U : ) :
((i : ι) → F.obj (Opposite.op (U i)))

For presheaves of types, terms of piOpens F U are just families of sections.

Instances For
@[simp]
theorem TopCat.Presheaf.piOpensIsoSectionsFamily_apply {X : TopCat} (F : ) {ι : Type x} (U : ) (i : ι) :
theorem TopCat.Presheaf.compatible_iff_leftRes_eq_rightRes {X : TopCat} (F : ) {ι : Type x} (U : ) :

Under the isomorphism piOpensIsoSectionsFamily, compatibility of sections is the same as being equalized by the arrows leftRes and rightRes of the equalizer diagram.

@[simp]
theorem TopCat.Presheaf.isGluing_iff_eq_res {X : TopCat} (F : ) {ι : Type x} (U : ) (s : F.obj (Opposite.op (iSup U))) :

Under the isomorphism piOpensIsoSectionsFamily, being a gluing of a family of sections sf is the same as lying in the preimage of res (the leftmost arrow of the equalizer diagram).

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

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

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

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 in terms of equalizer diagrams.

theorem TopCat.Sheaf.existsUnique_gluing {C : Type u} [CategoryTheory.ReflectsIsomorphisms CategoryTheory.ConcreteCategory.forget] [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, 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.ReflectsIsomorphisms CategoryTheory.ConcreteCategory.forget] [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, ∀ (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.ReflectsIsomorphisms CategoryTheory.ConcreteCategory.forget] [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.ReflectsIsomorphisms CategoryTheory.ConcreteCategory.forget] [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.ReflectsIsomorphisms CategoryTheory.ConcreteCategory.forget] [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