English
There is a natural isomorphism expressing the equivalence between Karoubi(SimplicialObject C) and the composition N₁ followed by Γ₂, realized through Karoubi embeddings and the Dold–Kan identifications.
Русский
Существуют натуральные изоморфизмы, выражающие эквивалентность Karoubi(SimplicialObject C) и композиции N₁ с Γ₂, реализованные через вложения Каруоби и идентификации Дольд–Кана.
LaTeX
$$$N_2 \circ (karoubiChainComplexEquivalence C Nat).functor = karoubiEmbedding \circ N_1 \circ (karoubiChainComplexEquivalence (Karoubi C) Nat).functor \circ (Functor.mapHomologicalComplex (KaroubiKaroubi.equivalence C).inverse)$$$
Lean4
/-- `PInfty` factors through the normalized Moore complex -/
@[simps!]
def PInftyToNormalizedMooreComplex (X : SimplicialObject A) : K[X] ⟶ N[X] :=
ChainComplex.ofHom _ _ _ _ _ _ (fun n => factorThru _ _ (factors_normalizedMooreComplex_PInfty n)) fun n =>
by
rw [← cancel_mono (NormalizedMooreComplex.objX X n).arrow, assoc, assoc, factorThru_arrow, ←
inclusionOfMooreComplexMap_f, ← normalizedMooreComplex_objD, ← (inclusionOfMooreComplexMap X).comm (n + 1) n,
inclusionOfMooreComplexMap_f, factorThru_arrow_assoc, ← alternatingFaceMapComplex_obj_d]
exact PInfty.comm (n + 1) n
