Commit 2025-02-12 13:36 40649a93

View on Github →

feat(AlgebraicTopology): relative cell complexes, refactor of CW-complexes (#21600) A structure RelativeCellComplex is introduced. It is used here in order to refactor the definition of CW-complexes. It shall also be used in the formalization of the small object argument.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/RelativeCellComplex/AttachCells.lean

Created Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean

added def HomotopicalAlgebra.RelativeCellComplex.Cells.i

added def HomotopicalAlgebra.RelativeCellComplex.Cells.ι

added structure HomotopicalAlgebra.RelativeCellComplex.Cells

added theorem HomotopicalAlgebra.RelativeCellComplex.hom_ext

added structure HomotopicalAlgebra.RelativeCellComplex

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

Modified Mathlib/Topology/CWComplex/Abstract/Basic.lean

deleted structure CategoryTheory.CWComplex

deleted def CategoryTheory.RelativeCWComplex.AttachCells

deleted def CategoryTheory.RelativeCWComplex.AttachGeneralizedCells.inclusion

deleted structure CategoryTheory.RelativeCWComplex.AttachGeneralizedCells

deleted def CategoryTheory.RelativeCWComplex.skInclusion

deleted def CategoryTheory.RelativeCWComplex.sphereInclusion

deleted def CategoryTheory.RelativeCWComplex.toTopCat

deleted structure CategoryTheory.RelativeCWComplex

Modified Mathlib/Topology/Category/TopCat/Sphere.lean

added def TopCat.diskBoundaryInclusion