Documentation

Mathlib.CategoryTheory.Idempotents.Karoubi

The Karoubi envelope of a category #

In this file, we define the Karoubi envelope Karoubi C of a category C.

Main constructions and definitions #

  • X : C

    an object of the underlying category

  • p : s.X s.X

    an endomorphism of the object

  • the condition that the given endomorphism is an idempotent

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 : XX 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.

Instances For

    A morphism P ⟶ Q in the category Karoubi C is a morphism in the underlying category C which satisfies a relation, which in the preadditive case, expresses that it induces a map between the corresponding "formal direct factors" and that it vanishes on the complement formal direct factor.

    Instances For

      It is possible to coerce an object of C into an object of Karoubi C. See also the functor toKaroubi.

      The obvious fully faithful functor toKaroubi sends an object X : C to the obvious formal direct factor of X given by 𝟙 X.

      Instances For

        The map sending f : P ⟶ Q to f.f : P.X ⟶ Q.X is additive.

        Instances For