open import Cat.Prelude

module Cat.Diagram.Idempotent {o h} (C : Precategory o h) where

open import Cat.Reasoning C
private variable
A B : Ob
f : Hom A B


# Idempotentsπ

Idempotents are the categorical generalisation of projections, in the sense of linear algebra. Formally, an idempotent is a map with Keeping in line with the view that an idempotent is like a projection, we can ask what it projects onto: We would then have some subobject of fixed elements, and a decomposition of as

When this is the case, we say that is a split idempotent: We have some pair of maps (the βprojectorβ) and with and

is-idempotent : Hom A A β Type _
is-idempotent e = e β e β‘ e

record is-split (e : Hom A A) : Type (o β h) where
field
{F}     : Ob
project : Hom A F
inject  : Hom F A

pβi : project β inject β‘ id
iβp : inject β project β‘ e

is-splitβis-idempotent : is-split f β is-idempotent f
is-splitβis-idempotent {f = f} spl =
f β f             β‘Λβ¨ apβ _β_ iβp iβp β©β‘Λ
(s β r) β (s β r) β‘β¨ cancel-inner pβi β©β‘
s β r             β‘β¨ iβp β©β‘
f                 β
where open is-split spl renaming (inject to s ; project to r)


Identities are always trivially (split) idempotent:

id-is-idempotent : β {A} β is-idempotent {A = A} id
id-is-idempotent = idr _

id-is-split : β {A} β is-split {A = A} id
id-is-split {A} .is-split.F = A
id-is-split .is-split.project = id
id-is-split .is-split.inject = id
id-is-split .is-split.pβi = idr _
id-is-split .is-split.iβp = idr _


Itβs not the case that idempotents are split in every category. Those where this is the case are called idempotent-complete. Every category can be embedded, by a fully faithful functor, into an idempotent-complete category; This construction is called the Karoubi envelope of

is-idempotent-complete : Type _
is-idempotent-complete = β {A} (f : Hom A A) β is-idempotent f β is-split f