isIso_rightHomologyι — Mathlib

English

Let S be a short complex in a category with zero morphisms. If the connecting map g is zero, then the right-hand homology inclusion map is an isomorphism.

Русский

Пусть S — короткий комплекс в категории, имеющей нуль-морфизмы. Если связующая карта g равна нулю, то включающий морфизм правой гомологии является изоморфизмом.

LaTeX

$$$S.g = 0 \Rightarrow \operatorname{IsIso}(S.rightHomologyι)$$$

Lean4

theorem isIso_rightHomologyι (hg : S.g = 0) : IsIso S.rightHomologyι :=
  RightHomologyData.isIso_ι _ hg

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