augment_d_succ_succ — Mathlib

English

There is a canonical isomorphism between the truncation of an augmented cochain complex and the augmented truncation, with identity on every component.

Русский

Существует каноническое изоморфизм между усечением дополненного коцепного комплекса и дополненным усечением, действующее как тождество на каждом компоненте.

LaTeX

$$$\\text{truncateAugment} : \\text{truncate}(\\text{augment}(C,f,w)) \\cong C$$$

Lean4

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

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