English
In the abelian/pseudoabelian setting, there is a canonical comparison isomorphism between the simplicial Dold–Kan N and the idempotent Karoubi version, showing that the two constructions agree up to the Karoubi idempotent completion.
Русский
В псевдобелевой среде существует каноническое сопоставление между конструкциями N и N по Карауби, показывающее согласованность двух подходов через караубьево дополнение.
LaTeX
$$$$ N \cong\, \mathrm{Idempotents}.\mathrm{Karoubi}.DoldKan.N $$$$
Lean4
/-- The comparison isomorphism between `normalizedMooreComplex A` and
the functor `Idempotents.DoldKan.N` from the pseudoabelian case -/
@[simps!]
def comparisonN : (N : SimplicialObject A ⥤ _) ≅ Idempotents.DoldKan.N :=
calc
N ≅ N ⋙ 𝟭 _ := Functor.leftUnitor N
_ ≅ N ⋙ (toKaroubiEquivalence _).functor ⋙ (toKaroubiEquivalence _).inverse :=
(Functor.isoWhiskerLeft _ (toKaroubiEquivalence _).unitIso)
_ ≅ (N ⋙ (toKaroubiEquivalence _).functor) ⋙ (toKaroubiEquivalence _).inverse := (Iso.refl _)
_ ≅ N₁ ⋙ (toKaroubiEquivalence _).inverse :=
(Functor.isoWhiskerRight (N₁_iso_normalizedMooreComplex_comp_toKaroubi A).symm _)
_ ≅ Idempotents.DoldKan.N := Iso.refl _
