open import Cat.Prelude

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:AAe : A \to A is a map with ee=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

XFX X \to F \mono X

When this is the case, we say that ee is a split idempotent: We have some pair of maps p:XFp : X \to F (the “projector”) and i:FXi : F \to X, with ri=idr \circ i = \id{id} and ir=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 
  where open is-split spl renaming (inject to s ; project to r)

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 full and faithful functor, into an idempotent-complete category; This construction is called the Karoubi envelope of C\ca{C}.

is-idempotent-complete : Type _
is-idempotent-complete =  {A} (f : Hom A A)  is-idempotent f  is-split f