# 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 #

Helper when we need some `c.rel i j`

(i.e. `ComplexShape.down ℕ`

),
e.g. `c_mk n (n+1) rfl`

This lemma is meant to be used with `nullHomotopicMap'_f_of_not_rel_left`

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]`

## Instances For

We can turn `hσ`

into a datum that can be passed to `nullHomotopicMap'`

.

## Equations

## Instances For

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

## Equations

## Instances For

`Hσ`

is null homotopic

## Equations

## Instances For

In degree `0`

, the null homotopic map `Hσ`

is zero.

The maps `hσ' q n m hnm`

are natural on the simplicial object

For each q, `Hσ q`

is a natural transformation.

## Equations

- AlgebraicTopology.DoldKan.natTransHσ q = { app := fun (X : CategoryTheory.SimplicialObject C) => AlgebraicTopology.DoldKan.Hσ q, naturality := ⋯ }

## Instances For

The maps `hσ' q n m hnm`

are compatible with the application of additive functors.

The null homotopic maps `Hσ`

are compatible with the application of additive functors.