decompId_p_naturality

Mathlib.CategoryTheory.Idempotents.Karoubi

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

English

Naturality of the split epi decompId_p with respect to morphisms.

Русский

Естественная совместимость разложения m с decompId_p по отношению к морфизмам.

LaTeX

$$$decompId_p P \circ f = (\mathrm{Hom.mk} f.f) \circ decompId_p Q$$$

Lean4

theorem decompId_p_naturality {P Q : Karoubi C} (f : P ⟶ Q) :
    decompId_p P ≫ f = (by exact Hom.mk f.f (by simp)) ≫ decompId_p Q := by simp

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

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

Разделы

Аффилиация

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