Documentation

Mathlib.CategoryTheory.GlueData

Gluing data #

We define GlueData as a family of data needed to glue topological spaces, schemes, etc. We provide the API to realize it as a multispan diagram, and also state lemmas about its interaction with a functor that preserves certain pullbacks.

structure CategoryTheory.GlueData (C : Type u₁) [CategoryTheory.Category.{v, u₁} C] :
Type (max u₁ (v + 1))

A gluing datum consists of

  1. An index type J
  2. An object U i for each i : J.
  3. An object V i j for each i j : J.
  4. A monomorphism f i j : V i j ⟶ U i for each i j : J.
  5. A transition map t i j : V i j ⟶ V j i for each i j : J. such that
  6. f i i is an isomorphism.
  7. t i i is the identity.
  8. The pullback for f i j and f i k exists.
  9. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i.
  10. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.
Instances For
    theorem CategoryTheory.GlueData.f_mono {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J) (j : self.J) :
    CategoryTheory.Mono (self.f i j)
    theorem CategoryTheory.GlueData.f_hasPullback {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J) (j : self.J) (k : self.J) :
    CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
    @[simp]
    theorem CategoryTheory.GlueData.t_fac {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J) (j : self.J) (k : self.J) :
    theorem CategoryTheory.GlueData.cocycle {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J) (j : self.J) (k : self.J) :
    theorem CategoryTheory.GlueData.t_fac_assoc {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J) (j : self.J) (k : self.J) {Z : C} (h : self.V (j, i) Z) :
    theorem CategoryTheory.GlueData.cocycle_assoc {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J) (j : self.J) (k : self.J) {Z : C} (h : CategoryTheory.Limits.pullback (self.f i j) (self.f i k) Z) :
    @[simp]
    theorem CategoryTheory.GlueData.t'_iij {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) :
    D.t' i i j = (CategoryTheory.Limits.pullbackSymmetry (D.f i i) (D.f i j)).hom
    @[simp]
    theorem CategoryTheory.GlueData.t_inv_apply {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (D.V (i, j))) :
    (D.t j i) ((D.t i j) x) = x
    Equations
    • =
    instance CategoryTheory.GlueData.t'_isIso {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) (k : D.J) :
    Equations
    • =

    (Implementation) The disjoint union of U i.

    Equations
    • D.sigmaOpens = D.U
    Instances For

      (Implementation) The diagram to take colimit of.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.GlueData.diagram_fstFrom {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) :
        D.diagram.fstFrom (i, j) = i
        @[simp]
        theorem CategoryTheory.GlueData.diagram_sndFrom {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) :
        D.diagram.sndFrom (i, j) = j
        @[simp]
        theorem CategoryTheory.GlueData.diagram_fst {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) :
        D.diagram.fst (i, j) = D.f i j
        @[simp]
        theorem CategoryTheory.GlueData.diagram_snd {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) :
        D.diagram.snd (i, j) = CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i)

        The glued object given a family of gluing data.

        Equations
        Instances For

          The map D.U i ⟶ D.glued for each i.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.GlueData.glue_condition_apply {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i : D.J) (j : D.J) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (D.V (i, j))) :
            (D j) ((D.f j i) ((D.t i j) x)) = (D i) ((D.f i j) x)

            The pullback cone spanned by V i j ⟶ U i and V i j ⟶ U j. This will often be a pullback diagram.

            Equations
            Instances For

              The projection ∐ D.U ⟶ D.glued given by the colimit.

              Equations
              Instances For
                theorem CategoryTheory.GlueData.types_ι_jointly_surjective (D : CategoryTheory.GlueData (Type v)) (x : D.glued) :
                ∃ (i : D.J) (y : D.U i), D i y = x
                instance CategoryTheory.GlueData.instHasPullbackMapF {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) (j : D.J) (k : D.J) :
                CategoryTheory.Limits.HasPullback (F.map (D.f i j)) (F.map (D.f i k))
                Equations
                • =
                @[simp]
                theorem CategoryTheory.GlueData.mapGlueData_f {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) (j : D.J) :
                (D.mapGlueData F).f i j = F.map (D.f i j)
                @[simp]
                theorem CategoryTheory.GlueData.mapGlueData_V {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) :
                (D.mapGlueData F).V i = F.obj (D.V i)
                @[simp]
                theorem CategoryTheory.GlueData.mapGlueData_t {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) (j : D.J) :
                (D.mapGlueData F).t i j = F.map (D.t i j)
                @[simp]
                theorem CategoryTheory.GlueData.mapGlueData_U {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) :
                (D.mapGlueData F).U i = F.obj (D.U i)
                @[simp]
                theorem CategoryTheory.GlueData.mapGlueData_t' {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) (j : D.J) (k : D.J) :
                (D.mapGlueData F).t' i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso F (D.f i j) (D.f i k)).inv (CategoryTheory.CategoryStruct.comp (F.map (D.t' i j k)) (CategoryTheory.Limits.PreservesPullback.iso F (D.f j k) (D.f j i)).hom)

                A functor that preserves the pullbacks of f i j and f i k can map a family of glue data.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def CategoryTheory.GlueData.diagramIso {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] :
                  D.diagram.multispan.comp F (D.mapGlueData F).diagram.multispan

                  The diagram of the image of a GlueData under a functor F is naturally isomorphic to the original diagram of the GlueData via F.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    If F preserves the gluing, we obtain an iso between the glued objects.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.GlueData.ι_gluedIso_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] (i : D.J) {Z : C'} (h : (D.mapGlueData F).glued Z) :
                      CategoryTheory.CategoryStruct.comp (F.map (D i)) (CategoryTheory.CategoryStruct.comp (D.gluedIso F).hom h) = CategoryTheory.CategoryStruct.comp ((D.mapGlueData F) i) h
                      @[simp]
                      theorem CategoryTheory.GlueData.ι_gluedIso_hom {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] (i : D.J) :
                      CategoryTheory.CategoryStruct.comp (F.map (D i)) (D.gluedIso F).hom = (D.mapGlueData F) i
                      @[simp]
                      theorem CategoryTheory.GlueData.ι_gluedIso_inv {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] (i : D.J) :
                      CategoryTheory.CategoryStruct.comp ((D.mapGlueData F) i) (D.gluedIso F).inv = F.map (D i)

                      If F preserves the gluing, and reflects the pullback of U i ⟶ glued and U j ⟶ glued, then F reflects the fact that V_pullback_cone is a pullback.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem CategoryTheory.GlueData.ι_jointly_surjective {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] (F : CategoryTheory.Functor C (Type v)) [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [(i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (x : F.obj D.glued) :
                        ∃ (i : D.J) (y : F.obj (D.U i)), F.map (D i) y = x

                        If there is a forgetful functor into Type that preserves enough (co)limits, then D.ι will be jointly surjective.

                        structure CategoryTheory.GlueData' (C : Type u₁) [CategoryTheory.Category.{v, u₁} C] :
                        Type (max u₁ (v + 1))

                        This is a variant of GlueData that only requires conditions on V (i, j) when i ≠ j. See GlueData.ofGlueData'

                        Instances For
                          theorem CategoryTheory.GlueData'.f_mono {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i : self.J) (j : self.J) (h : i j) :
                          CategoryTheory.Mono (self.f i j h)
                          theorem CategoryTheory.GlueData'.f_hasPullback {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i : self.J) (j : self.J) (k : self.J) (hij : i j) (hik : i k) :
                          CategoryTheory.Limits.HasPullback (self.f i j hij) (self.f i k hik)
                          theorem CategoryTheory.GlueData'.t_fac {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i : self.J) (j : self.J) (k : self.J) (hij : i j) (hik : i k) (hjk : j k) :
                          CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk) (CategoryTheory.Limits.pullback.snd (self.f j k hjk) (self.f j i )) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (self.f i j hij) (self.f i k hik)) (self.t i j hij)
                          @[simp]
                          theorem CategoryTheory.GlueData'.t_inv {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i : self.J) (j : self.J) (hij : i j) :
                          CategoryTheory.CategoryStruct.comp (self.t i j hij) (self.t j i ) = CategoryTheory.CategoryStruct.id (self.V i j hij)
                          @[simp]
                          theorem CategoryTheory.GlueData'.cocycle {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i : self.J) (j : self.J) (k : self.J) (hij : i j) (hik : i k) (hjk : j k) :
                          CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk) (CategoryTheory.CategoryStruct.comp (self.t' j k i hjk ) (self.t' k i j hij)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j hij) (self.f i k hik))
                          @[simp]
                          theorem CategoryTheory.GlueData'.cocycle_assoc {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i : self.J) (j : self.J) (k : self.J) (hij : i j) (hik : i k) (hjk : j k) {Z : C} (h : CategoryTheory.Limits.pullback (self.f i j hij) (self.f i k ) Z) :
                          CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk) (CategoryTheory.CategoryStruct.comp (self.t' j k i hjk ) (CategoryTheory.CategoryStruct.comp (self.t' k i j hij) h)) = h
                          @[simp]
                          theorem CategoryTheory.GlueData'.t_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i : self.J) (j : self.J) (hij : i j) {Z : C} (h : self.V i j Z) :
                          @[reducible, inline]
                          abbrev CategoryTheory.GlueData'.f' {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData' C) (i : D.J) (j : D.J) :
                          (if h : i = j then D.U i else D.V i j h) D.U i

                          (Implementation detail) the constructed GlueData.f from a GlueData'.

                          Equations
                          Instances For
                            Equations
                            • =
                            instance CategoryTheory.instHasPullbackF' {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData' C) (i : D.J) (j : D.J) (k : D.J) :
                            CategoryTheory.Limits.HasPullback (D.f' i j) (D.f' i k)
                            Equations
                            • =
                            def CategoryTheory.GlueData'.t'' {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData' C) (i : D.J) (j : D.J) (k : D.J) :
                            CategoryTheory.Limits.pullback (D.f' i j) (D.f' i k) CategoryTheory.Limits.pullback (D.f' j k) (D.f' j i)

                            (Implementation detail) the constructed GlueData.t' from a GlueData'.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              The constructed GlueData of a GlueData', where GlueData' is a variant of GlueData that only requires conditions on V (i, j) when i ≠ j.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For