English
There is a canonical isomorphism between the Karoubiized nondegenerate complex of a split simplicial object and the normalized complex N₁ of X.
Русский
Существует каноническое изоморождение между Карауобианализованным ненезаднегенным комплексом расщепленного симплициального объекта и нормализованным комплексом N₁ объекта X.
LaTeX
$$$(toKaroubi _).obj s.nondegComplex \cong N_1.obj X$$$
Lean4
/-- If `s` is a splitting of a simplicial object `X` in a preadditive category,
`s.nondegComplex` is a chain complex which is given in degree `n` by
the nondegenerate `n`-simplices of `X`. -/
@[simps]
noncomputable def nondegComplex : ChainComplex C ℕ where
X := s.N
d := s.d
shape i j hij := by simp only [d, K[X].shape i j hij, zero_comp, comp_zero]
d_comp_d' i j k _
_ := by
simp only [d, assoc]
have eq : K[X].d i j ≫ 𝟙 (X.obj (op ⦋j⦌)) ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0 := by simp
rw [s.decomposition_id] at eq
classical
rw [Fintype.sum_eq_add_sum_compl (IndexSet.id (op ⦋j⦌)), add_comp, comp_add, assoc, Preadditive.sum_comp,
Preadditive.comp_sum, Finset.sum_eq_zero, add_zero] at eq
swap
· intro A hA
simp only [Finset.mem_compl, Finset.mem_singleton] at hA
simp only [assoc, ιSummand_comp_d_comp_πSummand_eq_zero _ _ _ _ hA, comp_zero]
rw [eq, comp_zero]
