p_comm_f

Mathlib.CategoryTheory.Idempotents.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f

English

For every P in Karoubi(HomologicalComplex C c) and index n, P.p.f n is idempotent: P.p.f n ≫ P.p.f n = P.p.f n.

Русский

Для каждого P в Karoubi(HomologicalComplex C c) и индекса n, P.p.f n является идемпотентом: P.p.f n ∘ P.p.f n = P.p.f n.

LaTeX

$$P.p.f n ≫ P.p.f n = P.p.f n$$

Lean4

@[reassoc]
theorem p_comm_f : P.p.f n ≫ f.f.f n = f.f.f n ≫ Q.p.f n :=
  HomologicalComplex.congr_hom (p_comm f) n

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

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

Разделы

Аффилиация

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