decompId_p

Mathlib.CategoryTheory.Idempotents.Karoubi

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

← MathLib Explorer

English

The split epi in the factorisation of identity on P is decompId_p P.

Русский

Сепарационный эпиморфизм в факторизации тождества на P есть decompId_p P.

LaTeX

$$$decompId_p P: (P.X: Karoubi C) \to P$$$

Lean4

/-- The split epi which appears in the factorisation `decompId P`. -/
@[simps]
def decompId_p (P : Karoubi C) : (P.X : Karoubi C) ⟶ P :=
  ⟨P.p, by rw [coe_p, id_comp, P.idem]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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