The counit isomorphism of the Dold-Kan equivalence
The purpose of this file is to construct natural isomorphisms
N₁Γ₀ : Γ₀ ⋙ N₁ ≅ toKaroubi (ChainComplex C ℕ)
and N₂Γ₂ : Γ₂ ⋙ N₂ ≅ 𝟭 (Karoubi (ChainComplex C ℕ))
.
(See Equivalence.lean
for the general strategy of proof of the Dold-Kan equivalence.)
The isomorphism (Γ₀.splitting K).nondegComplex ≅ K
for all K : ChainComplex C ℕ
.
Instances For
The natural isomorphism (Γ₀.splitting K).nondegComplex ≅ K
for K : ChainComplex C ℕ
.
Instances For
The natural isomorphism Γ₀ ⋙ N₁ ≅ toKaroubi (ChainComplex C ℕ)
.
Instances For
Compatibility isomorphism between toKaroubi _ ⋙ Γ₂ ⋙ N₂
and Γ₀ ⋙ N₁
which
are functors ChainComplex C ℕ ⥤ Karoubi (ChainComplex C ℕ)
.
Instances For
The counit isomorphism of the Dold-Kan equivalence for additive categories.