mathlib3 documentation


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.)