p_comp

Mathlib.CategoryTheory.Idempotents.Karoubi

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

English

For any morphism f: P ⟶ Q in Karoubi C, f.f ≫ Q.p = f.f.

Русский

Для любого морфизма f: P ⟶ Q в Karoubi C выполняется f.f ≫ Q.p = f.f.

LaTeX

$$f.f ≫ Q.p = f.f$$

Lean4

@[reassoc (attr := simp)]
theorem p_comp {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f := by rw [← f.comm, ← assoc, P.idem]

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

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

Разделы

Аффилиация

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