English
Let X be an augmented simplicial object in a preadditive category. There is a canonical augmentation ε from the alternating face map complex attached to X to the chain complex concentrated in degree 0, defined by its components on each X and compatible with differentials.
Русский
Пусть X --- аугментированный симплициальный объект в прeадитивной категории. Существует каноническое дополнение ε к связанному с X разложениям чередующихся лицевых отображений к цепочечному комплексу, концентрацией в нулевой степени, и такое дополнение совместимо с дифференциалами.
LaTeX
$$$\varepsilon : \mathrm{SimplicialObject.Augmented.drop} \;\circlearrowleft\; \mathrm{AlgebraicTopology.alternatingFaceMapComplex} \;C \longrightarrow \mathrm{SimplicialObject.Augmented.point} \;\circlearrowleft\; \mathrm{ChainComplex.single_0} C,$$$
Lean4
/-- The natural transformation which gives the augmentation of the alternating face map
complex attached to an augmented simplicial object. -/
def ε [Limits.HasZeroObject C] :
SimplicialObject.Augmented.drop ⋙ AlgebraicTopology.alternatingFaceMapComplex C ⟶
SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C
where
app
X := by
refine (ChainComplex.toSingle₀Equiv _ _).symm ?_
refine ⟨X.hom.app (op ⦋0⦌), ?_⟩
dsimp
rw [alternatingFaceMapComplex_obj_d, objD, Fin.sum_univ_two, Fin.val_zero, pow_zero, one_smul, Fin.val_one, pow_one,
neg_smul, one_smul, add_comp, neg_comp, SimplicialObject.δ_naturality, SimplicialObject.δ_naturality]
apply add_neg_cancel
naturality X Y
f := by
apply HomologicalComplex.to_single_hom_ext
dsimp
erw [ChainComplex.toSingle₀Equiv_symm_apply_f_zero, ChainComplex.toSingle₀Equiv_symm_apply_f_zero]
simp only [ChainComplex.single₀_map_f_zero]
exact congr_app f.w _
