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 : ℕ)
:
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)
Instances For
def
AlgebraicTopology.DoldKan.homotopyQToZero
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
(X : CategoryTheory.SimplicialObject C)
(q : ℕ)
:
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
Instances For
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)
:
(AlgebraicTopology.DoldKan.homotopyPToId X (q + 1)).hom n (n + 1) = (AlgebraicTopology.DoldKan.homotopyPToId X q).hom 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 : ℕ)
:
(AlgebraicTopology.DoldKan.homotopyPInftyToId X).hom i j = (AlgebraicTopology.DoldKan.homotopyPToId X (j + 1)).hom 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
Equations
- AlgebraicTopology.DoldKan.homotopyPInftyToId X = { hom := fun (i j : ℕ) => (AlgebraicTopology.DoldKan.homotopyPToId X (j + 1)).hom i j, zero := ⋯, comm := ⋯ }
Instances For
@[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_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_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 ⋯
@[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.ofEq ⋯).trans (AlgebraicTopology.DoldKan.homotopyPInftyToId 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
Equations
- One or more equations did not get rendered due to their size.