comp_δ

Mathlib.Algebra.Homology.HomologySequence

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

English

Exactness of δ in ShortExact implies zero composition with homology map.

Русский

Точность δ в ShortExact влечет нулевую композицию с гомологическим отображением.

LaTeX

$$$\operatorname{comp}_{\delta}$$$

Lean4

@[reassoc (attr := simp)]
theorem comp_δ : HomologicalComplex.homologyMap S.g i ≫ hS.δ i j hij = 0 :=
  (snakeInput hS i j hij).L₀_g_δ

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

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

Разделы

Аффилиация

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