PInfty_f_add_QInfty_f

Mathlib.AlgebraicTopology.DoldKan.PInfty

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

English

In each degree n, the sum PInfty.f n + QInfty.f n is the identity on X_n.

Русский

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

LaTeX

$$$ (PInfty.f n) + (QInfty.f n) = \mathrm{Id}_{X_n} $$$

Lean4

theorem PInfty_f_add_QInfty_f (n : ℕ) : (PInfty.f n : X _⦋n⦌ ⟶ _) + QInfty.f n = 𝟙 _ :=
  HomologicalComplex.congr_hom PInfty_add_QInfty n

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

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

Разделы

Аффилиация

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