Attaching no cells

An isomorphism f : X₁ ⟶ X₂ is obtained by attaching an empty family of cells (HomotopicalAlgebra.AttachCells.ofIsIso): the pushout of the identity of an initial object along any morphism is an isomorphism. This fills the stages of a relative cell complex at which nothing is attached, for instance when all cells are attached at a single stage.

References

• R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990.

noncomputable def HomotopicalAlgebra.AttachCells.ofIsIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{w + 1}) C] {α : Type u_1} {A B : α → C} (g : (a : α) → A a ⟶ B a) {X₁ X₂ : C} (f : X₁ ⟶ X₂) [CategoryTheory.IsIso f] : AttachCells g f

An isomorphism is obtained by attaching no cells.

instance HomotopicalAlgebra.AttachCells.instIsEmptyιOfIsIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{w + 1}) C] {α : Type u_1} {A B : α → C} (g : (a : α) → A a ⟶ B a) {X₁ X₂ : C} (f : X₁ ⟶ X₂) [CategoryTheory.IsIso f] : IsEmpty (ofIsIso g f).ι

No cells are attached in AttachCells.ofIsIso.