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

# Karoubi envelopes🔗

We give a construction of the **Karoubi envelope**
$C˜$
of a precategory
$C,$
a formal construction which adds a choice of splittings for every idempotent in
$C.$
Furthermore, the Karoubi envelope is the *smallest*
idempotent-complete category which admits a map from
$C,$
in the sense that any
$F:C→D$
into an idempotent-complete category
$D$
factors through
$C˜:$

Furthermore, the `embedding functor`

$C→C˜$
is fully
faithful.

The `objects`

in
$C˜$
are given by pairs of an object
$c:C$
and an idempotent
$f:c→c.$
A map between
$(c,f)$
and
$(d,g)$
is given by a map
$ϕ:c→d$
which absorbs
$f$
from the left and
$g$
from the right:
$ϕ∘f=ϕ=g∘ϕ.$

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
$(c,e)$
in
$C˜$
*isn’t* the identity in
$C,$
it’s the chosen idempotent
$e!$

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
$x↦(x,id);$
The morphism part of the functor has to send
$f:x→y$
to some
$f_{′}:x→y$
which absorbs
$id$
on either side; But this is just
$f$
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 $f:(A,e)→(A,e)$ admits a splitting in $C˜.$ First, note that since $f$ is (by assumption) idempotent, we have an object given by $(A,f);$ We’ll split $f$ as a map

$(A,e)→(A,f)→(A,e)$The first map is given by the underlying map of
$f:A→A.$
We must show that
$f∘e=f,$
but we have this by the definition of maps in
$C˜.$
In the other direction, we can *again* take
$f:A→A,$
which also satisfies
$e∘f=f.$

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
$f,$
we must show that
$f∘f=f$
as a map
$(A,e)→(A,e),$
which we have by assumption; And we must show that
$f∘f=id$
as a map
$(A,f)→(A,f).$
But recall that the identity on
$(A,f)$
is
$f,$
so we *also* have this by assumption!

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

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

If
$C$
was already idempotent-complete, then `Embed`

is an equivalence of
categories between
$C$
and
$C˜:$

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 senses^{1}!

it is a completion that

*adds*splittings of idempotents, and a completion that*is*idempotent↩︎