English
There is a natural isomorphism in the Karoubi envelope between the Karoubiization of the nondegenerate complex functor and the forgetful functor composed with Dold–Kan’s N1.
Русский
Существует естественный изоморфизм в оболочке Кароуби между Кароуби-образом функторa ненегенеризованного комплекса и композицией забывающего функторa с N1 Дольда–Кана.
LaTeX
$$$\text{toKaroubi}(\text{nondegComplexFunctor}) \cong (\text{forget}) \circ \mathrm{DoldKan}.N_1$$$
Lean4
/-- The natural isomorphism (in `Karoubi (ChainComplex C ℕ)`) between the chain complex
of nondegenerate simplices of a split simplicial object and the normalized Moore complex
defined as a formal direct factor of the alternating face map complex. -/
@[simps!]
noncomputable def toKaroubiNondegComplexFunctorIsoN₁ :
nondegComplexFunctor ⋙ toKaroubi (ChainComplex C ℕ) ≅ forget C ⋙ DoldKan.N₁ :=
NatIso.ofComponents (fun S => S.s.toKaroubiNondegComplexIsoN₁) fun Φ =>
by
ext n
dsimp
simp only [assoc, PInfty_f_idem_assoc]
erw [← Split.cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋n⦌))]
rw [PInfty_f_naturality]
