isZero_of_isLE

Mathlib.Algebra.Homology.DerivedCategory.TStructure

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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