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.

source
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
Instances For
    source
    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.

    Equations
    Instances For
      source
      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)
      source
      @[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
      source
      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
      Instances For
        source
        @[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
        source
        @[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)
        source
        @[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
        source
        @[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).toPrefunctor.obj Y))
        source
        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).toPrefunctor.obj Y) ((AlgebraicTopology.alternatingFaceMapComplex A).toPrefunctor.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.
        Instances For