# 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.

Equations
• = Homotopy.equivSubZero.toFun .symm
Instances For
theorem AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant {C : Type u_1} [] {q : } {n : } (hqn : n < q) :
().hom n (n + 1) = .hom n (n + 1)
@[simp]
theorem AlgebraicTopology.DoldKan.homotopyPInftyToId_hom {C : Type u_1} [] (i : ) (j : ) :
= ().hom i j
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

Equations
• = { hom := fun (i j : ) => ().hom i j, zero := , comm := }
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 =
@[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 =

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

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