p_g'

Mathlib.Algebra.Homology.ShortComplex.RightHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.RightHomologyData.p_g'

English

If k and x satisfy a boundary relation k = g·x, then h.ι · h.descQ k = 0.

Русский

Если выполняется граница k = g·x, то h.ι · h.descQ k = 0.

LaTeX

$$$h.\iota \circ h.descQ(k,\, ) = 0$ при $k = g \circ x$$$

Lean4

@[reassoc (attr := simp)]
theorem p_g' : h.p ≫ h.g' = S.g :=
  p_descQ _ _ _

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

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

Разделы

Аффилиация

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