p_descQ

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

English

For right homology data, the map p followed by descQ recovers the original morphism: p ≫ descQ k hk = k.

Русский

Для правой гомологической структуры: p ≫ descQ k hk = k.

LaTeX

$$$h.p \;\circ\; h.descQ k hk = k$$$

Lean4

@[reassoc (attr := simp)]
theorem p_descQ (k : S.X₂ ⟶ A) (hk : S.f ≫ k = 0) : h.p ≫ h.descQ k hk = k :=
  h.hp.fac _ WalkingParallelPair.one

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

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

Разделы

Аффилиация

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