augmentTruncate_inv_f_zero — Mathlib

English

There is a canonical isomorphism between the augmented truncate of a chain complex and the original chain complex, with explicit maps given by identities on each component.

Русский

Существует каноническое изоморфизм между augmentation-усечением и исходным цепным комплексом, задаваемый тождественными отображениями на каждом компоненте.

LaTeX

$$$\\text{augmentTruncate}(C): (\\text{truncate.obj } C) \\text{ augmented by } C.d_{1,0} \\text{ to } C \\ \\cong\\ C$$$

Lean4

@[simp]
theorem augmentTruncate_inv_f_zero (C : ChainComplex V ℕ) : (augmentTruncate C).inv.f 0 = 𝟙 (C.X 0) :=
  rfl

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