Construction of homotopies for the Dold-Kan correspondence

(The general strategy of proof of the Dold-Kan correspondence is explained in Equivalence.lean.)

The purpose of the files Homotopies.lean, Faces.lean, Projections.lean and PInfty.lean is to construct an idempotent endomorphism PInfty : K[X] ⟶ K[X] of the alternating face map complex for each X : SimplicialObject C when C is a preadditive category. In the case C is abelian, this PInfty shall be the projection on the normalized Moore subcomplex of K[X] associated to the decomposition of the complex K[X] as a direct sum of this normalized subcomplex and of the degenerate subcomplex.

In PInfty.lean, this endomorphism PInfty shall be obtained by passing to the limit idempotent endomorphisms P q for all (q : ℕ). These endomorphisms P q are defined by induction. The idea is to start from the identity endomorphism P 0 of K[X] and to ensure by induction that the q higher face maps (except $d_0$) vanish on the image of P q. Then, in a certain degree n, the image of P q for a big enough q will be contained in the normalized subcomplex. This construction is done in Projections.lean.

It would be easy to define the P q degreewise (similarly as it is done in Simplicial Homotopy Theory by Goerrs-Jardine p. 149), but then we would have to prove that they are compatible with the differential (i.e. they are chain complex maps), and also that they are homotopic to the identity. These two verifications are quite technical. In order to reduce the number of such technical lemmas, the strategy that is followed here is to define a series of null homotopic maps Hσ q (attached to families of maps hσ) and use these in order to construct P q : the endomorphisms P q shall basically be obtained by altering the identity endomorphism by adding null homotopic maps, so that we get for free that they are morphisms of chain complexes and that they are homotopic to the identity. The most technical verifications that are needed about the null homotopic maps Hσ are obtained in Faces.lean.

In this file Homotopies.lean, we define the null homotopic maps Hσ q : K[X] ⟶ K[X], show that they are natural (see natTransHσ) and compatible the application of additive functors (see map_Hσ).

References

• [Albrecht Dold, Homology of Symmetric Products and Other Functors of Complexes][dold1958]
• [Paul G. Goerss, John F. Jardine, Simplicial Homotopy Theory][goerss-jardine-2009]

@[inline, reducible]

abbrev AlgebraicTopology.DoldKan.c : ComplexShape ℕ

As we are using chain complexes indexed by ℕ, we shall need the relation c such c m n if and only if n+1=m.

Equations

• AlgebraicTopology.DoldKan.c = ComplexShape.down ℕ

theorem AlgebraicTopology.DoldKan.c_mk (i : ℕ) (j : ℕ) (h : j + 1 = i) : AlgebraicTopology.DoldKan.c.Rel i j

Helper when we need some c.rel i j (i.e. ComplexShape.down ℕ), e.g. c_mk n (n+1) rfl

theorem AlgebraicTopology.DoldKan.cs_down_0_not_rel_left (j : ℕ) : ¬AlgebraicTopology.DoldKan.c.Rel 0 j

This lemma is meant to be used with nullHomotopicMap'_f_of_not_rel_left

def AlgebraicTopology.DoldKan.hσ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) (n : ℕ) : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1)))

The sequence of maps which gives the null homotopic maps Hσ that shall be in the inductive construction of the projections P q : K[X] ⟶ K[X]

Equations

• AlgebraicTopology.DoldKan.hσ q n = if n < q then 0 else (-1) ^ (n - q) • CategoryTheory.SimplicialObject.σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }

def AlgebraicTopology.DoldKan.hσ' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) (n : ℕ) (m : ℕ) : AlgebraicTopology.DoldKan.c.Rel m n → ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X m)

We can turn hσ into a datum that can be passed to nullHomotopicMap'.

Equations

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

theorem AlgebraicTopology.DoldKan.hσ'_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {q : ℕ} {n : ℕ} {m : ℕ} (hnq : n < q) (hnm : AlgebraicTopology.DoldKan.c.Rel m n) : AlgebraicTopology.DoldKan.hσ' q n m hnm = 0

theorem AlgebraicTopology.DoldKan.hσ'_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {q : ℕ} {n : ℕ} {a : ℕ} {m : ℕ} (ha : n = a + q) (hnm : AlgebraicTopology.DoldKan.c.Rel m n) : AlgebraicTopology.DoldKan.hσ' q n m hnm = CategoryTheory.CategoryStruct.comp ((-1) ^ a • CategoryTheory.SimplicialObject.σ X { val := a, isLt := (_ : a < Nat.succ n) }) (CategoryTheory.eqToHom (_ : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1))) = X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk m))))

theorem AlgebraicTopology.DoldKan.hσ'_eq' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {q : ℕ} {n : ℕ} {a : ℕ} (ha : n = a + q) : AlgebraicTopology.DoldKan.hσ' q n (n + 1) (_ : n + 1 = n + 1) = (-1) ^ a • CategoryTheory.SimplicialObject.σ X { val := a, isLt := (_ : a < Nat.succ n) }

def AlgebraicTopology.DoldKan.Hσ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X

The null homotopic map $(hσ q) ∘ d + d ∘ (hσ q)$

Equations

• AlgebraicTopology.DoldKan.Hσ q = Homotopy.nullHomotopicMap' (AlgebraicTopology.DoldKan.hσ' q)

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

Hσ is null homotopic

Equations

• AlgebraicTopology.DoldKan.homotopyHσToZero q = Homotopy.nullHomotopy' (AlgebraicTopology.DoldKan.hσ' q)

theorem AlgebraicTopology.DoldKan.Hσ_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) : (AlgebraicTopology.DoldKan.Hσ q).f 0 = 0

In degree 0, the null homotopic map Hσ is zero.

theorem AlgebraicTopology.DoldKan.hσ'_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) (n : ℕ) (m : ℕ) (hnm : AlgebraicTopology.DoldKan.c.Rel m n) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (AlgebraicTopology.DoldKan.hσ' q n m hnm) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.hσ' q n m hnm) (f.app (Opposite.op (SimplexCategory.mk m)))

The maps hσ' q n m hnm are natural on the simplicial object

def AlgebraicTopology.DoldKan.natTransHσ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) : AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C

For each q, Hσ q is a natural transformation.

Equations

• AlgebraicTopology.DoldKan.natTransHσ q = CategoryTheory.NatTrans.mk fun (X : CategoryTheory.SimplicialObject C) => AlgebraicTopology.DoldKan.Hσ q

theorem AlgebraicTopology.DoldKan.map_hσ' {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (G : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive G] (X : CategoryTheory.SimplicialObject C) (q : ℕ) (n : ℕ) (m : ℕ) (hnm : AlgebraicTopology.DoldKan.c.Rel m n) : AlgebraicTopology.DoldKan.hσ' q n m hnm = G.toPrefunctor.map (AlgebraicTopology.DoldKan.hσ' q n m hnm)

The maps hσ' q n m hnm are compatible with the application of additive functors.

theorem AlgebraicTopology.DoldKan.map_Hσ {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (G : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive G] (X : CategoryTheory.SimplicialObject C) (q : ℕ) (n : ℕ) : (AlgebraicTopology.DoldKan.Hσ q).f n = G.toPrefunctor.map ((AlgebraicTopology.DoldKan.Hσ q).f n)

The null homotopic maps Hσ are compatible with the application of additive functors.