English
Let C be a preadditive category with finite coproducts. There is a canonical functor that assigns to every split simplicial object in C the chain complex formed by its nondegenerate simplices.
Русский
Пусть C — прядпостопная категория с конечными комбинированными копроизведениями. Существует канонический функтор, который сопоставляет каждому расщеплённому симплициальному объекту в C цепной комплекс, образованный из ненегенерируемых симплисов.
LaTeX
$$$F: \mathrm{Split}(\mathcal{C}) \longrightarrow \mathrm{Ch}(\mathcal{C},\mathbb{N}), \quad F(S) = S.s.nondegComplex$$$
Lean4
/-- The functor which sends a split simplicial object in a preadditive category to
the chain complex which consists of nondegenerate simplices. -/
@[simps]
noncomputable def nondegComplexFunctor : Split C ⥤ ChainComplex C ℕ
where
obj S := S.s.nondegComplex
map {S₁ S₂}
Φ :=
{ f := Φ.f
comm' := fun i j _ => by
dsimp
erw [← cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋i⦌)),
((alternatingFaceMapComplex C).map Φ.F).comm_assoc i j]
simp only [assoc]
congr 2
apply S₁.s.hom_ext'
intro A
dsimp [alternatingFaceMapComplex]
rw [cofan_inj_naturality_symm_assoc Φ A]
by_cases h : A.EqId
· dsimp at h
subst h
rw [Splitting.cofan_inj_πSummand_eq_id]
dsimp
rw [comp_id, Splitting.cofan_inj_πSummand_eq_id_assoc]
·
rw [S₁.s.cofan_inj_πSummand_eq_zero_assoc _ _ (Ne.symm h), S₂.s.cofan_inj_πSummand_eq_zero _ _ (Ne.symm h),
zero_comp, comp_zero] }
