p_comp_d

Mathlib.CategoryTheory.Idempotents.HomologicalComplex

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

English

The composition P.p ≫ (f.f ≫ g.f) ≫ R.p reduces to f.f ≫ g.f by associativity and Karoubi-idempotence.

Русский

По ассоциации и идемпотентности Кароуоби композиция P.p ≫ (f.f ≫ g.f) ≫ R.p сводится к f.f ≫ g.f.

LaTeX

$$P.p ≫ (f.f ≫ g.f) ≫ R.p = f.f ≫ g.f$$

Lean4

@[simp, reassoc]
theorem p_comp_d : P.p.f n ≫ f.f.f n = f.f.f n :=
  HomologicalComplex.congr_hom (p_comp f) n

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

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

Разделы

Аффилиация

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