augment_X_succ — Mathlib

English

For any i, the (i+1)-st component of augment(C,f,w) is exactly the i-th component of C; i.e., (augment C f w).X_{i+1} ≅ C.X_i.

Русский

Для любого i компонент augmentation в степени (i+1) равен компоненту исходного C в степени i.

LaTeX

$$$ (\\text{augment}(C,f,w))_{i+1} = C_i \\quad (i\\in\\mathbb{N}) $$$

Lean4

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

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