diff --git a/src/algebraic_topology/dold_kan/compatibility.lean b/src/algebraic_topology/dold_kan/compatibility.lean
index 3567efda0ccc9..516e38ecaf374 100644
--- a/src/algebraic_topology/dold_kan/compatibility.lean
+++ b/src/algebraic_topology/dold_kan/compatibility.lean
@@ -36,7 +36,9 @@ inverse of `eB`:
 but whose inverse functor is `G`.
 
 When extra assumptions are given, we shall also provide simplification lemmas for the
-unit and counit isomorphisms of `equivalence`. (TODO)
+unit and counit isomorphisms of `equivalence`.
+
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
 
 -/
 
diff --git a/src/algebraic_topology/dold_kan/decomposition.lean b/src/algebraic_topology/dold_kan/decomposition.lean
index 1d89283129af6..f1cbbb85fd8b7 100644
--- a/src/algebraic_topology/dold_kan/decomposition.lean
+++ b/src/algebraic_topology/dold_kan/decomposition.lean
@@ -29,6 +29,8 @@ role in the proof that the functor
 `N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ))`
 reflects isomorphisms.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 open category_theory category_theory.category category_theory.preadditive opposite
diff --git a/src/algebraic_topology/dold_kan/degeneracies.lean b/src/algebraic_topology/dold_kan/degeneracies.lean
index c3b3de9892ba2..ab0584b061494 100644
--- a/src/algebraic_topology/dold_kan/degeneracies.lean
+++ b/src/algebraic_topology/dold_kan/degeneracies.lean
@@ -25,6 +25,8 @@ if `X : simplicial_object C` with `C` a preadditive category,
 `X.map θ.op ≫ P_infty.f n = 0`. It follows from the more precise
 statement vanishing statement `σ_comp_P_eq_zero` for the `P q`.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 open category_theory category_theory.category category_theory.limits
diff --git a/src/algebraic_topology/dold_kan/equivalence.lean b/src/algebraic_topology/dold_kan/equivalence.lean
new file mode 100644
index 0000000000000..dc025a7938b2b
--- /dev/null
+++ b/src/algebraic_topology/dold_kan/equivalence.lean
@@ -0,0 +1,175 @@
+/-
+Copyright (c) 2022 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import algebraic_topology.dold_kan.equivalence_pseudoabelian
+import algebraic_topology.dold_kan.normalized
+
+/-!
+
+# The Dold-Kan correspondence
+
+The Dold-Kan correspondence states that for any abelian category `A`, there is
+an equivalence between the category of simplicial objects in `A` and the
+category of chain complexes in `A` (with degrees indexed by `ℕ` and the
+homological convention that the degree is decreased by the differentials).
+
+In this file, we finish the construction of this equivalence by providing
+`category_theory.abelian.dold_kan.equivalence` which is of type
+`simplicial_object A ≌ chain_complex A ℕ` for any abelian category `A`.
+The functor `simplicial_object A ⥤ chain_complex A ℕ` of this equivalence is
+definitionally equal to `normalized_Moore_complex A`.
+
+## Overall strategy of the proof of the correspondence
+
+Before starting the implementation of the proof in Lean, the author noticed
+that the Dold-Kan equivalence not only applies to abelian categories, but
+should also hold generally for any pseudoabelian category `C`
+(i.e. a category with instances `[preadditive C]`
+`[has_finite_coproducts C]` and `[is_idempotent_complete C]`): this is
+`category_theory.idempotents.dold_kan.equivalence`.
+
+When the alternating face map complex `K[X]` of a simplicial object `X` in an
+abelian is studied, it is shown that it decomposes as a direct sum of the
+normalized subcomplex and of the degenerate subcomplex. The crucial observation
+is that in this decomposition, the projection on the normalized subcomplex can
+be defined in each degree using simplicial operators. Then, the definition
+of this projection `P_infty : K[X] ⟶ K[X]` can be carried out for any
+`X : simplicial_object C` when `C` is a preadditive category.
+
+The construction of the endomorphism `P_infty` is done in the files
+`homotopies.lean`, `faces.lean`, `projections.lean` and `p_infty.lean`.
+Eventually, as we would also like to show that the inclusion of the normalized
+Moore complex is a homotopy equivalence (cf. file `homotopy_equivalence.lean`),
+this projection `P_infty` needs to be homotopic to the identity. In our
+construction, we get this for free because `P_infty` is obtained by altering
+the identity endomorphism by null homotopic maps. More details about this
+aspect of the proof are in the file `homotopies.lean`.
+
+When the alternating face map complex `K[X]` is equipped with the idempotent
+endomorphism `P_infty`, it becomes an object in `karoubi (chain_complex C ℕ)`
+which is the idempotent completion of the category `chain_complex C ℕ`. In `functor_n.lean`,
+we obtain this functor `N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)`,
+which is formally extended as
+`N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)`. (Here, some functors
+have an index which is the number of occurrences of `karoubi` at the source or the
+target.)
+
+In `functor_gamma.lean`, assuming that the category `C` is additive,
+we define the functor in the other direction
+`Γ₂ : karoubi (chain_complex C ℕ) ⥤ karoubi (simplicial_object C)` as the formal
+extension of a functor `Γ₀ : chain_complex C ℕ ⥤ simplicial_object C` which is
+defined similarly as in *Simplicial Homotopy Theory* by Goerss-Jardine.
+In `degeneracies.lean`, we show that `P_infty` vanishes on the image of degeneracy
+operators, which is one of the key properties that makes it possible to contruct
+the isomorphism `N₂Γ₂ : Γ₂ ⋙ N₂ ≅ 𝟭 (karoubi (chain_complex C ℕ))`.
+
+The rest of the proof follows the strategy in the [original paper by Dold][dold1958]. We show
+that the functor `N₂` reflects isomorphisms in `n_reflects_iso.lean`: this relies on a
+decomposition of the identity of `X _[n]` using `P_infty.f n` and degeneracies obtained in
+`decomposition.lean`. Then, in `n_comp_gamma.lean`, we construct a natural transformation
+`Γ₂N₂.trans : N₂ ⋙ Γ₂ ⟶ 𝟭 (karoubi (simplicial_object C))`. It is shown that it is an
+isomorphism using the fact that `N₂` reflects isomorphisms, and because we can show
+that the composition `N₂ ⟶ N₂ ⋙ Γ₂ ⋙ N₂ ⟶ N₂` is the identity (see `identity_N₂`). The fact
+that `N₂` is defined as a formal direct factor makes the proof easier because we only
+have to compare endomorphisms of an alternating face map complex `K[X]` and we do not
+have to worry with inclusions of kernel subobjects.
+
+In `equivalence_additive.lean`, we obtain
+the equivalence `equivalence : karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ)`.
+It is in the namespace `category_theory.preadditive.dold_kan`. The functors in this
+equivalence are named `N` and `Γ`: by definition, they are `N₂` and `Γ₂`.
+
+In `equivalence_pseudoabelian.lean`, assuming `C` is idempotent complete,
+we obtain `equivalence : simplicial_object C ≌ chain_complex C ℕ`
+in the namespace `category_theory.idempotents.dold_kan`. This could be roughly
+obtained by composing the previous equivalence with the equivalences
+`simplicial_object C ≌ karoubi (simplicial_object C)` and
+`karoubi (chain_complex C ℕ) ≌ chain_complex C ℕ`. Instead, we polish this construction
+in `compatibility.lean` by ensuring good definitional properties of the equivalence (e.g.
+the inverse functor is definitionallly equal to
+`Γ₀' : chain_complex C ℕ ⥤ simplicial_object C`) and
+showing compatibilities for the unit and counit isomorphisms.
+
+In this file `equivalence.lean`, assuming the category `A` is abelian, we obtain
+`equivalence : simplicial_object A ≌ chain_complex A ℕ` in the namespace
+`category_theory.abelian.dold_kan`. This is obtained by replacing the functor
+`category_theory.idempotents.dold_kan.N` of the equivalence in the pseudoabelian case
+with the isomorphic functor `normalized_Moore_complex A` thanks to the isomorphism
+obtained in `normalized.lean`.
+
+TODO: Show functoriality properties of the three equivalences above. More precisely,
+for example in the case of abelian categories `A` and `B`, if `F : A ⥤ B` is an
+additive functor, we can show that the functors `N` for `A` and `B` are compatible
+with the functors `simplicial_object A ⥤ simplicial_object B` and
+`chain_complex A ℕ ⥤ chain_complex B ℕ` induced by `F`. (Note that this does not
+require that `F` is an exact functor!)
+
+TODO: Introduce the degenerate subcomplex `D[X]` which is generated by
+degenerate simplices, show that the projector `P_infty` corresponds to
+a decomposition `K[X] ≅ N[X] ⊞ D[X]`.
+
+TODO: dualise all of this as `cosimplicial_object A ⥤ cochain_complex A ℕ`. (It is unclear
+what is the best way to do this. The exact design may be decided when it is needed.)
+
+## 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]
+
+-/
+
+noncomputable theory
+
+open category_theory
+open category_theory.category
+open category_theory.idempotents
+
+variables {A : Type*} [category A] [abelian A]
+
+namespace category_theory
+
+namespace abelian
+
+namespace dold_kan
+
+open algebraic_topology.dold_kan
+
+/-- The functor `N` for the equivalence is `normalized_Moore_complex A` -/
+def N : simplicial_object A ⥤ chain_complex A ℕ := algebraic_topology.normalized_Moore_complex A
+
+/-- The functor `Γ` for the equivalence is the same as in the pseudoabelian case. -/
+def Γ : chain_complex A ℕ ⥤ simplicial_object A := idempotents.dold_kan.Γ
+
+/-- The comparison isomorphism between `normalized_Moore_complex A` and
+the functor `idempotents.dold_kan.N` from the pseudoabelian case -/
+@[simps]
+def comparison_N : (N : simplicial_object A ⥤ _) ≅ idempotents.dold_kan.N :=
+calc N ≅ N ⋙ 𝟭 _ : functor.left_unitor N
+... ≅ N ⋙ ((to_karoubi_equivalence _).functor ⋙ (to_karoubi_equivalence _).inverse) :
+  iso_whisker_left _ (to_karoubi_equivalence _).unit_iso
+... ≅ (N ⋙ (to_karoubi_equivalence _).functor) ⋙ (to_karoubi_equivalence _).inverse :
+  iso.refl _
+... ≅ N₁ ⋙ (to_karoubi_equivalence _).inverse : iso_whisker_right
+  (N₁_iso_normalized_Moore_complex_comp_to_karoubi A).symm _
+... ≅ idempotents.dold_kan.N : by refl
+
+/-- The Dold-Kan equivalence for abelian categories -/
+@[simps functor]
+def equivalence : simplicial_object A ≌ chain_complex A ℕ :=
+begin
+  let F : simplicial_object A ⥤ _ := idempotents.dold_kan.N,
+  let hF : is_equivalence F := is_equivalence.of_equivalence idempotents.dold_kan.equivalence,
+  letI : is_equivalence (N : simplicial_object A ⥤ _ ) :=
+    is_equivalence.of_iso comparison_N.symm hF,
+  exact N.as_equivalence,
+end
+
+lemma equivalence_inverse : (equivalence : simplicial_object A ≌ _).inverse = Γ := rfl
+
+end dold_kan
+
+end abelian
+
+end category_theory
diff --git a/src/algebraic_topology/dold_kan/equivalence_additive.lean b/src/algebraic_topology/dold_kan/equivalence_additive.lean
index 886aefc7db66b..742196ac2a72b 100644
--- a/src/algebraic_topology/dold_kan/equivalence_additive.lean
+++ b/src/algebraic_topology/dold_kan/equivalence_additive.lean
@@ -14,6 +14,8 @@ import algebraic_topology.dold_kan.n_comp_gamma
 This file defines `preadditive.dold_kan.equivalence` which is the equivalence
 of categories `karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ)`.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 noncomputable theory
diff --git a/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean b/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean
index dd766e8a5e41f..4d6fff16434a8 100644
--- a/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean
+++ b/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean
@@ -29,6 +29,8 @@ the composition of `N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)
 `idempotents.dold_kan.Γ` of the equivalence is by definition the functor
 `Γ₀` introduced in `functor_gamma.lean`.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 noncomputable theory
diff --git a/src/algebraic_topology/dold_kan/faces.lean b/src/algebraic_topology/dold_kan/faces.lean
index ae2b2f6e8fff0..d9e7af0e63960 100644
--- a/src/algebraic_topology/dold_kan/faces.lean
+++ b/src/algebraic_topology/dold_kan/faces.lean
@@ -25,6 +25,8 @@ The main lemma in this file is `higher_faces_vanish.induction`. It is based
 on two technical lemmas `higher_faces_vanish.comp_Hσ_eq` and
 `higher_faces_vanish.comp_Hσ_eq_zero`.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 open nat
diff --git a/src/algebraic_topology/dold_kan/functor_gamma.lean b/src/algebraic_topology/dold_kan/functor_gamma.lean
index 9a5675b665216..bd138e8ba7d11 100644
--- a/src/algebraic_topology/dold_kan/functor_gamma.lean
+++ b/src/algebraic_topology/dold_kan/functor_gamma.lean
@@ -27,6 +27,8 @@ By construction, `Γ₀.obj K` is a split simplicial object whose splitting is `
 We also construct `Γ₂ : karoubi (chain_complex C ℕ) ⥤ karoubi (simplicial_object C)`
 which shall be an equivalence for any additive category `C`.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 noncomputable theory
diff --git a/src/algebraic_topology/dold_kan/functor_n.lean b/src/algebraic_topology/dold_kan/functor_n.lean
index 17a1db8bb19eb..74f4d58a98df4 100644
--- a/src/algebraic_topology/dold_kan/functor_n.lean
+++ b/src/algebraic_topology/dold_kan/functor_n.lean
@@ -32,7 +32,7 @@ defined in `equivalence_pseudoabelian.lean`.
 When the category `C` is abelian, a relation between `N₁` and the
 normalized Moore complex functor shall be obtained in `normalized.lean`.
 
-(See `equivalence.lean` for the general strategy of proof.)
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
 
 -/
 
diff --git a/src/algebraic_topology/dold_kan/gamma_comp_n.lean b/src/algebraic_topology/dold_kan/gamma_comp_n.lean
index b3d66c5c2cfcc..86e9a3e0230c0 100644
--- a/src/algebraic_topology/dold_kan/gamma_comp_n.lean
+++ b/src/algebraic_topology/dold_kan/gamma_comp_n.lean
@@ -16,6 +16,8 @@ The purpose of this file is to construct natural isomorphisms
 `N₁Γ₀ : Γ₀ ⋙ N₁ ≅ to_karoubi (chain_complex C ℕ)`
 and `N₂Γ₂ : Γ₂ ⋙ N₂ ≅ 𝟭 (karoubi (chain_complex C ℕ))`.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 noncomputable theory
diff --git a/src/algebraic_topology/dold_kan/n_comp_gamma.lean b/src/algebraic_topology/dold_kan/n_comp_gamma.lean
index 52bdb21046dc0..ac2c1537c3539 100644
--- a/src/algebraic_topology/dold_kan/n_comp_gamma.lean
+++ b/src/algebraic_topology/dold_kan/n_comp_gamma.lean
@@ -21,6 +21,8 @@ that it becomes an isomorphism after the application of the functor
 `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)`
 which reflects isomorphisms.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 noncomputable theory
diff --git a/src/algebraic_topology/dold_kan/n_reflects_iso.lean b/src/algebraic_topology/dold_kan/n_reflects_iso.lean
index d9cd2e612a1e0..10541d6b39f98 100644
--- a/src/algebraic_topology/dold_kan/n_reflects_iso.lean
+++ b/src/algebraic_topology/dold_kan/n_reflects_iso.lean
@@ -21,6 +21,8 @@ In this file, it is shown that the functors
 `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))`
 reflect isomorphisms for any preadditive category `C`.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 open category_theory
diff --git a/src/algebraic_topology/dold_kan/normalized.lean b/src/algebraic_topology/dold_kan/normalized.lean
index c182615e41b7c..d01fa53ec4cd0 100644
--- a/src/algebraic_topology/dold_kan/normalized.lean
+++ b/src/algebraic_topology/dold_kan/normalized.lean
@@ -27,6 +27,8 @@ the Dold-Kan equivalence
 `category_theory.abelian.dold_kan.equivalence : simplicial_object A ≌ chain_complex A ℕ`
 with a functor (definitionally) equal to `normalized_Moore_complex A`.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 open category_theory category_theory.category category_theory.limits
diff --git a/src/algebraic_topology/dold_kan/notations.lean b/src/algebraic_topology/dold_kan/notations.lean
index 67fda8f17e311..3276ab335e94a 100644
--- a/src/algebraic_topology/dold_kan/notations.lean
+++ b/src/algebraic_topology/dold_kan/notations.lean
@@ -17,6 +17,8 @@ This file defines the notation `K[X] : chain_complex C ℕ` for the alternating
 map complex of `(X : simplicial_object C)` where `C` is a preadditive category, as well
 as `N[X]` for the normalized subcomplex in the case `C` is an abelian category.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 localized "notation (name := alternating_face_map_complex) `K[`X`]` :=
diff --git a/src/algebraic_topology/dold_kan/p_infty.lean b/src/algebraic_topology/dold_kan/p_infty.lean
index b95df628099e3..7b1c539dca8bf 100644
--- a/src/algebraic_topology/dold_kan/p_infty.lean
+++ b/src/algebraic_topology/dold_kan/p_infty.lean
@@ -22,7 +22,8 @@ to the limit the projections `P q` defined in `projections.lean`. This
 projection is a critical tool in this formalisation of the Dold-Kan correspondence,
 because in the case of abelian categories, `P_infty` corresponds to the
 projection on the normalized Moore subcomplex, with kernel the degenerate subcomplex.
-(See `equivalence.lean` for the general strategy of proof.)
+
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
 
 -/
 
diff --git a/src/algebraic_topology/dold_kan/projections.lean b/src/algebraic_topology/dold_kan/projections.lean
index 2439974a9359a..4b9ea21fdc872 100644
--- a/src/algebraic_topology/dold_kan/projections.lean
+++ b/src/algebraic_topology/dold_kan/projections.lean
@@ -30,6 +30,8 @@ By passing to the limit, these endomorphisms `P q` shall be used in `p_infty.lea
 in order to define `P_infty : K[X] ⟶ K[X]`, see `equivalence.lean` for the general
 strategy of proof of the Dold-Kan equivalence.
 
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 open category_theory category_theory.category category_theory.limits
diff --git a/src/algebraic_topology/dold_kan/split_simplicial_object.lean b/src/algebraic_topology/dold_kan/split_simplicial_object.lean
index f3b2c7fec482f..997675cde1821 100644
--- a/src/algebraic_topology/dold_kan/split_simplicial_object.lean
+++ b/src/algebraic_topology/dold_kan/split_simplicial_object.lean
@@ -18,6 +18,9 @@ import algebraic_topology.dold_kan.functor_n
 In this file we define a functor `nondeg_complex : simplicial_object.split C ⥤ chain_complex C ℕ`
 when `C` is a preadditive category with finite coproducts, and get an isomorphism
 `to_karoubi_nondeg_complex_iso_N₁ : nondeg_complex ⋙ to_karoubi _ ≅ forget C ⋙ dold_kan.N₁`.
+
+(See `equivalence.lean` for the general strategy of proof of the Dold-Kan equivalence.)
+
 -/
 
 noncomputable theory