Commit 2024-01-06 15:29 5dcfd144

View on Github →

feat(Algebra/Homology): the cylinder of a homological complex (#9483) In this PR, the cylinder object of a homological complex is constructed. It is used to show that a functor which inverts homotopy equivalences sends homotopic maps to the same map. In the future, it shall be used in order to show that homotopic maps become equal in the derived category.

Estimated changes

Modified Mathlib/Algebra/Homology/HomotopyCofiber.lean

added theorem HomologicalComplex.cylinder.inlX_π

added theorem HomologicalComplex.cylinder.inrX_π

added theorem HomologicalComplex.cylinder.map_ι₀_eq_map_ι₁

added theorem HomologicalComplex.cylinder.ι₀_desc

added theorem HomologicalComplex.cylinder.ι₀_π

added theorem HomologicalComplex.cylinder.ι₁_desc

added theorem HomologicalComplex.cylinder.ι₁_π

added theorem HomologicalComplex.cylinder.πCompι₀Homotopy.biprod_lift_id_sub_id

added theorem HomologicalComplex.cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f

added theorem HomologicalComplex.cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f

added theorem HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap_eq

added theorem Homotopy.map_eq_of_inverts_homotopyEquivalences