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, 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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type x} (U : ιTopologicalSpace.Opens X) (sf : (i : ι) → (CategoryTheory.forget C).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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type x} (U : ιTopologicalSpace.Opens X) (sf : (i : ι) → (CategoryTheory.forget C).obj (F.obj (Opposite.op (U i)))) (s : (CategoryTheory.forget C).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
    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 : TopCat.Presheaf (Type u) X} {ι : Type x} {U : ιTopologicalSpace.Opens X} (sf : (i : ι) → F.obj (Opposite.op (U i))) (i : (CategoryTheory.Pairwise ι)ᵒᵖ) :
        ((CategoryTheory.Pairwise.diagram U).op.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 : TopCat.Presheaf (Type u) X} {ι : Type x} {U : ιTopologicalSpace.Opens X} {sf : (i : ι) → (CategoryTheory.forget (Type u)).obj (F.obj (Opposite.op (U i)))} (h : F.IsCompatible U sf) :
          ((CategoryTheory.Pairwise.diagram U).op.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
          Instances For
            theorem TopCat.Presheaf.isGluing_iff_pairwise {X : TopCat} {F : TopCat.Presheaf (Type u) X} {ι : Type x} {U : ιTopologicalSpace.Opens X} {sf : (i : ι) → (CategoryTheory.forget (Type u)).obj (F.obj (Opposite.op (U i)))} {s : (CategoryTheory.forget (Type u)).obj (F.obj (Opposite.op (iSup U)))} :
            theorem TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types {X : TopCat} (F : TopCat.Presheaf (Type u) X) :
            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 : TopCat.Presheaf (Type u) X) (Fsh : F.IsSheafUniqueGluing) :
            F.IsSheaf

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

            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.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : TopCat.Sheaf C X) {ι : Type v} (U : ιTopologicalSpace.Opens X) (sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (U i)))) (h : TopCat.Presheaf.IsCompatible F.val U sf) :
            ∃! s : (CategoryTheory.forget C).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.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : TopCat.Sheaf C X) {ι : Type v} (U : ιTopologicalSpace.Opens X) (V : TopologicalSpace.Opens X) (iUV : (i : ι) → U i V) (hcover : V iSup U) (sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (U i)))) (h : TopCat.Presheaf.IsCompatible F.val U sf) :
            ∃! s : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V)), ∀ (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.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : TopCat.Sheaf C X) {ι : Type v} (U : ιTopologicalSpace.Opens X) (s : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (iSup U)))) (t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op (iSup U)))) (h : ∀ (i : ι), (F.val.map (TopologicalSpace.Opens.leSupr U i).op) s = (F.val.map (TopologicalSpace.Opens.leSupr U i).op) t) :
            s = t
            theorem TopCat.Sheaf.eq_of_locally_eq' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : TopCat.Sheaf C X) {ι : Type v} (U : ιTopologicalSpace.Opens X) (V : TopologicalSpace.Opens X) (iUV : (i : ι) → U i V) (hcover : V iSup U) (s : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V))) (t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V))) (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.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.ConcreteCategory.forget.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits CategoryTheory.ConcreteCategory.forget] {X : TopCat} (F : TopCat.Sheaf C X) {U₁ : TopologicalSpace.Opens X} {U₂ : TopologicalSpace.Opens X} {V : TopologicalSpace.Opens X} (i₁ : U₁ V) (i₂ : U₂ V) (hcover : V U₁ U₂) (s : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V))) (t : (CategoryTheory.forget C).obj (F.val.obj (Opposite.op V))) (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 : TopCat.Sheaf CommRingCat X) {U : TopologicalSpace.Opens X} {V : TopologicalSpace.Opens X} {W : TopologicalSpace.Opens X} {UW : TopologicalSpace.Opens X} {VW : TopologicalSpace.Opens X} (e : W U V) (x : ((RingHom.comp (F.val.map (CategoryTheory.homOfLE ).op) (RingHom.fst (F.val.obj (Opposite.op U)) (F.val.obj (Opposite.op V)))).eqLocus (RingHom.comp (F.val.map (CategoryTheory.homOfLE ).op) (RingHom.snd (F.val.obj (Opposite.op U)) (F.val.obj (Opposite.op V)))))) (y : (F.val.obj (Opposite.op W))) (h₁ : UW = U W) (h₂ : VW = V W) :
            (F.val.map (CategoryTheory.homOfLE e).op) ((F.objSupIsoProdEqLocus U V).inv x) = y (F.val.map (CategoryTheory.homOfLE ).op) (x).1 = (F.val.map (CategoryTheory.homOfLE ).op) y (F.val.map (CategoryTheory.homOfLE ).op) (x).2 = (F.val.map (CategoryTheory.homOfLE ).op) y