category_theory.glue_data

source

@[nolint]

structure category_theory.glue_data (C : Type u₁) [category_theory.category C] :

Type (max u₁ (v+1))

J : Type ?
U : self.J → C
V : self.J × self.J → C
f : Π (i j : self.J), self.V (i, j) ⟶ self.U i
f_mono : (∀ (i j : self.J), category_theory.mono (self.f i j)) . "apply_instance"
f_has_pullback : (∀ (i j k : self.J), category_theory.limits.has_pullback (self.f i j) (self.f i k)) . "apply_instance"
f_id : (∀ (i : self.J), category_theory.is_iso (self.f i i)) . "apply_instance"
t : Π (i j : self.J), self.V (i, j) ⟶ self.V (j, i)
t_id : ∀ (i : self.J), self.t i i = 𝟙 (self.V (i, i))
t' : Π (i j k : self.J), category_theory.limits.pullback (self.f i j) (self.f i k) ⟶ category_theory.limits.pullback (self.f j k) (self.f j i)
t_fac : ∀ (i j k : self.J), self.t' i j k ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.fst ≫ self.t i j
cocycle : ∀ (i j k : self.J), self.t' i j k ≫ self.t' j k i ≫ self.t' k i j = 𝟙 (category_theory.limits.pullback (self.f i j) (self.f i k))

A gluing datum consists of

An index type J
An object U i for each i : J.
An object V i j for each i j : J.
A monomorphism f i j : V i j ⟶ U i for each i j : J.
A transition map t i j : V i j ⟶ V j i for each i j : J. such that
f i i is an isomorphism.
t i i is the identity.
The pullback for f i j and f i k exists.
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.
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

source

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') :

self.t' i j k ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.fst ≫ self.t i j ≫ f'

source

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'

source

@[simp]

theorem category_theory.glue_data.t'_iij {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) :

D.t' i i j = (category_theory.limits.pullback_symmetry (D.f i i) (D.f i j)).hom

source

theorem category_theory.glue_data.t'_jii {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) :

D.t' j i i = category_theory.limits.pullback.fst ≫ D.t j i ≫ category_theory.inv category_theory.limits.pullback.snd

source

theorem category_theory.glue_data.t'_iji {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) :

D.t' i j i = category_theory.limits.pullback.fst ≫ D.t i j ≫ category_theory.inv category_theory.limits.pullback.snd

source

@[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

source

@[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))

source

@[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'

source

theorem category_theory.glue_data.t'_inv {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j k : D.J) :

D.t' i j k ≫ (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 = 𝟙 (category_theory.limits.pullback (D.f i j) (D.f i k))

source

@[protected, instance]

def category_theory.glue_data.t_is_iso {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) :

category_theory.is_iso (D.t i j)

source

@[protected, instance]

def category_theory.glue_data.t'_is_iso {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j k : D.J) :

category_theory.is_iso (D.t' i j k)

source

theorem category_theory.glue_data.t'_comp_eq_pullback_symmetry {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j k : D.J) :

D.t' j k i ≫ D.t' k i j = (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

source

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'

source

noncomputable def category_theory.glue_data.sigma_opens {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_coproduct D.U] :

C

(Implementation) The disjoint union of U i.

Equations

D.sigma_opens = ∐ D.U

source

def category_theory.glue_data.diagram {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) :

category_theory.limits.multispan_index C

(Implementation) The diagram to take colimit of.

Equations

D.diagram = {L := D.J × D.J, R := D.J, fst_from := prod.fst D.J, snd_from := prod.snd D.J, 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

source

@[simp]

theorem category_theory.glue_data.diagram_L {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) :

D.diagram.L = (D.J × D.J)

source

@[simp]

theorem category_theory.glue_data.diagram_R {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) :

D.diagram.R = D.J

source

@[simp]

theorem category_theory.glue_data.diagram_fst_from {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) :

D.diagram.fst_from (i, j) = i

source

@[simp]

theorem category_theory.glue_data.diagram_snd_from {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) (i j : D.J) :

D.diagram.snd_from (i, j) = j

source

@[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

source

@[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

source

@[simp]

theorem category_theory.glue_data.diagram_left {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) :

D.diagram.left = D.V

source

@[simp]

theorem category_theory.glue_data.diagram_right {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) :

D.diagram.right = D.U

source

noncomputable def category_theory.glue_data.glued {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_multicoequalizer D.diagram] :

C

The glued object given a family of gluing data.

Equations

D.glued = category_theory.limits.multicoequalizer D.diagram

source

noncomputable def category_theory.glue_data.ι {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_multicoequalizer D.diagram] (i : D.J) :

D.U i ⟶ D.glued

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

Equations

D.ι i = category_theory.limits.multicoequalizer.π D.diagram i

Instances for category_theory.glue_data.ι

source

@[simp]

theorem category_theory.glue_data.glue_condition {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_multicoequalizer D.diagram] (i j : D.J) :

D.t i j ≫ D.f j i ≫ D.ι j = D.f i j ≫ D.ι i

source

@[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)

source

noncomputable def category_theory.glue_data.V_pullback_cone {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_multicoequalizer D.diagram] (i j : D.J) :

category_theory.limits.pullback_cone (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.V_pullback_cone i j = category_theory.limits.pullback_cone.mk (D.f i j) (D.t i j ≫ D.f j i) _

source

noncomputable def category_theory.glue_data.π {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.has_colimits C] :

D.sigma_opens ⟶ D.glued

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

Equations

D.π = category_theory.limits.multicoequalizer.sigma_π D.diagram

Instances for category_theory.glue_data.π

category_theory.glue_data.π_epi

source

@[protected, instance]

def category_theory.glue_data.π_epi {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.has_colimits C] :

category_theory.epi D.π

source

theorem category_theory.glue_data.types_π_surjective (D : category_theory.glue_data (Type u_1)) :

function.surjective D.π

source

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

source

@[protected, instance]

def category_theory.glue_data.category_theory.functor.map.category_theory.limits.has_pullback {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) :

category_theory.limits.has_pullback (F.map (D.f i j)) (F.map (D.f i k))

source

@[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)

source

noncomputable def category_theory.glue_data.map_glue_data {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] :

category_theory.glue_data C'

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

Equations

D.map_glue_data F = {J := D.J, U := λ (i : D.J), F.obj (D.U i), V := λ (i : D.J × D.J), F.obj (D.V i), f := λ (i j : D.J), F.map (D.f i j), f_mono := _, f_has_pullback := _, f_id := _, t := λ (i j : D.J), F.map (D.t i j), t_id := _, t' := λ (i j k : D.J), (category_theory.limits.preserves_pullback.iso F (D.f i j) (D.f i k)).inv ≫ F.map (D.t' i j k) ≫ (category_theory.limits.preserves_pullback.iso F (D.f j k) (D.f j i)).hom, t_fac := _, cocycle := _}

source

@[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)

source

@[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) :

(D.map_glue_data F).t' i j k = (category_theory.limits.preserves_pullback.iso F (D.f i j) (D.f i k)).inv ≫ F.map (D.t' i j k) ≫ (category_theory.limits.preserves_pullback.iso F (D.f j k) (D.f j i)).hom

source

@[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)

source

@[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)

source

@[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

source

noncomputable def category_theory.glue_data.diagram_iso {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.diagram.multispan ⋙ F ≅ (D.map_glue_data F).diagram.multispan

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

D.diagram_iso F = category_theory.nat_iso.of_components (λ (x : category_theory.limits.walking_multispan D.diagram.fst_from D.diagram.snd_from), category_theory.glue_data.diagram_iso._match_1 D F x) _
category_theory.glue_data.diagram_iso._match_1 D F (category_theory.limits.walking_multispan.right b) = category_theory.iso.refl ((D.diagram.multispan ⋙ F).obj (category_theory.limits.walking_multispan.right b))
category_theory.glue_data.diagram_iso._match_1 D F (category_theory.limits.walking_multispan.left a) = category_theory.iso.refl ((D.diagram.multispan ⋙ F).obj (category_theory.limits.walking_multispan.left a))

source

@[simp]

theorem category_theory.glue_data.diagram_iso_app_left {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.diagram_iso F).app (category_theory.limits.walking_multispan.left i) = category_theory.iso.refl ((D.diagram.multispan ⋙ F).obj (category_theory.limits.walking_multispan.left i))

source

@[simp]

theorem category_theory.glue_data.diagram_iso_app_right {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.diagram_iso F).app (category_theory.limits.walking_multispan.right i) = category_theory.iso.refl ((D.diagram.multispan ⋙ F).obj (category_theory.limits.walking_multispan.right i))

source

@[simp]

theorem category_theory.glue_data.diagram_iso_hom_app_left {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.diagram_iso F).hom.app (category_theory.limits.walking_multispan.left i) = 𝟙 ((D.diagram.multispan ⋙ F).obj (category_theory.limits.walking_multispan.left i))

source

@[simp]

theorem category_theory.glue_data.diagram_iso_hom_app_right {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.diagram_iso F).hom.app (category_theory.limits.walking_multispan.right i) = 𝟙 ((D.diagram.multispan ⋙ F).obj (category_theory.limits.walking_multispan.right i))

source

@[simp]

theorem category_theory.glue_data.diagram_iso_inv_app_left {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.diagram_iso F).inv.app (category_theory.limits.walking_multispan.left i) = 𝟙 ((D.map_glue_data F).diagram.multispan.obj (category_theory.limits.walking_multispan.left i))

source

@[simp]

theorem category_theory.glue_data.diagram_iso_inv_app_right {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.diagram_iso F).inv.app (category_theory.limits.walking_multispan.right i) = 𝟙 ((D.map_glue_data F).diagram.multispan.obj (category_theory.limits.walking_multispan.right i))

source

theorem category_theory.glue_data.has_colimit_multispan_comp {C : Type u₁} [category_theory.category C] {C' : Type u₂} [category_theory.category C'] (D : category_theory.glue_data C) (F : C ⥤ C') [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.preserves_colimit D.diagram.multispan F] :

category_theory.limits.has_colimit (D.diagram.multispan ⋙ F)

source

theorem category_theory.glue_data.has_colimit_map_glue_data_diagram {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] [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.preserves_colimit D.diagram.multispan F] :

category_theory.limits.has_multicoequalizer (D.map_glue_data F).diagram

source

noncomputable def category_theory.glue_data.glued_iso {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] [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.preserves_colimit D.diagram.multispan F] :

F.obj D.glued ≅ (D.map_glue_data F).glued

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

Equations

D.glued_iso F = category_theory.preserves_colimit_iso F D.diagram.multispan ≪≫ category_theory.limits.has_colimit.iso_of_nat_iso (D.diagram_iso F)

source

@[simp]

theorem category_theory.glue_data.ι_glued_iso_hom {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] [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.preserves_colimit D.diagram.multispan F] (i : D.J) :

F.map (D.ι i) ≫ (D.glued_iso F).hom = (D.map_glue_data F).ι i

source

@[simp]

theorem category_theory.glue_data.ι_glued_iso_hom_assoc {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] [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.preserves_colimit D.diagram.multispan 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'

source

@[simp]

theorem category_theory.glue_data.ι_glued_iso_inv {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] [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.preserves_colimit D.diagram.multispan F] (i : D.J) :

(D.map_glue_data F).ι i ≫ (D.glued_iso F).inv = F.map (D.ι i)

source

@[simp]

theorem category_theory.glue_data.ι_glued_iso_inv_assoc {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] [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.preserves_colimit D.diagram.multispan 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'

source

noncomputable def category_theory.glue_data.V_pullback_cone_is_limit_of_map {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] [category_theory.limits.has_multicoequalizer D.diagram] [category_theory.limits.preserves_colimit D.diagram.multispan F] (i j : D.J) [category_theory.limits.reflects_limit (category_theory.limits.cospan (D.ι i) (D.ι j)) F] (hc : category_theory.limits.is_limit ((D.map_glue_data F).V_pullback_cone i j)) :

category_theory.limits.is_limit (D.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

D.V_pullback_cone_is_limit_of_map F i j hc = category_theory.limits.is_limit_of_reflects F (⇑((category_theory.limits.is_limit_map_cone_pullback_cone_equiv F _).symm) (let e : category_theory.limits.cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ category_theory.limits.cospan ((D.map_glue_data F).ι i) ((D.map_glue_data F).ι j) := category_theory.nat_iso.of_components (λ (x : category_theory.limits.walking_cospan), option.cases_on x (D.glued_iso F) (λ (x : category_theory.limits.walking_pair), category_theory.iso.refl ((category_theory.limits.cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (option.some x)))) _ in ⇑(category_theory.limits.is_limit.postcompose_hom_equiv e (category_theory.limits.pullback_cone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) _)) (hc.of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((D.map_glue_data F).V_pullback_cone i j).X) _))))

source

theorem category_theory.glue_data.ι_jointly_surjective {C : Type u₁} [category_theory.category C] (D : category_theory.glue_data C) [category_theory.limits.has_multicoequalizer D.diagram] (F : C ⥤ Type v) [category_theory.limits.preserves_colimit D.diagram.multispan F] [Π (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.

mathlib3 documentation

Gluing data #