Q_succ

Mathlib.AlgebraicTopology.DoldKan.Projections

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.DoldKan.Q_succ

English

A lemma expressing PInfty behavior in the Karoubi setting via Y.p and natTransPInfty_f.

Русский

Лемма о поведении PInfty в Каруоби-ситуации через Y.p и natTransPInfty_f.

LaTeX

$$$ ((PInfty.f n).f) = Y.p.app (op ⟦n⟧) \circ (PInfty : K[Y.X] ⟶ _).f n $$$

Lean4

theorem Q_succ (q : ℕ) : (Q (q + 1) : K[X] ⟶ _) = Q q - P q ≫ Hσ q :=
  by
  simp only [Q, P_succ, comp_add, comp_id]
  abel

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

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

Разделы

Аффилиация

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