mathlib3 documentation

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₁) [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]
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]

(Implementation) The disjoint union of U i.

Equations

(Implementation) The diagram to take colimit of.

Equations
@[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
@[simp]

The pullback cone spanned by V i j ⟶ U i and V i j ⟶ U j. This will often be a pullback diagram.

Equations
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_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)

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.