# 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₁) [] :
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₁} [] (self : ) (i : self.J) (j : self.J) :
CategoryTheory.Mono (self.f i j)
theorem CategoryTheory.GlueData.f_hasPullback {C : Type u₁} [] (self : ) (i : self.J) (j : self.J) (k : self.J) :
CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
theorem CategoryTheory.GlueData.f_id {C : Type u₁} [] (self : ) (i : self.J) :
@[simp]
theorem CategoryTheory.GlueData.t_id {C : Type u₁} [] (self : ) (i : self.J) :
self.t i i = CategoryTheory.CategoryStruct.id (self.V (i, i))
theorem CategoryTheory.GlueData.t_fac {C : Type u₁} [] (self : ) (i : self.J) (j : self.J) (k : self.J) :
CategoryTheory.CategoryStruct.comp (self.t' i j k) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (self.t i j)
theorem CategoryTheory.GlueData.cocycle {C : Type u₁} [] (self : ) (i : self.J) (j : self.J) (k : self.J) :
theorem CategoryTheory.GlueData.cocycle_assoc {C : Type u₁} [] (self : ) (i : self.J) (j : self.J) (k : self.J) {Z : C} (h : CategoryTheory.Limits.pullback (self.f i j) (self.f i k) Z) :
theorem CategoryTheory.GlueData.t_fac_assoc {C : Type u₁} [] (self : ) (i : self.J) (j : self.J) (k : self.J) {Z : C} (h : self.V (j, i) Z) :
CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (self.t i j) h)
@[simp]
theorem CategoryTheory.GlueData.t'_iij {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
D.t' i i j = (CategoryTheory.Limits.pullbackSymmetry (D.f i i) (D.f i j)).hom
theorem CategoryTheory.GlueData.t'_jii {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
D.t' j i i = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t j i) (CategoryTheory.inv CategoryTheory.Limits.pullback.snd))
theorem CategoryTheory.GlueData.t'_iji {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
D.t' i j i = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.inv CategoryTheory.Limits.pullback.snd))
theorem CategoryTheory.GlueData.t_inv_assoc {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) {Z : C} (h : D.V (i, j) Z) :
@[simp]
theorem CategoryTheory.GlueData.t_inv_apply {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) [inst : ] (x : .obj (D.V (i, j))) :
(D.t j i) ((D.t i j) x) = x
@[simp]
theorem CategoryTheory.GlueData.t_inv {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
instance CategoryTheory.GlueData.t_isIso {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
Equations
• =
instance CategoryTheory.GlueData.t'_isIso {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) (k : D.J) :
Equations
• =
theorem CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) (k : D.J) :
def CategoryTheory.GlueData.sigmaOpens {C : Type u₁} [] (D : ) :
C

(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_l {C : Type u₁} [] (D : ) :
D.diagram.L = (D.J × D.J)
@[simp]
theorem CategoryTheory.GlueData.diagram_r {C : Type u₁} [] (D : ) :
D.diagram.R = D.J
@[simp]
theorem CategoryTheory.GlueData.diagram_fstFrom {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
D.diagram.fstFrom (i, j) = i
@[simp]
theorem CategoryTheory.GlueData.diagram_sndFrom {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
D.diagram.sndFrom (i, j) = j
@[simp]
theorem CategoryTheory.GlueData.diagram_fst {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
D.diagram.fst (i, j) = D.f i j
@[simp]
theorem CategoryTheory.GlueData.diagram_snd {C : Type u₁} [] (D : ) (i : D.J) (j : D.J) :
D.diagram.snd (i, j) = CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i)
@[simp]
theorem CategoryTheory.GlueData.diagram_left {C : Type u₁} [] (D : ) :
D.diagram.left = D.V
@[simp]
theorem CategoryTheory.GlueData.diagram_right {C : Type u₁} [] (D : ) :
D.diagram.right = D.U
def CategoryTheory.GlueData.glued {C : Type u₁} [] (D : ) [] :
C

The glued object given a family of gluing data.

Equations
• D.glued =
Instances For
def CategoryTheory.GlueData.ι {C : Type u₁} [] (D : ) [] (i : D.J) :
D.U i D.glued

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

Equations
Instances For
@[simp]
theorem CategoryTheory.GlueData.glue_condition_apply {C : Type u₁} [] (D : ) [] (i : D.J) (j : D.J) [inst : ] (x : .obj (D.V (i, j))) :
(D j) ((D.f j i) ((D.t i j) x)) = (D i) ((D.f i j) x)
@[simp]
theorem CategoryTheory.GlueData.glue_condition {C : Type u₁} [] (D : ) [] (i : D.J) (j : D.J) :
def CategoryTheory.GlueData.vPullbackCone {C : Type u₁} [] (D : ) [] (i : D.J) (j : D.J) :

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
def CategoryTheory.GlueData.π {C : Type u₁} [] (D : ) [] :
D.sigmaOpens D.glued

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

Equations
• D =
Instances For
instance CategoryTheory.GlueData.π_epi {C : Type u₁} [] (D : ) [] :
Equations
• =
theorem CategoryTheory.GlueData.types_ι_jointly_surjective (D : ) (x : D.glued) :
∃ (i : D.J) (y : D.U i), D i y = x
instance CategoryTheory.GlueData.instHasPullbackMapF {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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_t {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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_f {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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_U {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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_J {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] :
(D.mapGlueData F).J = D.J
@[simp]
theorem CategoryTheory.GlueData.mapGlueData_V {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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₁} [] {C' : Type u₂} [] (D : ) (F : ) [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)
def CategoryTheory.GlueData.mapGlueData {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] :

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₁} [] {C' : Type u₂} [] (D : ) (F : ) [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
@[simp]
theorem CategoryTheory.GlueData.diagramIso_app_left {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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.diagramIso F).app = CategoryTheory.Iso.refl ((D.diagram.multispan.comp F).obj )
@[simp]
theorem CategoryTheory.GlueData.diagramIso_app_right {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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.diagramIso F).app = CategoryTheory.Iso.refl ((D.diagram.multispan.comp F).obj )
@[simp]
theorem CategoryTheory.GlueData.diagramIso_hom_app_left {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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.diagramIso F).hom.app = CategoryTheory.CategoryStruct.id ((D.diagram.multispan.comp F).obj )
@[simp]
theorem CategoryTheory.GlueData.diagramIso_hom_app_right {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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.diagramIso F).hom.app = CategoryTheory.CategoryStruct.id ((D.diagram.multispan.comp F).obj )
@[simp]
theorem CategoryTheory.GlueData.diagramIso_inv_app_left {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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.diagramIso F).inv.app = CategoryTheory.CategoryStruct.id ((D.mapGlueData F).diagram.multispan.obj )
@[simp]
theorem CategoryTheory.GlueData.diagramIso_inv_app_right {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [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.diagramIso F).inv.app = CategoryTheory.CategoryStruct.id ((D.mapGlueData F).diagram.multispan.obj )
theorem CategoryTheory.GlueData.hasColimit_multispan_comp {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] :
CategoryTheory.Limits.HasColimit (D.diagram.multispan.comp F)
theorem CategoryTheory.GlueData.hasColimit_mapGlueData_diagram {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] :
def CategoryTheory.GlueData.gluedIso {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] :
F.obj D.glued (D.mapGlueData F).glued

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₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [] [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₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [] [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_assoc {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] (i : D.J) {Z : C'} (h : F.obj D.glued Z) :
CategoryTheory.CategoryStruct.comp ((D.mapGlueData F) i) (CategoryTheory.CategoryStruct.comp (D.gluedIso F).inv h) = CategoryTheory.CategoryStruct.comp (F.map (D i)) h
@[simp]
theorem CategoryTheory.GlueData.ι_gluedIso_inv {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [] [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)
def CategoryTheory.GlueData.vPullbackConeIsLimitOfMap {C : Type u₁} [] {C' : Type u₂} [] (D : ) (F : ) [H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] [] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] (i : D.J) (j : D.J) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan (D i) (D j)) F] (hc : CategoryTheory.Limits.IsLimit ((D.mapGlueData F).vPullbackCone i j)) :
CategoryTheory.Limits.IsLimit (D.vPullbackCone i j)

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₁} [] (D : ) [] (F : ) [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.