mathlib documentation

category_theory.glue_data

Gluing data #

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₁) [category_theory.category 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 category_theory.glue_data
  • category_theory.glue_data.has_sizeof_inst
theorem category_theory.glue_data.t_fac_assoc {C : Type u₁} [category_theory.category C] (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₁} [category_theory.category C] (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]
@[simp]
theorem category_theory.glue_data.t_inv_apply {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) [I : category_theory.concrete_category C] (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₁} [category_theory.category C] (D : category_theory.glue_data C) (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₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) {X' : C} (f' : D.V (i, j) X') :
D.t i j D.t j i f' = f'
@[protected, instance]
@[protected, instance]
theorem category_theory.glue_data.t'_comp_eq_pullback_symmetry_assoc {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (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' = (category_theory.limits.pullback_symmetry (D.f j k) (D.f j i)).hom D.t' j i k (category_theory.limits.pullback_symmetry (D.f i k) (D.f i j)).hom f'

(Implementation) The disjoint union of U i.

Equations

(Implementation) The diagram to take colimit of.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.glue_data.diagram_fst {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) :
D.diagram.fst (i, j) = D.f i j
@[simp]
theorem category_theory.glue_data.diagram_snd {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) :
D.diagram.snd (i, j) = D.t i j D.f j i

The glued object given a family of gluing data.

Equations
@[simp]
theorem category_theory.glue_data.glue_condition_apply {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_multicoequalizer D.diagram] (i j : D.J) [I : category_theory.concrete_category C] (x : (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

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

Equations
Instances for category_theory.glue_data.π
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
@[simp]
theorem category_theory.glue_data.map_glue_data_V {C : Type u₁} [category_theory.category C] {C' : Type u₂} [category_theory.category C'] (D : category_theory.glue_data C) (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)

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₁} [category_theory.category C] {C' : Type u₂} [category_theory.category C'] (D : category_theory.glue_data C) (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₁} [category_theory.category C] {C' : Type u₂} [category_theory.category C'] (D : category_theory.glue_data C) (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) :
@[simp]
theorem category_theory.glue_data.map_glue_data_U {C : Type u₁} [category_theory.category C] {C' : Type u₂} [category_theory.category C'] (D : category_theory.glue_data C) (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₁} [category_theory.category C] {C' : Type u₂} [category_theory.category C'] (D : category_theory.glue_data C) (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₁} [category_theory.category C] {C' : Type u₂} [category_theory.category C'] (D : category_theory.glue_data C) (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

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

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

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