isIso_rightHomologyMap_of_iso — Mathlib

English

Let C be a category with zero morphisms. If S1 and S2 are short complexes over C possessing right homology, and φ: S1 → S2 is an isomorphism, then the induced rightHomologyMap φ is an isomorphism.

Русский

Пусть C — категория с нулевыми морфизмами. Пусть S1 и S2 — короткие комплексы над C, обладающие правой гомологией, и пусть φ: S1 → S2 является изоморфизмом. Тогда индуцированное отображение правой гомологии φ является изоморфизмом.

LaTeX

$$$IsIso\left(\mathrm{rightHomologyMap}(\varphi)\right)$$$

Lean4

instance isIso_rightHomologyMap_of_iso (φ : S₁ ⟶ S₂) [IsIso φ] [S₁.HasRightHomology] [S₂.HasRightHomology] :
    IsIso (rightHomologyMap φ) :=
  (inferInstance : IsIso (rightHomologyMapIso (asIso φ)).hom)

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