English
There is a canonical isomorphism between the Karoubi-constructed object of the nondegenerate complex and the Moore normalised complex N₁.obj X.
Русский
Существует каноническое изоморфизм между каруоби-объектом некондиционной части комплексa и нормализованным комплексом Moore N₁.obj X.
LaTeX
$$(toKaroubi).obj s.nondegComplex ≅ N₁.obj X$$
Lean4
/-- The chain complex `s.nondegComplex` attached to a splitting of a simplicial object `X`
becomes isomorphic to the normalized Moore complex `N₁.obj X` defined as a formal direct
factor in the category `Karoubi (ChainComplex C ℕ)`. -/
@[simps]
noncomputable def toKaroubiNondegComplexIsoN₁ : (toKaroubi _).obj s.nondegComplex ≅ N₁.obj X
where
hom :=
{ f :=
{ f := fun n => (s.cofan _).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n
comm' := fun i j _ => by
dsimp
rw [assoc, assoc, assoc, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, HomologicalComplex.Hom.comm] }
comm := by
ext n
dsimp
rw [id_comp, assoc, PInfty_f_idem] }
inv :=
{ f :=
{ f := fun n => s.πSummand (IndexSet.id (op ⦋n⦌))
comm' := fun i j _ => by
dsimp
slice_rhs 1 1 => rw [← id_comp (K[X].d i j)]
dsimp only [AlternatingFaceMapComplex.obj_X]
rw [s.decomposition_id, sum_comp, sum_comp, Finset.sum_eq_single (IndexSet.id (op ⦋i⦌)), assoc, assoc]
· intro A _ hA
simp only [assoc, s.ιSummand_comp_d_comp_πSummand_eq_zero _ _ _ hA, comp_zero]
· simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff] }
comm := by
ext n
dsimp
simp only [comp_id, PInfty_comp_πSummand_id] }
hom_inv_id := by
ext n
simp only [assoc, PInfty_comp_πSummand_id, Karoubi.comp_f, HomologicalComplex.comp_f, cofan_inj_πSummand_eq_id]
rfl
inv_hom_id := by
ext n
simp only [πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, Karoubi.comp_f, HomologicalComplex.comp_f, N₁_obj_p,
Karoubi.id_f]
