Commit 2025-02-15 11:19 2e68c4ec

View on Github →

feat(CategoryTheory): various properties of transfinite compositions (#21843) Some more basic API for transfinite compositions and relative cell complexes is added. It is also shown that isomorphisms are stable under transfinite compositions. After this, it will be possible to start proving the main results of the small object argument.

Estimated changes

Modified Mathlib/AlgebraicTopology/RelativeCellComplex/AttachCells.lean

added def HomotopicalAlgebra.AttachCells.ofArrowIso

added def HomotopicalAlgebra.AttachCells.reindex

Modified Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean

added def HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape

Modified Mathlib/CategoryTheory/Limits/Shapes/Preorder/HasIterationOfShape.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Preorder/TransfiniteCompositionOfShape.lean

added def CategoryTheory.TransfiniteCompositionOfShape.iic

Modified Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

added def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.iic

added theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.isIso

added theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_map_of_preserves