isIso_fromOpcycles — Mathlib

English

In a balanced preadditive category, if a short complex S is exact, g is epi, and S has right homology, then the natural map from opcycles is an isomorphism.

Русский

В сбалансированной предаддитивной категории, если короткий комплекс S точен, г (g) является эпиморфным и существует правая гомология, то естественное отображение fromOpcycles является изоморфизмом.

LaTeX

$$$S\ Exa ct \land Epi(S.g) \land S.HasRightHomology \implies \mathrm{IsIso}(S.fromOpcycles)$$$

Lean4

theorem isIso_fromOpcycles (hS : S.Exact) [Epi S.g] [S.HasRightHomology] : IsIso S.fromOpcycles :=
  hS.isIso_g' _

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