isoOfQuasiIsoAt_hom_inv_id — Mathlib

English

The hom component composed with the inverse of the iso derived from QuasiIsoAt yields the identity on the homology group.

Русский

Гомоморфизм, сочетающий компонент гомологии и обратный изоморфизм QuasiIsoAt, даёт тождественный отображение на гомологии.

LaTeX

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

Lean4

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

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