English
Let C be a category with additive structure and finite coproducts. There exists a functor Γ₀' from chain complexes over C (indexed by the natural numbers) to the category of simplicial objects equipped with a splitting, and this functor serves as the inverse (in the appropriate sense) of the Dold–Kan equivalence for abelian or pseudo-abelian categories.
Русский
Пусть C — категория с добавляющей структурой и конечными копродуктами. Существует функтор Γ₀' от цепочных комплексoв над C (индексируемых по ℕ) к категории симплициальных объектов со сплитом, и этот функтор является обратным к эквивалентности Долд-Кана в соответствующем смысле для абелевых или псевдоабелевых категорий.
LaTeX
$$$\Gamma_0' : \mathrm{ChainComplex}(C, \mathbb{N}) \longrightarrow \mathrm{SimplicialObject.Split}(C), \quad \Gamma_0 := \mathrm{Split.forget} \circ \Gamma_0' , \text{and } \Gamma_0 \text{ inverts the Dold--Kan equivalence for abelian or pseudoabelian } C.$$$
Lean4
/-- The functor `Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject.Split C`
that induces `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, which
shall be the inverse functor of the Dold-Kan equivalence for
abelian or pseudo-abelian categories. -/
@[simps]
def Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject.Split C
where
obj K := SimplicialObject.Split.mk' (Γ₀.splitting K)
map {K K'}
f :=
{ F := Γ₀.map f
f := f.f
comm := fun n => by
dsimp
simp only [← Splitting.cofan_inj_id, (Γ₀.splitting K).ι_desc]
rfl }
