English
There is an isomorphism between N₁ and normalizedMooreComplex composed with toKaroubi, illustrating the compatibility of Dold–Kan in the Karoubi setting.
Русский
Существует изоморфизм между N₁ и нормализованным Moore-комплексом в композиции с toKaroubi, показывающий совместимость диагностики Долд–Кана в каруоби-среде.
LaTeX
$$$N_1 \cong (\text{normalizedMooreComplex}) \circ (\mathrm{toKaroubi})$$$
Lean4
/-- When the category `A` is abelian,
the functor `N₁ : SimplicialObject A ⥤ Karoubi (ChainComplex A ℕ)` defined
using `PInfty` identifies to the composition of the normalized Moore complex functor
and the inclusion in the Karoubi envelope. -/
def N₁_iso_normalizedMooreComplex_comp_toKaroubi : N₁ ≅ normalizedMooreComplex A ⋙ toKaroubi _
where
hom := { app := fun X => { f := PInftyToNormalizedMooreComplex X } }
inv := { app := fun X => { f := inclusionOfMooreComplexMap X } }
hom_inv_id := by
ext X : 3
simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, NatTrans.comp_app, Karoubi.comp_f,
N₁_obj_p, NatTrans.id_app, Karoubi.id_f]
inv_hom_id := by
ext X : 3
rw [← cancel_mono (inclusionOfMooreComplexMap X)]
simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_f,
PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, inclusionOfMooreComplexMap_comp_PInfty]
dsimp only [Functor.comp_obj, toKaroubi]
rw [id_comp]
