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.Ob ] Σ[ 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.∘ φ ≡ φ)) KH≡ : ∀ {a b : C.Ob} {af : C.Hom a a} {bf : C.Hom b b} {ai : is-idempotent af} {bi : is-idempotent bf} {f g : KHom (a , af , ai) (b , bf , bi)} → fst f ≡ fst g → f ≡ g KH≡ = Σ-prop-path (λ _ → hlevel 1)
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) = KH≡ {ai = i} {bi = j} p Karoubi .idl {x = _ , _ , i} {_ , _ , j} (f , p , q) = KH≡ {ai = i} {bi = j} q Karoubi .assoc {w = _ , _ , i} {z = _ , _ , j} _ _ _ = KH≡ {ai = i} {bi = j} (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 = KH≡ {ai = id-is-idempotent} {bi = id-is-idempotent} refl Embed .F-∘ f g = KH≡ {ai = id-is-idempotent} {bi = id-is-idempotent} 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 (λ _ → hlevel 1) 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 = KH≡ {ai = f-idem} {bi = f-idem} f-idem spl .i∘p = KH≡ {ai = i} {bi = i} 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 = KH≡ {ai = ie} {bi = ie} i∘p same .inverses .invr = KH≡ {ai = id-is-idempotent} {bi = id-is-idempotent} p∘i
This makes the Karoubi envelope an “idempotent completion” in two different technical senses1!
it is a completion that adds splittings of idempotents, and a completion that is idempotent↩︎