complement

Mathlib.CategoryTheory.Idempotents.Biproducts

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

Lean4

/-- `P.complement` is the formal direct factor of `P.X` given by the idempotent
endomorphism `𝟙 P.X - P.p` -/
@[simps]
def complement (P : Karoubi C) : Karoubi C where
  X := P.X
  p := 𝟙 _ - P.p
  idem := idem_of_id_sub_idem P.p P.idem

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

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

Разделы

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

Аффилиация

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