Documentation

Mathlib.CategoryTheory.Idempotents.Basic

Idempotent complete categories #

In this file, we define the notion of idempotent complete categories (also known as Karoubian categories, or pseudoabelian in the case of preadditive categories).

Main definitions #

References #

A category is idempotent complete iff all idempotent endomorphisms p split as a composition p = e ≫ i with i ≫ e = 𝟙 _

Instances

    A category is idempotent complete iff all idempotent endomorphisms p split as a composition p = e ≫ i with i ≫ e = 𝟙 _

    A category is idempotent complete iff for all idempotent endomorphisms, the equalizer of the identity and this idempotent exists.

    @[instance 100]

    An abelian category is idempotent complete.

    Equations
    • ⋯ = ⋯