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


Idempotents are the categorical generalisation of projections, in the sense of linear algebra. Formally, an idempotent e:Aβ†’Ae : A \to A is a map with e∘e=ee \circ e = e. 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 FF of fixed elements, and a decomposition of ee as

Xβ†’Fβ†ͺX X \to F \hookrightarrow X

When this is the case, we say that ee is a split idempotent: We have some pair of maps p:Xβ†’Fp : X \to F (the β€œprojector”) and i:Fβ†’Xi : F \to X, with r∘i=id⁑r \circ i = \operatorname{id}_{} and i∘r=ei \circ r = e.

is-idempotent : Hom A A β†’ Type _
is-idempotent e = e ∘ e ≑ e

record is-split (e : Hom A A) : Type (o βŠ” h) where
    {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 C\mathcal{C}.

is-idempotent-complete : Type _
is-idempotent-complete = βˆ€ {A} (f : Hom A A) β†’ is-idempotent f β†’ is-split f