P_add_Q_f

Mathlib.AlgebraicTopology.DoldKan.Projections

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

English

In each degree n, the sum P q.f n + Q q.f n equals the identity on X_n.

Русский

В каждой степени n сумма P q.f n и Q q.f n равна тождественному отображению на X_n.

LaTeX

$$$ (P_q.f_n) + (Q_q.f_n) = \mathrm{Id}_{X_n} $$$

Lean4

theorem P_add_Q_f (q n : ℕ) : (P q).f n + (Q q).f n = 𝟙 (X _⦋n⦌) :=
  HomologicalComplex.congr_hom (P_add_Q q) n

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

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

Разделы

Аффилиация

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