Commit 2025-07-15 08:10 d0f1801b

View on Github →

feat(AlgebraicTopology): cylinder objects in model categories (#26171) We introduce a notion of (pre)cylinder for an object A : C in a model category. It consists of an object I, a weak equivalence π : I ⟶ A equipped with two sections i₀ and i₁. This notion shall be important in the definition of "left homotopies" in model categories.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/ModelCategory/Cylinder.lean

added theorem HomotopicalAlgebra.Cylinder.exists_very_good

added theorem HomotopicalAlgebra.Cylinder.ofFactorizationData_i

added def HomotopicalAlgebra.Cylinder.symm

added theorem HomotopicalAlgebra.Cylinder.symm_i

added structure HomotopicalAlgebra.Cylinder

added theorem HomotopicalAlgebra.Precylinder.inl_i

added theorem HomotopicalAlgebra.Precylinder.inr_i

added def HomotopicalAlgebra.Precylinder.symm

added theorem HomotopicalAlgebra.Precylinder.symm_i

added structure HomotopicalAlgebra.Precylinder

Modified Mathlib/AlgebraicTopology/ModelCategory/Instances.lean

Modified Mathlib/AlgebraicTopology/ModelCategory/IsCofibrant.lean

added theorem HomotopicalAlgebra.isCofibrant_of_cofibration

added theorem HomotopicalAlgebra.isFibrant_of_fibration

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

added theorem CategoryTheory.IsPushout.of_coprod_inl_with_id

added theorem CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial