Theorems · Inductive type · category theory

CategoryTheory.Idempotents.Karoubi

(C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max u_1 v_1)

In a preadditive category C, when an object X decomposes as X ≅ P ⨿ Q, one may consider P as a direct factor of X and up to unique isomorphism, it is determined by the obvious idempotent X ⟶ P ⟶ X which is the projection onto P with kernel Q. More generally, one may define a formal direct factor of an object X : C : it consists of an idempotent p : X ⟶ X which is thought as the "formal image" of p. The type Karoubi C shall be the type of the objects of the karoubi envelope of C. It makes sense for any category C.

Defined in

Mathlib.CategoryTheory.Idempotents.Karoubi

Cited by

233 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category