δ_comp

Mathlib.Algebra.Homology.HomologySequence

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

English

δ_comp in ShortExact implies zero composition with homology maps.

Русский

δ_comp в ShortExact означает тождественный нуль композиции с гомологическими отображениями.

LaTeX

$$$hS.\delta i j hij ≫ \mathrm{homologyMap}\,S.f j = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem δ_comp : hS.δ i j hij ≫ HomologicalComplex.homologyMap S.f j = 0 :=
  (snakeInput hS i j hij).δ_L₃_f

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

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

Разделы

Аффилиация

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