liftCycles_i

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

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

English

For any A, if k: A ⟶ S.X₂ and hk is a boundary condition, then liftCycles k hk ≫ iCycles = k.

Русский

Для любого A, если k: A ⟶ S.X₂ и hk задаёт границу, тогда liftCycles k hk ∘ iCycles = k.

LaTeX

$$$S.liftCycles\,k\,hk \circ S.iCycles = k$$$

Lean4

@[reassoc (attr := simp)]
theorem liftCycles_i : S.liftCycles k hk ≫ S.iCycles = k :=
  LeftHomologyData.liftK_i _ k hk

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

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

Разделы

Аффилиация

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