Attaching cells

Given a family of morphisms g a : A a ⟶ B a and a morphism f : X₁ ⟶ X₂, we introduce a structure AttachCells g f which expresses that X₂ is obtained from X₁ by attaching cells of the form g a. It means that there is a pushout diagram of the form

⨿ i, A (π i) -----> X₁
  |                 |f
  v                 v
⨿ i, B (π i) -----> X₂

In other words, the morphism f is a pushout of coproducts of morphisms of the form g a : A a ⟶ B a, see nonempty_attachCells_iff.

See the file Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean for transfinite compositions of morphisms f with AttachCells g f structures.

structure HomotopicalAlgebra.AttachCells {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} (g : (a : α) → A a ⟶ B a) {X₁ X₂ : C} (f : X₁ ⟶ X₂) : Type (max (max (max t u) v) (w + 1))

Given a family of morphisms g a : A a ⟶ B a and a morphism f : X₁ ⟶ X₂, this structure contains the data and properties which expresses that X₂ is obtained from X₁ by attaching cells of the form g a.

• ι : Type w

  the index type of the cells

• π : self.ι → α

  for each i : ι, we shall attach a cell given by the morphism g (π i).

• cofan₁ : CategoryTheory.Limits.Cofan fun (i : self.ι) => A (self.π i)

  a colimit cofan which gives the coproduct of the object A (π i)

• cofan₂ : CategoryTheory.Limits.Cofan fun (i : self.ι) => B (self.π i)

  a colimit cofan which gives the coproduct of the object B (π i)

• isColimit₁ : CategoryTheory.Limits.IsColimit self.cofan₁

  cofan₁ is colimit

• isColimit₂ : CategoryTheory.Limits.IsColimit self.cofan₂

  cofan₂ is colimit

• m : self.cofan₁.pt ⟶ self.cofan₂.pt

  the coproduct of the maps g (π i) : A (π i) ⟶ B (π i) for all i : ι.

• hm (i : self.ι) : CategoryTheory.CategoryStruct.comp (self.cofan₁.inj i) self.m = CategoryTheory.CategoryStruct.comp (g (self.π i)) (self.cofan₂.inj i)
• g₁ : self.cofan₁.pt ⟶ X₁

  the top morphism of the pushout square

• g₂ : self.cofan₂.pt ⟶ X₂

  the bottom morphism of the pushout square

• isPushout : CategoryTheory.IsPushout self.g₁ self.m f self.g₂

@[simp]

theorem HomotopicalAlgebra.AttachCells.hm_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (self : AttachCells g f) (i : self.ι) {Z : C} (h : self.cofan₂.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.cofan₁.inj i) (CategoryTheory.CategoryStruct.comp self.m h) = CategoryTheory.CategoryStruct.comp (g (self.π i)) (CategoryTheory.CategoryStruct.comp (self.cofan₂.inj i) h)

theorem HomotopicalAlgebra.AttachCells.pushouts_coproducts {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) : (CategoryTheory.MorphismProperty.coproducts.{w, v, u} (CategoryTheory.MorphismProperty.ofHoms g)).pushouts f

def HomotopicalAlgebra.AttachCells.cell {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) (i : c.ι) : B (c.π i) ⟶ X₂

The inclusion of a cell.

theorem HomotopicalAlgebra.AttachCells.cell_def {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) (i : c.ι) : c.cell i = CategoryTheory.CategoryStruct.comp (c.cofan₂.inj i) c.g₂

theorem HomotopicalAlgebra.AttachCells.cell_def_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) (i : c.ι) {Z : C} (h : X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.cell i) h = CategoryTheory.CategoryStruct.comp (c.cofan₂.inj i) (CategoryTheory.CategoryStruct.comp c.g₂ h)

theorem HomotopicalAlgebra.AttachCells.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Z : C} {φ φ' : X₂ ⟶ Z} (h₀ : CategoryTheory.CategoryStruct.comp f φ = CategoryTheory.CategoryStruct.comp f φ') (h : ∀ (i : c.ι), CategoryTheory.CategoryStruct.comp (c.cell i) φ = CategoryTheory.CategoryStruct.comp (c.cell i) φ') : φ = φ'

def HomotopicalAlgebra.AttachCells.ofArrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : AttachCells g f'

If f and f' are isomorphic morphisms and the target of f is obtained by attaching cells to the source of f, then the same holds for f'.

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_m {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).m = c.m

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_cofan₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).cofan₁ = c.cofan₁

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).ι = c.ι

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_isColimit₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).isColimit₂ = c.isColimit₂

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_isColimit₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).isColimit₁ = c.isColimit₁

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_g₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).g₂ = CategoryTheory.CategoryStruct.comp c.g₂ (CategoryTheory.Arrow.rightFunc.map e.hom)

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_cofan₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).cofan₂ = c.cofan₂

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_g₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (c.ofArrowIso e).g₁ = CategoryTheory.CategoryStruct.comp c.g₁ (CategoryTheory.Arrow.leftFunc.map e.hom)

@[simp]

theorem HomotopicalAlgebra.AttachCells.ofArrowIso_π {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') (a✝ : c.ι) : (c.ofArrowIso e).π a✝ = c.π a✝

def HomotopicalAlgebra.AttachCells.reindex {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : AttachCells g f

This definition allows the replacement of the ι field of a AttachCells g f structure by an equivalent type.

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).ι = ι'

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_isColimit₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).isColimit₁ = c.isColimit₁.whiskerEquivalence (CategoryTheory.Discrete.equivalence e)

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_cofan₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).cofan₁ = CategoryTheory.Limits.Cofan.mk c.cofan₁.pt fun (i' : ι') => c.cofan₁.inj (e i')

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_g₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).g₂ = c.g₂

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_isColimit₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).isColimit₂ = c.isColimit₂.whiskerEquivalence (CategoryTheory.Discrete.equivalence e)

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_m {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).m = c.m

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_g₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).g₁ = c.g₁

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_cofan₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) : (c.reindex e).cofan₂ = CategoryTheory.Limits.Cofan.mk c.cofan₂.pt fun (i' : ι') => c.cofan₂.inj (e i')

@[simp]

theorem HomotopicalAlgebra.AttachCells.reindex_π {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) (i' : ι') : (c.reindex e).π i' = c.π (e i')

def HomotopicalAlgebra.AttachCells.reindexCellTypes {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a} {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : AttachCells g f) {α' : Type t'} {A' B' : α' → C} (g' : (i' : α') → A' i' ⟶ B' i') (a : α → α') (ha : (i : α) → CategoryTheory.Arrow.mk (g i) ≅ CategoryTheory.Arrow.mk (g' (a i))) : AttachCells g' f

If a family of maps g is contained in another family g' (up to isomorphisms), if f : X₁ ⟶ X₂ is a morphism, and X₂ is obtained from X₁ by attaching cells of the form g, then it is also obtained by attaching cells of the form g'.

theorem HomotopicalAlgebra.nonempty_attachCells_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} (g : (a : α) → A a ⟶ B a) {X₁ X₂ : C} (f : X₁ ⟶ X₂) : Nonempty (AttachCells g f) ↔ (CategoryTheory.MorphismProperty.coproducts.{w, v, u} (CategoryTheory.MorphismProperty.ofHoms g)).pushouts f