mathlib3 documentation


THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. The counit isomorphism of the Dold-Kan equivalence

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