asIsoHomologyπ_inv_comp_homologyπ

English

The inverse of the Iso from S.asIsoHomologyπ composed with S.homologyπ is the identity on S.homology.

Русский

Обратная часть изоморфизма S.asIsoHomologyπ, умноженная на S.homologyπ, даёт тождество на S.homology.

LaTeX

$$(S.asIsoHomologyπ hf).inv ≫ S.homologyπ = 𝟙 _$$

Lean4

@[reassoc (attr := simp)]
theorem asIsoHomologyπ_inv_comp_homologyπ (hf : S.f = 0) [S.HasHomology] :
    (S.asIsoHomologyπ hf).inv ≫ S.homologyπ = 𝟙 _ :=
  Iso.inv_hom_id _

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