augment_hom_zero — Mathlib

English

In a simplicial object, the augmentation map's 0-th hom component equals the given map f.

Русский

В простейшем объекте аугментация имеет нулевой компонент гомоморфизмы, равный заданному отображению f.

LaTeX

$$(X.augment X₀ f w).hom.app (op ⟦0⟧) = f$$

Lean4

theorem augment_hom_zero (X : SimplicialObject C) (X₀ : C) (f : X _⦋0⦌ ⟶ X₀) (w) :
    (X.augment X₀ f w).hom.app (op ⦋0⦌) = f := by simp

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