mathlib documentation

algebraic_topology.dold_kan.gamma_comp_n

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