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

• J : Type v

  The index type J of a gluing datum

• U : self.J → C

  For each i : J, an object U i

• V : self.J × self.J → C

  For each i j : J, an object V i j

• f (i j : self.J) : self.V (i, j) ⟶ self.U i

  For each i j : J, a monomorphism f i j : V i j ⟶ U i

• f_mono (i j : self.J) : Mono (self.f i j)
• f_hasPullback (i j k : self.J) : Limits.HasPullback (self.f i j) (self.f i k)
• f_id (i : self.J) : IsIso (self.f i i)
• t (i j : self.J) : self.V (i, j) ⟶ self.V (j, i)

  For each i j : J, a transition map t i j : V i j ⟶ V j i

• t_id (i : self.J) : self.t i i = CategoryStruct.id (self.V (i, i))
• t' (i j k : self.J) : Limits.pullback (self.f i j) (self.f i k) ⟶ Limits.pullback (self.f j k) (self.f j i)

  The morphism via which 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

• t_fac (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (Limits.pullback.snd (self.f j k) (self.f j i)) = CategoryStruct.comp (Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
• cocycle (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryStruct.id (Limits.pullback (self.f i j) (self.f i k))

theorem CategoryTheory.GlueData.t_fac_assoc {C : Type u₁} [Category.{v, u₁} C] (self : GlueData C) (i j k : self.J) {Z : C} (h : self.V (j, i) ⟶ Z) : CategoryStruct.comp (self.t' i j k) (CategoryStruct.comp (Limits.pullback.snd (self.f j k) (self.f j i)) h) = CategoryStruct.comp (Limits.pullback.fst (self.f i j) (self.f i k)) (CategoryStruct.comp (self.t i j) h)

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.GlueData.t_inv_apply {C : Type u₁} [Category.{v, u₁} C] (D : GlueData C) (i j : D.J) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType (D.V (i, j))) : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (D.t i j)) x) = x

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

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

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

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

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

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

(Implementation) The disjoint union of U i.

Equations

• D.sigmaOpens = ∐ D.U

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

(Implementation) The diagram to take colimit of.

Equations

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

@[simp]

theorem CategoryTheory.GlueData.diagram_fst {C : Type u₁} [Category.{v, u₁} C] (D : GlueData C) (i j : D.J) : D.diagram.fst (i, j) = D.f i j

@[simp]

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

@[simp]

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

@[simp]

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

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

The glued object given a family of gluing data.

Equations

• D.glued = CategoryTheory.Limits.multicoequalizer D.diagram

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

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

Equations

• D.ι i = CategoryTheory.Limits.Multicoequalizer.π D.diagram i

@[simp]

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

@[simp]

theorem CategoryTheory.GlueData.glue_condition_apply {C : Type u₁} [Category.{v, u₁} C] (D : GlueData C) [Limits.HasMulticoequalizer D.diagram] (i j : D.J) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType (D.V (i, j))) : (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) x)) = (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) x)

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

• D.vPullbackCone i j = CategoryTheory.Limits.PullbackCone.mk (D.f i j) (CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i)) ⋯

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

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

Equations

• D.π = CategoryTheory.Limits.Multicoequalizer.sigmaπ D.diagram

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

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

theorem CategoryTheory.GlueData.types_ι_jointly_surjective (D : GlueData (Type v)) (x : D.glued) : ∃ (i : D.J) (y : D.U i), D.ι i y = x

instance CategoryTheory.GlueData.instHasPullbackMapF {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i j k : D.J) : Limits.HasPullback (F.map (D.f i j)) (F.map (D.f i k))

def CategoryTheory.GlueData.mapGlueData {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] : GlueData C'

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.

@[simp]

theorem CategoryTheory.GlueData.mapGlueData_V {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (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_U {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (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₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i j : D.J) : (D.mapGlueData F).t i j = F.map (D.t i j)

@[simp]

theorem CategoryTheory.GlueData.mapGlueData_t' {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i j k : D.J) : (D.mapGlueData F).t' i j k = CategoryStruct.comp (Limits.PreservesPullback.iso F (D.f i j) (D.f i k)).inv (CategoryStruct.comp (F.map (D.t' i j k)) (Limits.PreservesPullback.iso F (D.f j k) (D.f j i)).hom)

@[simp]

theorem CategoryTheory.GlueData.mapGlueData_f {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i j : D.J) : (D.mapGlueData F).f i j = F.map (D.f i j)

@[simp]

theorem CategoryTheory.GlueData.mapGlueData_J {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] : (D.mapGlueData F).J = D.J

def CategoryTheory.GlueData.diagramIso {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (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.

@[simp]

theorem CategoryTheory.GlueData.diagramIso_app_left {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) : (D.diagramIso F).app (Limits.WalkingMultispan.left i) = Iso.refl ((D.diagram.multispan.comp F).obj (Limits.WalkingMultispan.left i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_app_right {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) : (D.diagramIso F).app (Limits.WalkingMultispan.right i) = Iso.refl ((D.diagram.multispan.comp F).obj (Limits.WalkingMultispan.right i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_hom_app_left {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) : (D.diagramIso F).hom.app (Limits.WalkingMultispan.left i) = CategoryStruct.id ((D.diagram.multispan.comp F).obj (Limits.WalkingMultispan.left i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_hom_app_right {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) : (D.diagramIso F).hom.app (Limits.WalkingMultispan.right i) = CategoryStruct.id ((D.diagram.multispan.comp F).obj (Limits.WalkingMultispan.right i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_inv_app_left {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) : (D.diagramIso F).inv.app (Limits.WalkingMultispan.left i) = CategoryStruct.id ((D.mapGlueData F).diagram.multispan.obj (Limits.WalkingMultispan.left i))

@[simp]

theorem CategoryTheory.GlueData.diagramIso_inv_app_right {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) : (D.diagramIso F).inv.app (Limits.WalkingMultispan.right i) = CategoryStruct.id ((D.mapGlueData F).diagram.multispan.obj (Limits.WalkingMultispan.right i))

theorem CategoryTheory.GlueData.hasColimit_multispan_comp {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [Limits.HasMulticoequalizer D.diagram] [Limits.PreservesColimit D.diagram.multispan F] : Limits.HasColimit (D.diagram.multispan.comp F)

theorem CategoryTheory.GlueData.hasColimit_mapGlueData_diagram {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [Limits.HasMulticoequalizer D.diagram] [Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] : Limits.HasMulticoequalizer (D.mapGlueData F).diagram

def CategoryTheory.GlueData.gluedIso {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [Limits.HasMulticoequalizer D.diagram] [Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] : F.obj D.glued ≅ (D.mapGlueData F).glued

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

Equations

• D.gluedIso F = CategoryTheory.preservesColimitIso F D.diagram.multispan ≪≫ CategoryTheory.Limits.HasColimit.isoOfNatIso (D.diagramIso F)

@[simp]

theorem CategoryTheory.GlueData.ι_gluedIso_hom {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [Limits.HasMulticoequalizer D.diagram] [Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) : CategoryStruct.comp (F.map (D.ι i)) (D.gluedIso F).hom = (D.mapGlueData F).ι i

@[simp]

theorem CategoryTheory.GlueData.ι_gluedIso_hom_assoc {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [Limits.HasMulticoequalizer D.diagram] [Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) {Z : C'} (h : (D.mapGlueData F).glued ⟶ Z) : CategoryStruct.comp (F.map (D.ι i)) (CategoryStruct.comp (D.gluedIso F).hom h) = CategoryStruct.comp ((D.mapGlueData F).ι i) h

@[simp]

theorem CategoryTheory.GlueData.ι_gluedIso_inv {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [Limits.HasMulticoequalizer D.diagram] [Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) : CategoryStruct.comp ((D.mapGlueData F).ι i) (D.gluedIso F).inv = F.map (D.ι i)

@[simp]

theorem CategoryTheory.GlueData.ι_gluedIso_inv_assoc {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [Limits.HasMulticoequalizer D.diagram] [Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) {Z : C'} (h : F.obj D.glued ⟶ Z) : CategoryStruct.comp ((D.mapGlueData F).ι i) (CategoryStruct.comp (D.gluedIso F).inv h) = CategoryStruct.comp (F.map (D.ι i)) h

def CategoryTheory.GlueData.vPullbackConeIsLimitOfMap {C : Type u₁} [Category.{v, u₁} C] {C' : Type u₂} [Category.{v, u₂} C'] (D : GlueData C) (F : Functor C C') [Limits.HasMulticoequalizer D.diagram] [Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), Limits.PreservesLimit (Limits.cospan (D.f i j) (D.f i k)) F] (i j : D.J) [Limits.ReflectsLimit (Limits.cospan (D.ι i) (D.ι j)) F] (hc : Limits.IsLimit ((D.mapGlueData F).vPullbackCone i j)) : 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.

theorem CategoryTheory.GlueData.ι_jointly_surjective {C : Type u₁} [Category.{v, u₁} C] (D : GlueData C) [Limits.HasMulticoequalizer D.diagram] (F : Functor C (Type v)) [Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), Limits.PreservesLimit (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₁) [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'

• J : Type v

  Indexing type of a glue data.

• U : self.J → C

  Objects of a glue data to be glued.

• V (i j : self.J) : i ≠ j → C

  Objects representing the intersections.

• f (i j : self.J) (h : i ≠ j) : self.V i j h ⟶ self.U i

  The inclusion maps of the intersection into the object.

• f_mono (i j : self.J) (h : i ≠ j) : Mono (self.f i j h)
• f_hasPullback (i j k : self.J) (hij : i ≠ j) (hik : i ≠ k) : Limits.HasPullback (self.f i j hij) (self.f i k hik)
• t (i j : self.J) (h : i ≠ j) : self.V i j h ⟶ self.V j i ⋯

  The transition maps between the intersections.

• t' (i j k : self.J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : Limits.pullback (self.f i j hij) (self.f i k hik) ⟶ Limits.pullback (self.f j k hjk) (self.f j i ⋯)

  The transition maps between the intersection of intersections.

• t_fac (i j k : self.J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : CategoryStruct.comp (self.t' i j k hij hik hjk) (Limits.pullback.snd (self.f j k hjk) (self.f j i ⋯)) = CategoryStruct.comp (Limits.pullback.fst (self.f i j hij) (self.f i k hik)) (self.t i j hij)
• t_inv (i j : self.J) (hij : i ≠ j) : CategoryStruct.comp (self.t i j hij) (self.t j i ⋯) = CategoryStruct.id (self.V i j hij)
• cocycle (i j k : self.J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : CategoryStruct.comp (self.t' i j k hij hik hjk) (CategoryStruct.comp (self.t' j k i hjk ⋯ ⋯) (self.t' k i j ⋯ ⋯ hij)) = CategoryStruct.id (Limits.pullback (self.f i j hij) (self.f i k hik))

@[simp]

theorem CategoryTheory.GlueData'.cocycle_assoc {C : Type u₁} [Category.{v, u₁} C] (self : GlueData' C) (i j k : self.J) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) {Z : C} (h : Limits.pullback (self.f i j hij) (self.f i k ⋯) ⟶ Z) : CategoryStruct.comp (self.t' i j k hij hik hjk) (CategoryStruct.comp (self.t' j k i hjk ⋯ ⋯) (CategoryStruct.comp (self.t' k i j ⋯ ⋯ hij) h)) = h

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.GlueData'.f' {C : Type u₁} [Category.{v, u₁} C] (D : GlueData' C) (i 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

• D.f' i j = if h : i = j then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (D.f i j h)

instance CategoryTheory.instMonoF' {C : Type u₁} [Category.{v, u₁} C] (D : GlueData' C) (i j : D.J) : Mono (D.f' i j)

instance CategoryTheory.instIsIsoF' {C : Type u₁} [Category.{v, u₁} C] (D : GlueData' C) (i : D.J) : IsIso (D.f' i i)

instance CategoryTheory.instHasPullbackF' {C : Type u₁} [Category.{v, u₁} C] (D : GlueData' C) (i j k : D.J) : Limits.HasPullback (D.f' i j) (D.f' i k)

def CategoryTheory.GlueData'.t'' {C : Type u₁} [Category.{v, u₁} C] (D : GlueData' C) (i j k : D.J) : Limits.pullback (D.f' i j) (D.f' i k) ⟶ 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.

def CategoryTheory.GlueData.ofGlueData' {C : Type u₁} [Category.{v, u₁} C] (D : GlueData' C) : GlueData C

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.