English
Γ₀ is the inverse to the Dold–Kan equivalence in the setting of abelian or pseudo-abelian categories; it is obtained by forgetting the splitting after applying Γ₀'.
Русский
Γ₀ является обратным к эквивалентности Долд–Кана в рамках абелевой или псевдоабелевой категории; получается путём преобразования Γ₀' и последующего забывания сплита.
LaTeX
$$$\Gamma_0 = \mathrm{Split.forget} \circ \Gamma_0' , \quad \Gamma_0 \text{ invert the Dold--Kan equivalence on the given setting.}$$$
Lean4
/-- The functor `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, which is
the inverse functor of the Dold-Kan equivalence when `C` is an abelian
category, or more generally a pseudoabelian category. -/
@[simps!]
def Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C :=
Γ₀' ⋙ Split.forget _
