# Documentation

Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

# The normalized Moore complex and the alternating face map complex are homotopy equivalent #

In this file, when the category A is abelian, we obtain the homotopy equivalence homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex between the normalized Moore complex and the alternating face map complex of a simplicial object in A.

noncomputable def AlgebraicTopology.DoldKan.homotopyPToId {C : Type u_1} [] (q : ) :

Inductive construction of homotopies from P q to 𝟙 _

Equations
• One or more equations did not get rendered due to their size.
Instances For

The complement projection Q q to P q is homotopic to zero.

Instances For
theorem AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant {C : Type u_1} [] {q : } {n : } (hqn : n < q) :
Homotopy.hom () n (n + 1) = Homotopy.hom () n (n + 1)
@[simp]
def AlgebraicTopology.DoldKan.homotopyPInftyToId {C : Type u_1} [] :
Homotopy AlgebraicTopology.DoldKan.PInfty ()

Construction of the homotopy from PInfty to the identity using eventually (termwise) constant homotopies from P q to the identity for all q

Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom {A : Type u_2} [] :
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.hom =
@[simp]
theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId {A : Type u_2} [] :
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyInvHomId = Homotopy.trans (Homotopy.ofEq (_ : = AlgebraicTopology.DoldKan.PInfty)) ()
@[simp]
theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv {A : Type u_2} [] :
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.inv =
@[simp]
theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId {A : Type u_2} [] :
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyHomInvId = Homotopy.ofEq (_ : )

The inclusion of the Moore complex in the alternating face map complex is a homotopy equivalence

Instances For