# mathlib3documentation

category_theory.glue_data

# Gluing data #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define glue_data 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.

@[nolint]
structure category_theory.glue_data (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 category_theory.glue_data
• category_theory.glue_data.has_sizeof_inst
theorem category_theory.glue_data.t_fac_assoc {C : Type u₁} (self : category_theory.glue_data C) (i j k : self.J) {X' : C} (f' : self.V (j, i) X') :
theorem category_theory.glue_data.cocycle_assoc {C : Type u₁} (self : category_theory.glue_data C) (i j k : self.J) {X' : C} (f' : category_theory.limits.pullback (self.f i j) (self.f i k) X') :
self.t' i j k self.t' j k i self.t' k i j f' = f'
@[simp]
theorem category_theory.glue_data.t'_iij {C : Type u₁} (i j : D.J) :
D.t' i i j = (D.f i j)).hom
theorem category_theory.glue_data.t'_jii {C : Type u₁} (i j : D.J) :
theorem category_theory.glue_data.t'_iji {C : Type u₁} (i j : D.J) :
@[simp]
theorem category_theory.glue_data.t_inv_apply {C : Type u₁} (i j : D.J) (x : (D.V (i, j))) :
(D.t j i) ((D.t i j) x) = x
@[simp]
theorem category_theory.glue_data.t_inv {C : Type u₁} (i j : D.J) :
D.t i j D.t j i = 𝟙 (D.V (i, j))
@[simp]
theorem category_theory.glue_data.t_inv_assoc {C : Type u₁} (i j : D.J) {X' : C} (f' : D.V (i, j) X') :
D.t i j D.t j i f' = f'
theorem category_theory.glue_data.t'_inv {C : Type u₁} (i j k : D.J) :
D.t' i j k (D.f j i)).hom D.t' j i k (D.f i j)).hom = 𝟙 (category_theory.limits.pullback (D.f i j) (D.f i k))
@[protected, instance]
def category_theory.glue_data.t_is_iso {C : Type u₁} (i j : D.J) :
@[protected, instance]
def category_theory.glue_data.t'_is_iso {C : Type u₁} (i j k : D.J) :
theorem category_theory.glue_data.t'_comp_eq_pullback_symmetry {C : Type u₁} (i j k : D.J) :
D.t' j k i D.t' k i j = (D.f j i)).hom D.t' j i k (D.f i j)).hom
theorem category_theory.glue_data.t'_comp_eq_pullback_symmetry_assoc {C : Type u₁} (i j k : D.J) {X' : C} (f' : category_theory.limits.pullback (D.f i j) (D.f i k) X') :
D.t' j k i D.t' k i j f' = (D.f j i)).hom D.t' j i k (D.f i j)).hom f'
noncomputable def category_theory.glue_data.sigma_opens {C : Type u₁}  :
C

(Implementation) The disjoint union of U i.

Equations

(Implementation) The diagram to take colimit of.

Equations
• D.diagram = {L := D.J × D.J, R := D.J, fst_from := , snd_from := , left := D.V, right := D.U, fst := λ (_x : D.J × D.J), category_theory.glue_data.diagram._match_1 D _x, snd := λ (_x : D.J × D.J), category_theory.glue_data.diagram._match_2 D _x}
• category_theory.glue_data.diagram._match_1 D (i, j) = D.f i j
• category_theory.glue_data.diagram._match_2 D (i, j) = D.t i j D.f j i
@[simp]
theorem category_theory.glue_data.diagram_L {C : Type u₁}  :
D.diagram.L = (D.J × D.J)
@[simp]
theorem category_theory.glue_data.diagram_R {C : Type u₁}  :
D.diagram.R = D.J
@[simp]
theorem category_theory.glue_data.diagram_fst_from {C : Type u₁} (i j : D.J) :
D.diagram.fst_from (i, j) = i
@[simp]
theorem category_theory.glue_data.diagram_snd_from {C : Type u₁} (i j : D.J) :
D.diagram.snd_from (i, j) = j
@[simp]
theorem category_theory.glue_data.diagram_fst {C : Type u₁} (i j : D.J) :
D.diagram.fst (i, j) = D.f i j
@[simp]
theorem category_theory.glue_data.diagram_snd {C : Type u₁} (i j : D.J) :
D.diagram.snd (i, j) = D.t i j D.f j i
@[simp]
@[simp]
noncomputable def category_theory.glue_data.glued {C : Type u₁}  :
C

The glued object given a family of gluing data.

Equations
noncomputable def category_theory.glue_data.ι {C : Type u₁} (i : D.J) :
D.U i D.glued

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

Equations
Instances for category_theory.glue_data.ι
@[simp]
theorem category_theory.glue_data.glue_condition {C : Type u₁} (i j : D.J) :
D.t i j D.f j i D.ι j = D.f i j D.ι i
@[simp]
theorem category_theory.glue_data.glue_condition_apply {C : Type u₁} (i j : D.J) (x : (D.V (i, j))) :
(D.ι j) ((D.f j i) ((D.t i j) x)) = (D.ι i) ((D.f i j) x)
noncomputable def category_theory.glue_data.V_pullback_cone {C : Type u₁} (i j : D.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
noncomputable def category_theory.glue_data.π {C : Type u₁}  :

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

Equations
Instances for category_theory.glue_data.π
@[protected, instance]
theorem category_theory.glue_data.types_ι_jointly_surjective (D : category_theory.glue_data (Type u_1)) (x : D.glued) :
(i : D.J) (y : D.U i), D.ι i y = x
@[protected, instance]
@[simp]
theorem category_theory.glue_data.map_glue_data_V {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) :
(D.map_glue_data F).V i = F.obj (D.V i)
noncomputable def category_theory.glue_data.map_glue_data {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.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
@[simp]
theorem category_theory.glue_data.map_glue_data_f {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i j : D.J) :
(D.map_glue_data F).f i j = F.map (D.f i j)
@[simp]
theorem category_theory.glue_data.map_glue_data_t' {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i j k : D.J) :
(D.map_glue_data F).t' i j k = (D.f i k)).inv F.map (D.t' i j k) (D.f j i)).hom
@[simp]
theorem category_theory.glue_data.map_glue_data_U {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) :
(D.map_glue_data F).U i = F.obj (D.U i)
@[simp]
theorem category_theory.glue_data.map_glue_data_t {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i j : D.J) :
(D.map_glue_data F).t i j = F.map (D.t i j)
@[simp]
theorem category_theory.glue_data.map_glue_data_J {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] :
(D.map_glue_data F).J = D.J
noncomputable def category_theory.glue_data.diagram_iso {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] :

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

Equations
@[simp]
theorem category_theory.glue_data.diagram_iso_app_left {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) :
@[simp]
theorem category_theory.glue_data.diagram_iso_app_right {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) :
@[simp]
theorem category_theory.glue_data.diagram_iso_hom_app_left {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) :
@[simp]
theorem category_theory.glue_data.diagram_iso_hom_app_right {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) :
@[simp]
theorem category_theory.glue_data.diagram_iso_inv_app_left {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J × D.J) :
@[simp]
theorem category_theory.glue_data.diagram_iso_inv_app_right {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) :
theorem category_theory.glue_data.has_colimit_multispan_comp {C : Type u₁} {C' : Type u₂} (F : C C')  :
noncomputable def category_theory.glue_data.glued_iso {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F]  :

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

Equations
@[simp]
theorem category_theory.glue_data.ι_glued_iso_hom {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) :
F.map (D.ι i) (D.glued_iso F).hom = (D.map_glue_data F).ι i
@[simp]
theorem category_theory.glue_data.ι_glued_iso_hom_assoc {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) {X' : C'} (f' : (D.map_glue_data F).glued X') :
F.map (D.ι i) (D.glued_iso F).hom f' = (D.map_glue_data F).ι i f'
@[simp]
theorem category_theory.glue_data.ι_glued_iso_inv {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) :
(D.map_glue_data F).ι i (D.glued_iso F).inv = F.map (D.ι i)
@[simp]
theorem category_theory.glue_data.ι_glued_iso_inv_assoc {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) {X' : C'} (f' : F.obj D.glued X') :
(D.map_glue_data F).ι i (D.glued_iso F).inv f' = F.map (D.ι i) f'
noncomputable def category_theory.glue_data.V_pullback_cone_is_limit_of_map {C : Type u₁} {C' : Type u₂} (F : C C') [H : Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.limits.cospan (D.f i j) (D.f i k)) F] (i j : D.J) [ F] (hc : category_theory.limits.is_limit ((D.map_glue_data F).V_pullback_cone 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
theorem category_theory.glue_data.ι_jointly_surjective {C : Type u₁} (F : C Type v) [Π (i j k : D.J), category_theory.limits.preserves_limit (category_theory.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.