isIso_leftHomologyMap_of_iso — Mathlib

English

If φ is an isomorphism and S₁, S₂ have left homology, then leftHomologyMap φ is an isomorphism.

Русский

Если φ — изоморфизм, а S₁, S₂ обладают левой гомологией, то leftHomologyMap φ является изоморфизмом.

LaTeX

$$$\text{IsIso}(\text{leftHomologyMap}(\varphi))$$$

Lean4

instance isIso_leftHomologyMap_of_iso (φ : S₁ ⟶ S₂) [IsIso φ] [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    IsIso (leftHomologyMap φ) :=
  (inferInstance : IsIso (leftHomologyMapIso (asIso φ)).hom)

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