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

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

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

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

@[simp]

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

def AlgebraicTopology.DoldKan.homotopyPInftyToId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) : Homotopy AlgebraicTopology.DoldKan.PInfty (CategoryTheory.CategoryStruct.id (AlgebraicTopology.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

@[simp]

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

@[simp]

theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] {Y : CategoryTheory.SimplicialObject A} : AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyInvHomId = Homotopy.trans (Homotopy.ofEq (_ : CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex Y) (AlgebraicTopology.inclusionOfMooreComplexMap Y) = AlgebraicTopology.DoldKan.PInfty)) (AlgebraicTopology.DoldKan.homotopyPInftyToId Y)

@[simp]

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

@[simp]

theorem AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] {Y : CategoryTheory.SimplicialObject A} : AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyHomInvId = Homotopy.ofEq (_ : CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap Y) (AlgebraicTopology.DoldKan.splitMonoInclusionOfMooreComplexMap Y).retraction = CategoryTheory.CategoryStruct.id ((AlgebraicTopology.normalizedMooreComplex A).obj Y))

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

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