isoOfQuasiIsoAt_inv_hom_id — Mathlib

English

The inverse of the iso from QuasiIsoAt composed with the homology map equals the identity on the target homology.

Русский

Обратный изоморфизм из QuasiIsoAt, умноженный слева на гомологическое отображение, даёт тождественность на целевой гомологии.

LaTeX

$$(isoOfQuasiIsoAt f i).inv ≫ homologyMap f i = 𝟙 _$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfQuasiIsoAt_inv_hom_id (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :
    (isoOfQuasiIsoAt f i).inv ≫ homologyMap f i = 𝟙 _ :=
  (isoOfQuasiIsoAt f i).inv_hom_id

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