Relative cell complexes

In this file, we define a structure RelativeCellComplex which expresses that a morphism f : X ⟶ Y is a transfinite composition of morphisms, all of which consists in attaching cells. Here, we allow a different family of authorized cells at each step. For example, (relative) CW-complexes are defined in the file Mathlib/Topology/CWComplex/Abstract/Basic.lean by requiring that at the nth step, we attach n-disks along their boundaries.

This structure RelativeCellComplex is also used in the formalization of the small object argument, see the file Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean.

References

• https://ncatlab.org/nlab/show/small+object+argument

structure HomotopicalAlgebra.RelativeCellComplex {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C} (basicCell : (j : J) → (i : α j) → A j i ⟶ B j i) {X Y : C} (f : X ⟶ Y) extends CategoryTheory.TransfiniteCompositionOfShape J f : Type (max (max (max (max t u) v) (w + 1)) w')

Let J be a well ordered type. Assume that for each j : J, we have a family basicCell j of morphisms. A relative cell complex is a morphism f : X ⟶ Y which is a transfinite composition of morphisms in such a way that at the step j : J, we attach cells in the family basicCell j.

• F : Functor J C
• isoBot : self.F.obj ⊥ ≅ X
• isWellOrderContinuous : self.F.IsWellOrderContinuous
• incl : self.F ⟶ (Functor.const J).obj Y
• isColimit : Limits.IsColimit { pt := Y, ι := self.incl }
• fac : CategoryStruct.comp self.isoBot.inv (self.incl.app ⊥) = f
• attachCells (j : J) (hj : ¬IsMax j) : AttachCells (basicCell j) (self.F.map (CategoryTheory.homOfLE ⋯))

  If j is not the maximum element, F.obj (Order.succ j) is obtained from F.obj j by attaching cells in the family of morphisms basicCell j.

structure HomotopicalAlgebra.RelativeCellComplex.Cells {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C} {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y} (c : RelativeCellComplex basicCell f) : Type (max u_1 w')

The index type of cells in a relative cell complex.

• j : J

  the step where the cell is added

• hj : ¬IsMax self.j
• k : (c.attachCells self.j ⋯).ι

  the index of the cell

def HomotopicalAlgebra.RelativeCellComplex.Cells.i {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C} {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y} {c : RelativeCellComplex basicCell f} (γ : c.Cells) : α γ.j

Given a cell γ in a relative cell complex, this is the corresponding index in the family of morphisms basicCell γ.j.

Equations

• γ.i = (c.attachCells γ.j ⋯).π γ.k

def HomotopicalAlgebra.RelativeCellComplex.Cells.ι {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C} {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y} {c : RelativeCellComplex basicCell f} (γ : c.Cells) : B γ.j γ.i ⟶ Y

The inclusion of a cell.

Equations

• γ.ι = CategoryTheory.CategoryStruct.comp ((c.attachCells γ.j ⋯).cell γ.k) (c.incl.app (Order.succ γ.j))

theorem HomotopicalAlgebra.RelativeCellComplex.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C} {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y} (c : RelativeCellComplex basicCell f) {Z : C} {φ₁ φ₂ : Y ⟶ Z} (h₀ : CategoryTheory.CategoryStruct.comp f φ₁ = CategoryTheory.CategoryStruct.comp f φ₂) (h : ∀ (γ : c.Cells), CategoryTheory.CategoryStruct.comp γ.ι φ₁ = CategoryTheory.CategoryStruct.comp γ.ι φ₂) : φ₁ = φ₂

def HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} {α : Type u_1} {A B : α → C} (g : (i : α) → A i ⟶ B i) (c : RelativeCellComplex (fun (x : J) => g) f) : (CategoryTheory.MorphismProperty.coproducts.{w, v, u} (CategoryTheory.MorphismProperty.ofHoms g)).pushouts.TransfiniteCompositionOfShape J f

If f is a relative cell complex with respect to a constant family of morphisms g, then f is a transfinite composition of pushouts of coproducts of morphisms in the family g.

Equations

• HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape g c = { toTransfiniteCompositionOfShape := c.toTransfiniteCompositionOfShape, map_mem := ⋯ }

@[simp]

theorem HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape_toTransfiniteCompositionOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} {α : Type u_1} {A B : α → C} (g : (i : α) → A i ⟶ B i) (c : RelativeCellComplex (fun (x : J) => g) f) : (transfiniteCompositionOfShape g c).toTransfiniteCompositionOfShape = c.toTransfiniteCompositionOfShape