truncateAugment — Mathlib

English

The inverse of the truncate-augment is identity at degree 0 as well, i.e. inv.f_0 = id.

Русский

Обратный компонент нулевой степени - тождественный.

LaTeX

$$$\\text{truncateAugment}.inv.f_0 = \\mathrm{id}_{(\\text{truncate.obj } (\\text{augment } C f w)).X_0}$$$

Lean4

/-- Truncating an augmented cochain complex is isomorphic (with components the identity)
to the original complex.
-/
def truncateAugment (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) :
    truncate.obj (augment C f w) ≅ C where
  hom := { f := fun _ => 𝟙 _ }
  inv :=
    { f := fun _ => 𝟙 _
      comm' := fun i j => by cases j <;> simp }
  hom_inv_id := by
    ext i
    cases i <;> simp
  inv_hom_id := by
    ext i
    cases i <;> simp

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