module Cat.Instances.Karoubi {o h} (C : Precategory o h) where

Karoubi envelopes🔗

We give a construction of the Karoubi envelope of a precategory a formal construction which adds a choice of splittings for every idempotent in Furthermore, the Karoubi envelope is the smallest idempotent-complete category which admits a map from in the sense that any into an idempotent-complete category factors through

Furthermore, the embedding functor is fully faithful.

The objects in are given by pairs of an object and an idempotent A map between and is given by a map which absorbs from the left and from the right:

private
  KOb : Type (o  h)
  KOb = Σ[ c  C ] Σ[ f  C.Hom c c ] (is-idempotent f)

  KHom : KOb  KOb  Type h
  KHom (c , f , _) (d , g , _) = Σ[ φ  C.Hom c d ] ((φ C.∘ f  φ) × (g C.∘ φ  φ))

We can see that these data assemble into a precategory. However, note that the identity on in isn’t the identity in it’s the chosen idempotent

Karoubi : Precategory (o  h) h
Karoubi .Ob = KOb
Karoubi .Hom = KHom
Karoubi .Hom-set _ _ = hlevel 2

Karoubi .id {x = c , e , i} = e , i , i
Karoubi ._∘_ (f , fp , fp') (g , gp , gp') = f C.∘ g , C.pullr gp , C.pulll fp'

Karoubi .idr {x = _ , _ , i} {_ , _ , j} (f , p , q) = Σ-prop-path! p
Karoubi .idl {x = _ , _ , i} {_ , _ , j} (f , p , q) = Σ-prop-path! q
Karoubi .assoc {w = _ , _ , i} {z = _ , _ , j} _ _ _ = Σ-prop-path! (C.assoc _ _ _)

We can now define the embedding functor from C to its Karoubi envelope. It has object part The morphism part of the functor has to send to some which absorbs on either side; But this is just again.

Embed : Functor C Karoubi
Embed .F₀ x = x , C.id , id-is-idempotent
Embed .F₁ f = f , C.idr _ , C.idl _
Embed .F-id = Σ-prop-path! refl
Embed .F-∘ f g = Σ-prop-path! refl

An elementary argument shows that the morphism part of Embed has an inverse given by projecting the first component of the pair; Hence, Embed is fully faithful.

Embed-is-fully-faithful : is-fully-faithful Embed
Embed-is-fully-faithful = is-iso→is-equiv $
  iso fst  _  Σ-prop-path! refl) λ _  refl

Idempotent-completeness🔗

We now show that any idempotent admits a splitting in First, note that since is (by assumption) idempotent, we have an object given by We’ll split as a map

The first map is given by the underlying map of We must show that but we have this by the definition of maps in In the other direction, we can again take which also satisfies

is-idempotent-complete-Karoubi : CI.is-idempotent-complete Karoubi
is-idempotent-complete-Karoubi {A = A , e , i} (f , p , q) idem = spl where
  open CI.is-split

  f-idem : f C.∘ f  f
  f-idem i = idem i .fst

  spl : CI.is-split Karoubi (f , p , q)
  spl .F = A , f , f-idem
  spl .project = f , p , f-idem
  spl .inject = f , f-idem , q

For this to be a splitting of we must show that as a map which we have by assumption; And we must show that as a map But recall that the identity on is so we also have this by assumption!

  spl .p∘i = Σ-prop-path! f-idem
  spl .i∘p = Σ-prop-path! f-idem

Hence is an idempotent-complete category which admits as a full subcategory.

If was already idempotent-complete, then Embed is an equivalence of categories between and

Karoubi-is-completion : is-idempotent-complete  is-equivalence Embed
Karoubi-is-completion complete = ff+split-eso→is-equivalence Embed-is-fully-faithful eso where
  eso : is-split-eso Embed
  eso (c , e , ie) = c' , same where
    open is-split (complete e ie) renaming (F to c'; inject to i; project to p)
    module Karoubi = Cat.Morphism Karoubi
    open Inverses
    same : (c' , C.id , _) Karoubi.≅ (c , e , ie)
    same .to = i , C.idr _ , C.rswizzle (sym i∘p) p∘i
    same .from = p , C.lswizzle (sym i∘p) p∘i , C.idl _
    same .inverses .invl = Σ-prop-path! i∘p
    same .inverses .invr = Σ-prop-path! p∘i

This makes the Karoubi envelope an “idempotent completion” in two different technical senses1!


  1. it is a completion that adds splittings of idempotents, and a completion that is idempotent↩︎