decompId_i_naturality

Mathlib.CategoryTheory.Idempotents.Karoubi

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

English

Naturality of the split mono decompId_i with respect to morphisms.

Русский

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

LaTeX

$$$f \circ decompId_i = decompId_i \circ (\text{Hom.mk} f.f)$$$

Lean4

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

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

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

Разделы

Аффилиация

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