mathlib3 documentation


THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.

(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)