Skip to content

Commit 04e1822

Browse files
JacquesCaretteJacquesCarette
authored
Merge pull request #263 from TOTBWF/karoubi-envelope
Idempotents, Split Idempotents and Karoubi Envelopes
2 parents 5fc0077 + 9b58c07 commit 04e1822

File tree

4 files changed

+271
-0
lines changed

4 files changed

+271
-0
lines changed

‎src/Categories/Category/Construction/KaroubiEnvelope.agda‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Category using (Category; _[_≈_])
4+
5+
-- Karoubi Envelopes. These are the free completions of categories under split idempotents
6+
module Categories.Category.Construction.KaroubiEnvelope {o ℓ e} (𝒞 : Category o ℓ e) where
7+
8+
open import Level
9+
10+
open import Categories.Morphism.Idempotent.Bundles 𝒞
11+
open import Categories.Morphism.Reasoning 𝒞
12+
13+
private
14+
module 𝒞 = Category 𝒞
15+
open 𝒞.HomReasoning
16+
open 𝒞.Equiv
17+
18+
open Idempotent
19+
open Idempotent⇒
20+
21+
KaroubiEnvelope : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
22+
KaroubiEnvelope = record
23+
{ Obj = Idempotent
24+
; _⇒_ = Idempotent⇒
25+
; _≈_ = λ f g → 𝒞 [ Idempotent⇒.hom f ≈ Idempotent⇒.hom g ]
26+
; id = id
27+
; _∘_ = _∘_
28+
; assoc = 𝒞.assoc
29+
; sym-assoc = 𝒞.sym-assoc
30+
; identityˡ = λ {I} {J} {f} → absorbˡ f
31+
; identityʳ = λ {I} {J} {f} → absorbʳ f
32+
; identity² = λ {I} → idempotent I
33+
; equiv = record
34+
{ refl = refl
35+
; sym = sym
36+
; trans = trans
37+
}
38+
; ∘-resp-≈ = 𝒞.∘-resp-≈
39+
}

‎src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Category.Core
4+
5+
module Categories.Category.Construction.KaroubiEnvelope.Properties {o ℓ e} (𝒞 : Category o ℓ e) where
6+
7+
open import Data.Product using (_,_)
8+
9+
open import Categories.Functor renaming (id to idF)
10+
open import Categories.Functor.Properties
11+
12+
open import Categories.Category.Construction.KaroubiEnvelope
13+
14+
open import Categories.Morphism.Idempotent
15+
import Categories.Morphism.Idempotent.Bundles as BundledIdem
16+
17+
open Category 𝒞
18+
open Equiv
19+
20+
--------------------------------------------------------------------------------
21+
-- Some facts about embedding 𝒞 into it's Karoubi Envelope
22+
23+
KaroubiEmbedding : Functor 𝒞 (KaroubiEnvelope 𝒞)
24+
KaroubiEmbedding = record
25+
{ F₀ = λ X → record
26+
{ obj = X
27+
; isIdempotent = record
28+
{ idem = id
29+
; idempotent = identity²
30+
}
31+
}
32+
; F₁ = λ f → record
33+
{ hom = f
34+
; absorbˡ = identityˡ
35+
; absorbʳ = identityʳ
36+
}
37+
; identity = refl
38+
; homomorphism = refl
39+
; F-resp-≈ = λ eq → eq
40+
}
41+
42+
private
43+
module KaroubiEmbedding = Functor KaroubiEmbedding
44+
45+
karoubi-embedding-full : Full KaroubiEmbedding
46+
karoubi-embedding-full = record
47+
{ from = record
48+
{ _⟨$⟩_ = λ f → BundledIdem.Idempotent⇒.hom f
49+
; cong = λ eq → eq
50+
}
51+
; right-inverse-of = λ _ → refl
52+
}
53+
54+
karoubi-embedding-faithful : Faithful KaroubiEmbedding
55+
karoubi-embedding-faithful f g eq = eq
56+
57+
karoubi-embedding-fully-faithful : FullyFaithful KaroubiEmbedding
58+
karoubi-embedding-fully-faithful = karoubi-embedding-full , karoubi-embedding-faithful
59+
60+
--------------------------------------------------------------------------------
61+
-- Some facts about splitting idempotents
62+
63+
-- All idempotents in the Karoubi Envelope are split
64+
idempotent-split : ∀ {A} → Idempotent (KaroubiEnvelope 𝒞) A → SplitIdempotent (KaroubiEnvelope 𝒞) A
65+
idempotent-split {A} I = record
66+
{ idem = idem
67+
; isSplitIdempotent = record
68+
{ obj = record
69+
{ isIdempotent = record
70+
{ idem = idem.hom
71+
; idempotent = idempotent
72+
}
73+
}
74+
; retract = record
75+
{ hom = idem.hom
76+
; absorbˡ = idempotent
77+
; absorbʳ = idem.absorbʳ
78+
}
79+
; section = record
80+
{ hom = idem.hom
81+
; absorbˡ = idem.absorbˡ
82+
; absorbʳ = idempotent
83+
}
84+
; retracts = idempotent
85+
; splits = idempotent
86+
}
87+
}
88+
where
89+
module A = BundledIdem.Idempotent A
90+
open Idempotent I
91+
module idem = BundledIdem.Idempotent⇒ idem

‎src/Categories/Morphism/Idempotent.agda‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Category.Core
4+
5+
-- Idempotents and Split Idempotents
6+
module Categories.Morphism.Idempotent {o ℓ e} (𝒞 : Category o ℓ e) where
7+
8+
open import Level
9+
10+
open import Categories.Morphism 𝒞
11+
open import Categories.Morphism.Reasoning 𝒞
12+
13+
open Category 𝒞
14+
open HomReasoning
15+
16+
record Idempotent (A : Obj) : Set (ℓ ⊔ e) where
17+
field
18+
idem : A ⇒ A
19+
idempotent : idem ∘ idem ≈ idem
20+
21+
record IsSplitIdempotent {A : Obj} (i : A ⇒ A) : Set (o ⊔ ℓ ⊔ e) where
22+
field
23+
{obj} : Obj
24+
retract : A ⇒ obj
25+
section : obj ⇒ A
26+
retracts : retract ∘ section ≈ id
27+
splits : section ∘ retract ≈ i
28+
29+
retract-absorb : retract ∘ i ≈ retract
30+
retract-absorb = begin
31+
retract ∘ i ≈˘⟨ refl⟩∘⟨ splits ⟩
32+
retract ∘ section ∘ retract ≈⟨ cancelˡ retracts ⟩
33+
retract ∎
34+
35+
section-absorb : i ∘ section ≈ section
36+
section-absorb = begin
37+
i ∘ section ≈˘⟨ splits ⟩∘⟨refl ⟩
38+
(section ∘ retract) ∘ section ≈⟨ cancelʳ retracts ⟩
39+
section ∎
40+
41+
idempotent : i ∘ i ≈ i
42+
idempotent = begin
43+
i ∘ i ≈˘⟨ splits ⟩∘⟨ splits ⟩
44+
(section ∘ retract) ∘ (section ∘ retract) ≈⟨ cancelInner retracts ⟩
45+
section ∘ retract ≈⟨ splits ⟩
46+
i ∎
47+
48+
record SplitIdempotent (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
49+
field
50+
idem : A ⇒ A
51+
isSplitIdempotent : IsSplitIdempotent idem
52+
53+
open IsSplitIdempotent isSplitIdempotent public
54+
55+
-- All split idempotents are idempotent
56+
SplitIdempotent⇒Idempotent : ∀ {A} → SplitIdempotent A → Idempotent A
57+
SplitIdempotent⇒Idempotent Split = record { Split }
58+
where
59+
module Split = SplitIdempotent Split
60+
61+
module _ {A} {f : A ⇒ A} (S T : IsSplitIdempotent f) where
62+
private
63+
module S = IsSplitIdempotent S
64+
module T = IsSplitIdempotent T
65+
66+
split-idempotent-unique : S.obj ≅ T.obj
67+
split-idempotent-unique = record
68+
{ from = T.retract ∘ S.section
69+
; to = S.retract ∘ T.section
70+
; iso = record
71+
{ isoˡ = begin
72+
(S.retract ∘ T.section) ∘ (T.retract ∘ S.section) ≈⟨ center T.splits ⟩
73+
S.retract ∘ f ∘ S.section ≈⟨ pullˡ S.retract-absorb ⟩
74+
S.retract ∘ S.section ≈⟨ S.retracts ⟩
75+
id ∎
76+
; isoʳ = begin
77+
(T.retract ∘ S.section) ∘ (S.retract ∘ T.section) ≈⟨ center S.splits ⟩
78+
T.retract ∘ f ∘ T.section ≈⟨ pullˡ T.retract-absorb ⟩
79+
T.retract ∘ T.section ≈⟨ T.retracts ⟩
80+
id ∎
81+
}
82+
}

‎src/Categories/Morphism/Idempotent/Bundles.agda‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Category using (Category; _[_,_]; _[_∘_]; _[_≈_])
4+
5+
-- Bundled versions of Idempotents, as well as maps between idempotents.
6+
module Categories.Morphism.Idempotent.Bundles {o ℓ e} (𝒞 : Category o ℓ e) where
7+
8+
open import Level
9+
10+
import Categories.Morphism.Idempotent 𝒞 as Idem
11+
open import Categories.Morphism.Reasoning 𝒞
12+
13+
private
14+
module 𝒞 = Category 𝒞
15+
open 𝒞.HomReasoning
16+
open 𝒞.Equiv
17+
18+
--------------------------------------------------------------------------------
19+
-- Bundled Idempotents, and maps between them
20+
21+
record Idempotent : Set (o ⊔ ℓ ⊔ e) where
22+
field
23+
{obj} : 𝒞.Obj
24+
isIdempotent : Idem.Idempotent obj
25+
26+
open Idem.Idempotent isIdempotent public
27+
28+
open Idempotent
29+
30+
record Idempotent⇒ (I J : Idempotent) : Set (ℓ ⊔ e) where
31+
private
32+
module I = Idempotent I
33+
module J = Idempotent J
34+
field
35+
hom : 𝒞 [ I.obj , J.obj ]
36+
absorbˡ : 𝒞 [ 𝒞 [ J.idem ∘ hom ] ≈ hom ]
37+
absorbʳ : 𝒞 [ 𝒞 [ hom ∘ I.idem ] ≈ hom ]
38+
39+
open Idempotent⇒
40+
41+
--------------------------------------------------------------------------------
42+
-- Identity and Composition of maps between Idempotents
43+
44+
id : ∀ {I} → Idempotent⇒ I I
45+
id {I} = record
46+
{ hom = idem I
47+
; absorbˡ = idempotent I
48+
; absorbʳ = idempotent I
49+
}
50+
51+
_∘_ : ∀ {I J K} → (f : Idempotent⇒ J K) → (g : Idempotent⇒ I J) → Idempotent⇒ I K
52+
_∘_ {I} {J} {K} f g = record
53+
{ hom = 𝒞 [ f.hom ∘ g.hom ]
54+
; absorbˡ = pullˡ f.absorbˡ
55+
; absorbʳ = pullʳ g.absorbʳ
56+
}
57+
where
58+
module f = Idempotent⇒ f
59+
module g = Idempotent⇒ g

0 commit comments

Comments
 (0)