isIso_toCycles

Mathlib.Algebra.Homology.ShortComplex.Exact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.Exact.isIso_toCycles

English

If S is exact, and certain mono/left-homology conditions hold, then the map to cycles is an isomorphism.

Русский

Если S экзактна и выполняются условия моно/левая гомология, то переход к циклам изоморфен.

LaTeX

$$\mathrm{IsIso}(S.toCycles)$$

Lean4

theorem isIso_toCycles (hS : S.Exact) [Mono S.f] [S.HasLeftHomology] : IsIso S.toCycles :=
  hS.isIso_f' _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru