isIso_homologyι

Mathlib.Algebra.Homology.ShortComplex.Homology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.isIso_homologyι

← MathLib Explorer

English

If S.g = 0, then S.homologyι is an isomorphism.

Русский

Если g комплекса равен нулю, то омонглогический мэппинг ι есть изоморфизм.

LaTeX

$$IsIso S.homologyι$$

Lean4

theorem isIso_homologyι (hg : S.g = 0) [S.HasHomology] : IsIso S.homologyι :=
  by
  have := S.isIso_rightHomologyι hg
  dsimp only [homologyι]
  infer_instance

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

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

Разделы

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

Аффилиация

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