ε_app_f_zero — Mathlib

English

For any augmented simplicial object X, the degree zero component of ε.app X equals the degree-zero component map X.hom.app at 0.

Русский

Для любого аугментированного симплициального объекта X нулевой компонент ε.app X равен гомоморфизму X.hom.app на нуле.

LaTeX

$$$(\varepsilon.{\rm app}\,X).f\,0 = X.{\rm hom}.app(\mathrm{op}\;⟨0⟩)$$$

Lean4

@[simp]
theorem ε_app_f_zero [Limits.HasZeroObject C] (X : SimplicialObject.Augmented C) : (ε.app X).f 0 = X.hom.app (op ⦋0⦌) :=
  ChainComplex.toSingle₀Equiv_symm_apply_f_zero _ _

Похожие утверждения