p_comm

Mathlib.CategoryTheory.Idempotents.Karoubi

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

English

Associativity-related simplification: P.p ≫ (f.f ≫ g.f) ≫ R.p simplifies to f.f ≫ g.f.

Русский

Упрощение по ассоциации: 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

@[reassoc]
theorem p_comm {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f ≫ Q.p := by rw [p_comp, comp_p]

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

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

Разделы

Аффилиация

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