mathlib documentation


The unit isomorphism of the Dold-Kan equivalence

In order to construct the unit isomorphism of the Dold-Kan equivalence, we first construct natural transformations Γ₂N₁.nat_trans : N₁ ⋙ Γ₂ ⟶ to_karoubi (simplicial_object C) and Γ₂N₂.nat_trans : N₂ ⋙ Γ₂ ⟶ 𝟭 (simplicial_object C). It is then shown that Γ₂N₂.nat_trans is an isomorphism by using that it becomes an isomorphism after the application of the functor N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ) which reflects isomorphisms.