isZero_of_isGE

Mathlib.Algebra.Homology.DerivedCategory.TStructure

URI: https://scilib.ai/kg/mathlib#DerivedCategory.isZero_of_isGE

← MathLib Explorer

English

If i < n and X.IsGE n, then the i-th homology of X vanishes.

Русский

Если i < n и X.IsGE n, то i-я гомология X равна нулю.

LaTeX

$$$$ (i < n) \wedge [X.IsGE(n)] \Rightarrow IsZero\big((\mathrm{homologyFunctor}\;C\;i).\obj X\big). $$$$

Lean4

theorem isZero_of_isGE (X : DerivedCategory C) (n i : ℤ) (hi : i < n) [hX : X.IsGE n] :
    IsZero ((homologyFunctor _ i).obj X) := by
  rw [isGE_iff] at hX
  exact hX i hi

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

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

Разделы

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

Аффилиация

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