open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Diagram.Idempotent as CI

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

Karoubi envelopesπŸ”—

We give a construction of the Karoubi envelope C˜\~\mathcal{C} of a precategory C\mathcal{C}, a formal construction which adds a choice of splittings for every idempotent in C\mathcal{C}. Furthermore, the Karoubi envelope is the smallest idempotent-complete category which admits a map from C\mathcal{C}, in the sense that any F:Cβ†’DF : \mathcal{C} \to \mathcal{D} into an idempotent-complete category D\mathcal{D} factors through C˜\~\mathcal{C}:

Cβ†ͺCΛœβ†’D \mathcal{C} {\hookrightarrow}\~\mathcal{C} \to \mathcal{D}

Furthermore, the embedding functor Cβ†’C˜\mathcal{C} \to \~\mathcal{C} is fully faithful.

The objects in C˜\~\mathcal{C} are given by pairs of an object c:Cc : \mathcal{C} and an idempotent f:cβ†’cf : c \to c. A map between (c,f)(c,f) and (d,g)(d,g) is given by a map Ο•:cβ†’d\phi : c \to d which absorbs ff from the left and gg from the right: Ο•βˆ˜f=Ο•=gβˆ˜Ο•\phi \circ f = \phi = g \circ \phi.

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 (c,e)(c,e) in C˜\~\mathcal{C} isn’t the identity in CC, it’s the chosen idempotent ee!

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 x↦(x,id)x \mapsto (x, {{\mathrm{id}}_{}}); The morphism part of the functor has to send f:xβ†’yf : x \to y to some fβ€²:xβ†’yf' : x \to y which absorbs id{{\mathrm{id}}_{}} on either side; But this is just ff again.

Embed : Functor C Karoubi
Embed .Fβ‚€ x = x , C.id , C.idr _
Embed .F₁ f = f , C.idr _ , C.idl _
Embed .F-id = KH≑ {ai = C.idl _} {bi = C.idl _} refl
Embed .F-∘ f g = KH≑ {ai = C.idl _} {bi = C.idl _} 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 f:(A,e)β†’(A,e)f : (A, e) \to (A, e) admits a splitting in C˜\~\mathcal{C}. First, note that since ff is (by assumption) idempotent, we have an object given by (A,f)(A, f); We’ll split ff as a map

(A,e)β†’(A,f)β†’(A,e) (A, e) \to (A, f) \to (A, e)

The first map is given by the underlying map of f:Aβ†’Af : A \to A. We must show that f∘e=ff \circ e = f, but we have this by the definition of maps in C˜\~\mathcal{C}. In the other direction, we can again take f:Aβ†’Af : A \to A, which also satisfies e∘f=fe \circ 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 ff, we must show that f∘f=ff \circ f = f as a map (A,e)β†’(A,e)(A, e) \to (A, e), which we have by assumption; And we must show that f∘f=idf \circ f = {{\mathrm{id}}_{}} as a map (A,f)β†’(A,f)(A, f) \to (A, f). But recall that the identity on (A,f)(A, f) is ff, 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 C˜\~\mathcal{C} is an idempotent-complete category which admits CC as a full subcategory.