isIso_homologyMap'_of_isIso — Mathlib

English

If φ is an isomorphism, then homologyMap'(φ) is an isomorphism.

Русский

Если φ — изоморфизм, то homologyMap'(φ) является изоморфизмом.

LaTeX

$$$\text{IsIso}(\mathrm{homologyMap}'(φ, h_1, h_2))$$$

Lean4

instance isIso_homologyMap'_of_isIso (φ : S₁ ⟶ S₂) [IsIso φ] (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
    IsIso (homologyMap' φ h₁ h₂) :=
  (inferInstance : IsIso (homologyMapIso' (asIso φ) h₁ h₂).hom)

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