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 states 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))

• J : Type v
• U : s.J → C
• V : s.J × s.J → C
• f : (i j : s.J) → CategoryTheory.GlueData.V s (i, j) ⟶ CategoryTheory.GlueData.U s i
• f_mono : ∀ (i j : s.J), CategoryTheory.Mono (CategoryTheory.GlueData.f s i j)
• f_hasPullback : ∀ (i j k : s.J), CategoryTheory.Limits.HasPullback (CategoryTheory.GlueData.f s i j) (CategoryTheory.GlueData.f s i k)
• f_id : ∀ (i : s.J), CategoryTheory.IsIso (CategoryTheory.GlueData.f s i i)
• t : (i j : s.J) → CategoryTheory.GlueData.V s (i, j) ⟶ CategoryTheory.GlueData.V s (j, i)
• t_id : ∀ (i : s.J), CategoryTheory.GlueData.t s i i = CategoryTheory.CategoryStruct.id (CategoryTheory.GlueData.V s (i, i))
• t' : (i j k : s.J) → CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f s i j) (CategoryTheory.GlueData.f s i k) ⟶ CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f s j k) (CategoryTheory.GlueData.f s j i)
• t_fac : ∀ (i j k : s.J), CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' s i j k) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.GlueData.t s i j)
• cocycle : ∀ (i j k : s.J), CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' s i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' s j k i) (CategoryTheory.GlueData.t' s k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f s i j) (CategoryTheory.GlueData.f s i k))

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 = 𝟙 _.

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 (CategoryTheory.GlueData.f self i j) (CategoryTheory.GlueData.f self i k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' self i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' self j k i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' self k i j) h)) = h

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 : CategoryTheory.GlueData.V self (j, i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' self i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t self i j) h)

@[simp]

theorem CategoryTheory.GlueData.t'_iij {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) : CategoryTheory.GlueData.t' D i i j = (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.GlueData.f D i i) (CategoryTheory.GlueData.f D i j)).hom

theorem CategoryTheory.GlueData.t'_jii {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) : CategoryTheory.GlueData.t' D j i i = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D j i) (CategoryTheory.inv CategoryTheory.Limits.pullback.snd))

theorem CategoryTheory.GlueData.t'_iji {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) : CategoryTheory.GlueData.t' D i j i = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D i j) (CategoryTheory.inv CategoryTheory.Limits.pullback.snd))

theorem CategoryTheory.GlueData.t_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) {Z : C} (h : CategoryTheory.GlueData.V D (i, j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D j i) h) = h

@[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 (CategoryTheory.GlueData.V D (i, j))) : ↑(CategoryTheory.GlueData.t D j i) (↑(CategoryTheory.GlueData.t D i j) x) = x

@[simp]

theorem CategoryTheory.GlueData.t_inv {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D i j) (CategoryTheory.GlueData.t D j i) = CategoryTheory.CategoryStruct.id (CategoryTheory.GlueData.V D (i, j))

theorem CategoryTheory.GlueData.t'_inv {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) (k : D.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' D i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.GlueData.f D j k) (CategoryTheory.GlueData.f D j i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' D j i k) (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.GlueData.f D i k) (CategoryTheory.GlueData.f D i j)).hom)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k))

instance CategoryTheory.GlueData.t_isIso {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) : CategoryTheory.IsIso (CategoryTheory.GlueData.t D i j)

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) : CategoryTheory.IsIso (CategoryTheory.GlueData.t' D i j k)

theorem CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry_assoc {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) (k : D.J) {Z : C} (h : CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' D j k i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' D k i j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.GlueData.f D j k) (CategoryTheory.GlueData.f D j i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' D j i k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.GlueData.f D i k) (CategoryTheory.GlueData.f D i j)).hom h))

theorem CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) (k : D.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' D j k i) (CategoryTheory.GlueData.t' D k i j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.GlueData.f D j k) (CategoryTheory.GlueData.f D j i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' D j i k) (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.GlueData.f D i k) (CategoryTheory.GlueData.f D i j)).hom)

def CategoryTheory.GlueData.sigmaOpens {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasCoproduct D.U] : C

(Implementation) The disjoint union of U i.

def CategoryTheory.GlueData.diagram {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) : CategoryTheory.Limits.MultispanIndex C

(Implementation) The diagram to take colimit of.

@[simp]

theorem CategoryTheory.GlueData.diagram_l {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) : (CategoryTheory.GlueData.diagram D).L = (D.J × D.J)

@[simp]

theorem CategoryTheory.GlueData.diagram_r {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) : (CategoryTheory.GlueData.diagram D).R = D.J

@[simp]

theorem CategoryTheory.GlueData.diagram_fstFrom {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i : D.J) (j : D.J) : CategoryTheory.Limits.MultispanIndex.fstFrom (CategoryTheory.GlueData.diagram D) (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) : CategoryTheory.Limits.MultispanIndex.sndFrom (CategoryTheory.GlueData.diagram D) (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) : CategoryTheory.Limits.MultispanIndex.fst (CategoryTheory.GlueData.diagram D) (i, j) = CategoryTheory.GlueData.f D 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) : CategoryTheory.Limits.MultispanIndex.snd (CategoryTheory.GlueData.diagram D) (i, j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D i j) (CategoryTheory.GlueData.f D j i)

@[simp]

theorem CategoryTheory.GlueData.diagram_left {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) : (CategoryTheory.GlueData.diagram D).left = D.V

@[simp]

theorem CategoryTheory.GlueData.diagram_right {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) : (CategoryTheory.GlueData.diagram D).right = D.U

def CategoryTheory.GlueData.glued {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] : C

The glued object given a family of gluing data.

def CategoryTheory.GlueData.ι {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] (i : D.J) : CategoryTheory.GlueData.U D i ⟶ CategoryTheory.GlueData.glued D

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

@[simp]

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

@[simp]

theorem CategoryTheory.GlueData.glue_condition {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] (i : D.J) (j : D.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.f D j i) (CategoryTheory.GlueData.ι D j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.ι D i)

def CategoryTheory.GlueData.vPullbackCone {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] (i : D.J) (j : D.J) : CategoryTheory.Limits.PullbackCone (CategoryTheory.GlueData.ι D i) (CategoryTheory.GlueData.ι 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.

def CategoryTheory.GlueData.π {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.GlueData.sigmaOpens D ⟶ CategoryTheory.GlueData.glued D

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

instance CategoryTheory.GlueData.π_epi {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Epi (CategoryTheory.GlueData.π D)

theorem CategoryTheory.GlueData.types_π_surjective (D : CategoryTheory.GlueData (Type u_1)) : Function.Surjective (CategoryTheory.GlueData.π D)

theorem CategoryTheory.GlueData.types_ι_jointly_surjective (D : CategoryTheory.GlueData (Type u_1)) (x : CategoryTheory.GlueData.glued D) : ∃ i y, CategoryTheory.GlueData.ι (Type u_1) CategoryTheory.types D (_ : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D))) i y = x

instance CategoryTheory.GlueData.instHasPullbackObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorVMkJUMapF {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J) (j : D.J) (k : D.J) : CategoryTheory.Limits.HasPullback (F.map (CategoryTheory.GlueData.f D i j)) (F.map (CategoryTheory.GlueData.f D i k))

@[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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J) (j : D.J) : CategoryTheory.GlueData.t (CategoryTheory.GlueData.mapGlueData D F) i j = F.map (CategoryTheory.GlueData.t D i j)

@[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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J) (j : D.J) : CategoryTheory.GlueData.f (CategoryTheory.GlueData.mapGlueData D F) i j = F.map (CategoryTheory.GlueData.f D 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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J) : CategoryTheory.GlueData.U (CategoryTheory.GlueData.mapGlueData D F) i = F.obj (CategoryTheory.GlueData.U D i)

@[simp]

theorem CategoryTheory.GlueData.mapGlueData_J {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] : (CategoryTheory.GlueData.mapGlueData D F).J = D.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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J × D.J) : CategoryTheory.GlueData.V (CategoryTheory.GlueData.mapGlueData D F) i = F.obj (CategoryTheory.GlueData.V D 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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J) (j : D.J) (k : D.J) : CategoryTheory.GlueData.t' (CategoryTheory.GlueData.mapGlueData D F) i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso F (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)).inv (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.GlueData.t' D i j k)) (CategoryTheory.Limits.PreservesPullback.iso F (CategoryTheory.GlueData.f D j k) (CategoryTheory.GlueData.f D j i)).hom)

def CategoryTheory.GlueData.mapGlueData {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] : CategoryTheory.GlueData C'

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

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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] : CategoryTheory.Functor.comp (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F ≅ CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram (CategoryTheory.GlueData.mapGlueData D F))

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

@[simp]

theorem CategoryTheory.GlueData.diagramIso_app_left {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J × D.J) : (CategoryTheory.GlueData.diagramIso D F).app (CategoryTheory.Limits.WalkingMultispan.left i) = CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F).obj (CategoryTheory.Limits.WalkingMultispan.left i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_app_right {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J) : (CategoryTheory.GlueData.diagramIso D F).app (CategoryTheory.Limits.WalkingMultispan.right i) = CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F).obj (CategoryTheory.Limits.WalkingMultispan.right i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_hom_app_left {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J × D.J) : (CategoryTheory.GlueData.diagramIso D F).hom.app (CategoryTheory.Limits.WalkingMultispan.left i) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F).obj (CategoryTheory.Limits.WalkingMultispan.left i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_hom_app_right {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J) : (CategoryTheory.GlueData.diagramIso D F).hom.app (CategoryTheory.Limits.WalkingMultispan.right i) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F).obj (CategoryTheory.Limits.WalkingMultispan.right i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_inv_app_left {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J × D.J) : (CategoryTheory.GlueData.diagramIso D F).inv.app (CategoryTheory.Limits.WalkingMultispan.left i) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram (CategoryTheory.GlueData.mapGlueData D F))).obj (CategoryTheory.Limits.WalkingMultispan.left i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_inv_app_right {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (i : D.J) : (CategoryTheory.GlueData.diagramIso D F).inv.app (CategoryTheory.Limits.WalkingMultispan.right i) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram (CategoryTheory.GlueData.mapGlueData D F))).obj (CategoryTheory.Limits.WalkingMultispan.right i))

theorem CategoryTheory.GlueData.hasColimit_multispan_comp {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') [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F)

theorem CategoryTheory.GlueData.hasColimit_mapGlueData_diagram {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] : CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram (CategoryTheory.GlueData.mapGlueData D F))

def CategoryTheory.GlueData.gluedIso {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] : F.obj (CategoryTheory.GlueData.glued D) ≅ CategoryTheory.GlueData.glued (CategoryTheory.GlueData.mapGlueData D F)

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

@[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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] (i : D.J) {Z : C'} (h : CategoryTheory.GlueData.glued (CategoryTheory.GlueData.mapGlueData D F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.GlueData.ι D i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.gluedIso D F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.ι (CategoryTheory.GlueData.mapGlueData D 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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] (i : D.J) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.GlueData.ι D i)) (CategoryTheory.GlueData.gluedIso D F).hom = CategoryTheory.GlueData.ι (CategoryTheory.GlueData.mapGlueData D F) i

@[simp]

theorem CategoryTheory.GlueData.ι_gluedIso_inv_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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] (i : D.J) {Z : C'} (h : F.obj (CategoryTheory.GlueData.glued D) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.ι (CategoryTheory.GlueData.mapGlueData D F) i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.gluedIso D F).inv h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.GlueData.ι D i)) h

@[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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] (i : D.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.ι (CategoryTheory.GlueData.mapGlueData D F) i) (CategoryTheory.GlueData.gluedIso D F).inv = F.map (CategoryTheory.GlueData.ι D i)

def CategoryTheory.GlueData.vPullbackConeIsLimitOfMap {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 (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] (i : D.J) (j : D.J) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan (CategoryTheory.GlueData.ι D i) (CategoryTheory.GlueData.ι D j)) F] (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.GlueData.vPullbackCone (CategoryTheory.GlueData.mapGlueData D F) i j)) : CategoryTheory.Limits.IsLimit (CategoryTheory.GlueData.vPullbackCone D 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.

theorem CategoryTheory.GlueData.ι_jointly_surjective {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.GlueData.diagram D)] (F : CategoryTheory.Functor C (Type v)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.MultispanIndex.multispan (CategoryTheory.GlueData.diagram D)) F] [(i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (CategoryTheory.GlueData.f D i j) (CategoryTheory.GlueData.f D i k)) F] (x : F.obj (CategoryTheory.GlueData.glued D)) : ∃ i y, C.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor (CategoryTheory.GlueData.U D i) (CategoryTheory.GlueData.glued D) (CategoryTheory.GlueData.ι D i) y = x

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