isIso_δ

Mathlib.Algebra.Homology.HomologySequence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.ShortExact.isIso_δ

← MathLib Explorer

English

If both H_i(S.X2) and H_j(S.X2) vanish (i.e., hi and hj), then δ i j hij is an isomorphism.

Русский

Если обе гомологии в i и j исчезают, то δ i j hij является изоморфизмом.

LaTeX

$$hS.δ i j hij is an isomorphism$$

Lean4

theorem isIso_δ (hi : IsZero (S.X₂.homology i)) (hj : IsZero (S.X₂.homology j)) : IsIso (hS.δ i j hij) :=
  (HomologicalComplex.HomologySequence.snakeInput _ _ _ _).isIso_δ hi hj

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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