augment_X_zero — Mathlib

English

In the augmented chain complex, the degree-0 component is exactly X; i.e., the zeroth component of augment(C,f,w) is X.

Русский

В аугментированном цепном комплексе нулевая степень равна X; то есть компонент на уровне 0 равен X.

LaTeX

$$$ (\\text{augment}(C,f,w))_0 = X $$$

Lean4

@[simp]
theorem augment_X_zero (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) : (augment C f w).X 0 = X :=
  rfl

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