The mapping cone of a homotopy equivalence is contractible #
A morphism of cochain complexes f : K ⟶ L sits in the distinguished triangle
K ⟶ L ⟶ cone f ⟶ K⟦1⟧ of the homotopy category. In a pretriangulated category the third
object of a distinguished triangle is zero exactly when its first morphism is an isomorphism, so
the mapping cone of f is zero in the homotopy category as soon as f becomes an isomorphism
there, in particular when f is a homotopy equivalence. Being zero in the homotopy category means
that the identity is null-homotopic, which is the form in which this file records the statement.
Main results #
CochainComplex.mappingCone.nonempty_homotopy_id_zero_of_isIso_quotient_map: the mapping cone of a morphism inverted by the homotopy category is contractible.CochainComplex.mappingCone.nonempty_homotopy_id_zero_of_homotopyEquiv: the mapping cone of a homotopy equivalence is contractible.
theorem
CochainComplex.mappingCone.nonempty_homotopy_id_zero_of_isIso_quotient_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(f : K ⟶ L)
[CategoryTheory.IsIso ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f)]
:
The mapping cone of a morphism which becomes an isomorphism in the homotopy category is contractible.
theorem
CochainComplex.mappingCone.nonempty_homotopy_id_zero_of_homotopyEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(e : HomotopyEquiv K L)
:
The mapping cone of a homotopy equivalence is contractible.