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} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (q : ℕ) : Homotopy (P q) (CategoryTheory.CategoryStruct.id (AlternatingFaceMapComplex.obj X))

Inductive construction of homotopies from P q to 𝟙 _

Equations

• One or more equations did not get rendered due to their size.
• AlgebraicTopology.DoldKan.homotopyPToId X 0 = Homotopy.refl (AlgebraicTopology.DoldKan.P 0)

noncomputable def AlgebraicTopology.DoldKan.homotopyQToZero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (q : ℕ) : Homotopy (Q q) 0

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

Equations

• AlgebraicTopology.DoldKan.homotopyQToZero X q = Homotopy.equivSubZero.toFun (AlgebraicTopology.DoldKan.homotopyPToId X q).symm

theorem AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {q n : ℕ} (hqn : n < q) : (homotopyPToId X (q + 1)).hom n (n + 1) = (homotopyPToId X q).hom n (n + 1)

noncomputable def AlgebraicTopology.DoldKan.homotopyPInftyToId {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) : Homotopy PInfty (CategoryTheory.CategoryStruct.id (AlternatingFaceMapComplex.obj X))

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

Equations

• AlgebraicTopology.DoldKan.homotopyPInftyToId X = { hom := fun (i j : ℕ) => (AlgebraicTopology.DoldKan.homotopyPToId X (j + 1)).hom i j, zero := ⋯, comm := ⋯ }

@[simp]

theorem AlgebraicTopology.DoldKan.homotopyPInftyToId_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (i j : ℕ) : (homotopyPInftyToId X).hom i j = (homotopyPToId X (j + 1)).hom i j

noncomputable def AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Abelian A] {Y : CategoryTheory.SimplicialObject A} : HomotopyEquiv ((normalizedMooreComplex A).obj Y) ((alternatingFaceMapComplex A).obj Y)

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.

@[simp]

theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Abelian A] {Y : CategoryTheory.SimplicialObject A} : homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyHomInvId = Homotopy.ofEq ⋯

@[simp]

theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Abelian A] {Y : CategoryTheory.SimplicialObject A} : homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.inv = PInftyToNormalizedMooreComplex Y

@[simp]

theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Abelian A] {Y : CategoryTheory.SimplicialObject A} : homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.hom = inclusionOfMooreComplexMap Y

@[simp]

theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.Abelian A] {Y : CategoryTheory.SimplicialObject A} : homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyInvHomId = (Homotopy.ofEq ⋯).trans (homotopyPInftyToId Y)