The Dold-Kan correspondence for pseudoabelian categories #
In this file, for any idempotent complete additive category C,
the Dold-Kan equivalence
idempotents.dold_kan.equivalence C : simplicial_object C ≌ chain_complex C ℕ
is obtained. It is deduced from the equivalence
preadditive.dold_kan.equivalence between the respective idempotent
completions of these categories using the fact that when C is idempotent complete,
then both simplicial_object C and chain_complex C ℕ are idempotent complete.
The construction of idempotents.dold_kan.equivalence uses the tools
introduced in the file compatibility.lean. Doing so, the functor
idempotents.dold_kan.N of the equivalence is
the composition of N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)
(defined in functor_n.lean) and the inverse of the equivalence
chain_complex C ℕ ≌ karoubi (chain_complex C ℕ). The functor
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.)
The functor N for the equivalence is obtained by composing
N' : simplicial_object C ⥤ karoubi (chain_complex C ℕ) and the inverse
of the equivalence chain_complex C ℕ ≌ karoubi (chain_complex C ℕ).
The functor Γ for the equivalence is Γ'.
The Dold-Kan equivalence for pseudoabelian categories given
by the functors N and Γ. It is obtained by applying the results in
compatibility.lean to the equivalence preadditive.dold_kan.equivalence.
The natural isomorphism NΓ' satisfies the compatibility that is needed for the construction of our counit isomorphismη`
The counit isomorphism induced by N₁Γ₀
The unit isomorphism induced by Γ₂N₁.