truncateAugment_inv_f — Mathlib

English

In the isomorphism between truncation and augmented, the inverse components are identities on all degrees.

Русский

Обратная часть изоморфизма между усечением иaugmentation — тождественна на всех степенях.

LaTeX

$$$\\text{truncateAugment}.inv.f_i = \\mathrm{id}_{(\\text{truncate}.(\\text{augment}(C,f,w))).X_i} \\quad \\forall i$$$

Lean4

@[simp]
theorem truncateAugment_inv_f (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) (i : ℕ) :
    (truncateAugment C f w).inv.f i = 𝟙 ((truncate.obj (augment C f w)).X i) :=
  rfl

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