Commit 2025-08-11 11:23 06586024

View on Github →

feat(AlgebraicTopology): path objects in model categories (#26958) This PR dualizes #26171 which was about cylinder objects.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/ModelCategory/IsCofibrant.lean

Created Mathlib/AlgebraicTopology/ModelCategory/PathObject.lean

added theorem HomotopicalAlgebra.PathObject.exists_very_good

added theorem HomotopicalAlgebra.PathObject.ofFactorizationData_p

added def HomotopicalAlgebra.PathObject.symm

added theorem HomotopicalAlgebra.PathObject.symm_p

added structure HomotopicalAlgebra.PathObject

added theorem HomotopicalAlgebra.PrepathObject.p_fst

added theorem HomotopicalAlgebra.PrepathObject.p_snd

added def HomotopicalAlgebra.PrepathObject.symm

added theorem HomotopicalAlgebra.PrepathObject.symm_p

added structure HomotopicalAlgebra.PrepathObject

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

added theorem CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal

added theorem CategoryTheory.IsPullback.of_prod_fst_with_id