The contraction of the alternating constant complex in degree zero

Mathlib's ChainComplex.alternatingConstHomotopyEquiv contracts the alternating constant complex on X onto X placed in degree zero. This module records its degree-zero component (ChainComplex.alternatingConstHomotopyEquiv_hom_f_zero): the identification of the two degree-zero terms, both of which are X.

@[simp]

theorem ChainComplex.alternatingConstHomotopyEquiv_hom_f_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) : (alternatingConstHomotopyEquiv X).hom.f 0 = (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X).inv

In degree zero, the contraction of the alternating constant complex is the identification of its degree-zero term with that of the single complex.