Skip to content

Commit 73279ca

Browse files
plt-amyplt-amy
committed
defn: beck coequalisers
1 parent 6225bd7 commit 73279ca

File tree

2 files changed

+299
-15
lines changed

2 files changed

+299
-15
lines changed

‎src/Cat/Functor/Adjoint/Monad.lagda.md‎

Lines changed: 20 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ open _=>_
1010

1111
# The Monad from an Adjunction
1212

13-
```
13+
```agda
1414
module
1515
Cat.Functor.Adjoint.Monad
1616
{o₁ h₁ o₂ h₂ : _}
@@ -31,15 +31,15 @@ private
3131
Every adjunction $L \dashv R$ gives rise to a monad, where the
3232
underlying functor is $R \circ L$.
3333

34-
```
34+
```agda
3535
Adjunction→Monad : Monad C
3636
Adjunction→Monad .M = R F∘ L
3737
```
3838

3939
The unit of the monad is just adjunction monad, and the multiplication
4040
comes from the counit.
4141

42-
```
42+
```agda
4343
Adjunction→Monad .unit = adj.unit
4444
Adjunction→Monad .mult = NT (λ x → R.₁ (η adj.counit (L.₀ x))) λ x y f →
4545
R.₁ (adj.counit.ε (L.₀ y)) C.∘ R.₁ (L.₁ (R.₁ (L.₁ f))) ≡⟨ sym (R.F-∘ _ _) ⟩
@@ -52,22 +52,27 @@ The monad laws follow from the zig-zag identities. In fact, the
5252
`right-ident`{.Agda}ity law is exactly the `zag`{.Agda ident="adj.zag"}
5353
identity.
5454

55-
```
55+
```agda
5656
Adjunction→Monad .right-ident {x} = adj.zag
5757
```
5858

5959
The others are slightly more involved.
6060

61-
```
62-
Adjunction→Monad .left-ident =
63-
R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ (adj.unit.η _)) ≡⟨ sym (R.F-∘ _ _) ⟩
64-
R.₁ (adj.counit.ε _ D.∘ L.₁ (adj.unit.η _)) ≡⟨ ap R.₁ adj.zig ⟩
65-
R.₁ D.id ≡⟨ R.F-id ⟩
66-
C.id ∎
61+
```agda
62+
Adjunction→Monad .left-ident {x} = path where abstract
63+
path : R.₁ (adj.counit.ε (L.F₀ x)) C.∘ R.₁ (L.₁ (adj.unit.η x)) ≡ C.id
64+
path =
65+
R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ (adj.unit.η _)) ≡⟨ sym (R.F-∘ _ _) ⟩
66+
R.₁ (adj.counit.ε _ D.∘ L.₁ (adj.unit.η _)) ≡⟨ ap R.₁ adj.zig ⟩
67+
R.₁ D.id ≡⟨ R.F-id ⟩
68+
C.id ∎
6769
68-
Adjunction→Monad .mult-assoc =
69-
R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ (R.₁ (adj.counit.ε _))) ≡⟨ sym (R.F-∘ _ _) ⟩
70-
R.₁ (adj.counit.ε _ D.∘ L.₁ (R.₁ (adj.counit.ε _))) ≡⟨ ap R.₁ (adj.counit.is-natural _ _ _) ⟩
71-
R.₁ (adj.counit.ε _ D.∘ adj.counit.ε _) ≡⟨ R.F-∘ _ _ ⟩
72-
R.₁ (adj.counit.ε _) C.∘ R.₁ (adj.counit.ε _) ∎
70+
Adjunction→Monad .mult-assoc {x} = path where abstract
71+
path : R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ (R.₁ (adj.counit.ε (L.F₀ x))))
72+
≡ R.₁ (adj.counit.ε _) C.∘ R.₁ (adj.counit.ε (L .F₀ (R.F₀ (L.F₀ x))))
73+
path =
74+
R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ (R.₁ (adj.counit.ε _))) ≡⟨ sym (R.F-∘ _ _) ⟩
75+
R.₁ (adj.counit.ε _ D.∘ L.₁ (R.₁ (adj.counit.ε _))) ≡⟨ ap R.₁ (adj.counit.is-natural _ _ _) ⟩
76+
R.₁ (adj.counit.ε _ D.∘ adj.counit.ε _) ≡⟨ R.F-∘ _ _ ⟩
77+
R.₁ (adj.counit.ε _) C.∘ R.₁ (adj.counit.ε _) ∎
7378
```

‎src/Cat/Functor/Monadic/Beck.lagda.md‎

Lines changed: 279 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,279 @@
1+
```agda
2+
open import Cat.Functor.Adjoint.Monadic
3+
open import Cat.Functor.Adjoint.Monad
4+
open import Cat.Diagram.Coequaliser
5+
open import Cat.Functor.Adjoint
6+
open import Cat.Diagram.Monad
7+
open import Cat.Prelude
8+
9+
import Cat.Functor.Reasoning as F-r
10+
import Cat.Reasoning as C-r
11+
12+
module
13+
Cat.Functor.Monadic.Beck
14+
{o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
15+
(F : Functor C D) (G : Functor D C)
16+
(F⊣G : F ⊣ G)
17+
where
18+
```
19+
20+
<!--
21+
```agda
22+
private
23+
module F = F-r F
24+
module G = F-r G
25+
module C = C-r C
26+
module D = C-r D
27+
module GF = F-r (G F∘ F)
28+
module T = Monad (Adjunction→Monad F⊣G)
29+
private
30+
T : Monad C
31+
T = Adjunction→Monad F⊣G
32+
C^T : Precategory _ _
33+
C^T = Eilenberg-Moore C T
34+
open _⊣_ F⊣G
35+
open _=>_
36+
open Algebra-hom
37+
open Algebra-on
38+
```
39+
-->
40+
41+
# Beck's coequaliser
42+
43+
Let $(F \dashv U) : \ca{C} \leftrightarrows \ca{D}$ be a pair of
44+
[adjoint functors]. Recall that every such adjunction [induces] a
45+
[monad] $T$ (which we will abbreviate by $T$) on the category $\ca{C}$,
46+
and a "[comparison]" functor $K : \ca{C} \to \ca{C}^{T}$ into the
47+
[Eilenberg-Moore category] of $T$. In this module we will lay out a
48+
sufficient condition for the functor $K to have a left adjoint, which we
49+
denote $K^{-1}$. Let us first establish a result about the presentation
50+
of $T$-[algebras] by "generators and relations".
51+
52+
[monad]: Cat.Diagram.Monad.html
53+
[induces]: Cat.Functor.Adjoint.Monad.html
54+
[adjoint functors]: Cat.Functor.Adjoint.html
55+
[comparison]: Cat.Functor.Adjoint.Monadic.html
56+
[algebras]: Cat.Diagram.Monad.html#algebras-over-a-monad
57+
[Eilenberg-Moore category]: Cat.Diagram.Monad.html#eilenberg-moore-category
58+
59+
Suppose that we are given a $T$-algebra $(A, \nu)$. Note that $(TA,
60+
\mu)$ is also a $T$-algebra, namely the free $T$-algebra on the object
61+
$A$. Let us illustrate this with a concrete example: Suppose we have the
62+
cyclic group $\bb{Z}/n\bb{Z}$, for some natural number $n$, which we
63+
regard as a subgroup of $\bb{Z}$. The corresponding algebra $(TA, \mu)$
64+
would be the [free group] on one generator --- the group of integers
65+
---, whence we conclude that, in general, this $(TA, \mu)$ algebra
66+
is very far from being the $(A, \nu)$ algebra we started with.
67+
68+
[free group]: Algebra.Group.Free.html
69+
70+
Still thinking about our $\bb{Z}/n\bb{Z}$ example, it feels like we
71+
should be able to [quotient] the algebra $(TA, \mu)$ by some set of
72+
_relations_ and get back the algebra $(A, \nu)$ we started with. This is
73+
absolutely true, and it's true even when the category of $T$-algebras is
74+
lacking in quotients! In particular, we have the following theorem:
75+
76+
[quotient]: Data.Set.Coequaliser.html#quotients
77+
78+
**Theorem**. Every $T$-algebra $(A, \nu)$ is the [coequaliser] of the diagram
79+
80+
[coequaliser]: Cat.Diagram.Coequaliser.html
81+
82+
~~~{.quiver .short-1}
83+
\[\begin{tikzcd}
84+
{(T^2A,\mu)} & {(TA,\mu)} & {(A,\nu)}
85+
\arrow["\mu", shift left=1, from=1-1, to=1-2]
86+
\arrow["T\nu"', shift right=1, from=1-1, to=1-2]
87+
\arrow[from=1-2, to=1-3]
88+
\end{tikzcd}\]
89+
~~~
90+
91+
Furthermore, the arrows $\mu$ and $T\nu$ have a common left inverse, so
92+
this is a reflexive coequaliser, called the **Beck coequaliser**.
93+
94+
<!--
95+
```agda
96+
module _ (Aalg : Algebra C T) where
97+
private
98+
A = Aalg .fst
99+
module A = Algebra-on (Aalg .snd)
100+
101+
TA : Algebra C T
102+
TA = Free C T .Functor.F₀ A
103+
104+
TTA : Algebra C T
105+
TTA = Free C T .Functor.F₀ (T.M₀ A)
106+
107+
mult : Algebra-hom C T TTA TA
108+
mult .morphism = T.mult .η _
109+
mult .commutes = sym T.mult-assoc
110+
111+
fold : Algebra-hom C T TTA TA
112+
fold .morphism = T.M₁ A.ν
113+
fold .commutes =
114+
T.M₁ A.ν C.∘ T.mult .η _ ≡˘⟨ T.mult .is-natural _ _ _ ⟩
115+
T.mult .η _ C.∘ T.M₁ (T.M₁ A.ν) ∎
116+
```
117+
-->
118+
119+
The calculation is just.. well, calculation, so we present it without
120+
much further commentary. Observe that $\nu$ coequalises $\mu$ and $T\nu$
121+
essentially by the definition of being an algebra map.
122+
123+
```agda
124+
open is-coequaliser
125+
algebra-is-coequaliser
126+
: is-coequaliser C^T {A = TTA} {B = TA} {E = Aalg}
127+
mult fold (record { morphism = A.ν ; commutes = sym A.ν-mult })
128+
algebra-is-coequaliser .coequal = Algebra-hom-path C $
129+
A.ν C.∘ T.mult .η _ ≡˘⟨ A.ν-mult ⟩
130+
A.ν C.∘ T.M₁ A.ν ∎
131+
```
132+
133+
The colimiting map from $(A, \nu)$ to some other algebra $(F, \nu')$
134+
which admits a map $e' : (TA, \mu) \to (F, \nu')$ is given by the
135+
composite
136+
137+
$$
138+
A \xto{\eta} TA \xto{e'} F\text{,}
139+
$$
140+
141+
which is a map of algebras by a long computation, and satisfies the
142+
properties of a coequalising map by slightly shorter computations, which
143+
can be seen below. Uniqueness of this map follows almost immediately
144+
from the algebra laws.
145+
146+
```agda
147+
algebra-is-coequaliser .coequalise {F = F} {e'} p .morphism =
148+
e' .morphism C.∘ T.unit .η A
149+
algebra-is-coequaliser .coequalise {F = F} {e'} p .commutes =
150+
(e' .morphism C.∘ unit.η A) C.∘ A.ν ≡⟨ C.extendr (unit.is-natural _ _ _) ⟩
151+
(e' .morphism C.∘ T.M₁ A.ν) C.∘ unit.η (T.M₀ A) ≡˘⟨ ap morphism p C.⟩∘⟨refl ⟩
152+
(e' .morphism C.∘ T.mult .η A) C.∘ unit.η (T.M₀ A) ≡⟨ C.cancelr T.right-ident ⟩
153+
e' .morphism ≡⟨ C.intror (sym (T.M-∘ _ _) ∙ ap T.M₁ A.ν-unit ∙ T.M-id) ⟩
154+
e' .morphism C.∘ T.M₁ A.ν C.∘ T.M₁ (unit.η A) ≡⟨ C.pulll (sym (ap morphism p)) ⟩
155+
(e' .morphism C.∘ T.mult .η A) C.∘ T.M₁ (unit.η A) ≡⟨ C.pushl (e' .commutes) ⟩
156+
F .snd .ν C.∘ T.M₁ (e' .morphism) C.∘ T.M₁ (unit.η A) ≡˘⟨ C.refl⟩∘⟨ T.M-∘ _ _ ⟩
157+
F .snd .ν C.∘ T.M₁ (e' .morphism C.∘ unit.η A) ∎
158+
algebra-is-coequaliser .universal {F = F} {e'} {p} = Algebra-hom-path C $
159+
(e' .morphism C.∘ unit.η _) C.∘ A.ν ≡⟨ C.extendr (unit.is-natural _ _ _) ⟩
160+
(e' .morphism C.∘ T.M₁ A.ν) C.∘ unit.η _ ≡˘⟨ ap morphism p C.⟩∘⟨refl ⟩
161+
(e' .morphism C.∘ T.mult .η _) C.∘ unit.η _ ≡⟨ C.cancelr T.right-ident ⟩
162+
e' .morphism ∎
163+
algebra-is-coequaliser .unique {F = F} {e'} {p} {colim} q =
164+
Algebra-hom-path C $ sym $
165+
e' .morphism C.∘ unit.η A ≡⟨ ap morphism q C.⟩∘⟨refl ⟩
166+
(colim .morphism C.∘ A.ν) C.∘ unit.η A ≡⟨ C.cancelr A.ν-unit ⟩
167+
colim .morphism ∎
168+
```
169+
170+
# Presented algebras
171+
172+
The lemma above says that every algebra which exists can be presented by
173+
generators and relations; The relations are encoded by the pair of maps
174+
$T^2A \tto TA$ in Beck's coequaliser, above. But what about the
175+
converse? The following lemma says that, if every algebra presented by
176+
generators-and-relations (encoded by a parallel pair $T^2A \tto TA$) has
177+
a coequaliser _in $\ca{D}$_, then the comparison functor $\ca{D} \to
178+
\ca{C}^T$ has a left adjoint.
179+
180+
<!--
181+
```agda
182+
module _
183+
(has-coeq : (M : Algebra C T) → Coequaliser D (F.₁ (M .snd .ν)) (counit.ε _))
184+
where
185+
186+
open Coequaliser
187+
open Functor
188+
```
189+
-->
190+
191+
On objects, this left adjoint acts by sending each algebra $M$ to the
192+
coequaliser of (the diagram underlying) its Beck coequaliser. In a
193+
sense, this is "the best approximation in $\ca{D}$ of the algebra". The
194+
action on morphisms is uniquely determined since it's a map out of a
195+
coequaliser.
196+
197+
If we consider the comparison functor as being "the $T$-algebra
198+
underlying an object of $\ca{D}$", then the functor we construct below
199+
is the "free object of $\ca{D}$ on a $T$-algebra". Why is this
200+
adjunction relevant, though? Its failure to be an equivalence measures
201+
just how far our original adjunction is from being monadic, that is, how
202+
far $\ca{D}$ is from being the category of $T$-algebras.
203+
204+
```agda
205+
Comparison⁻¹ : Functor (Eilenberg-Moore C T) D
206+
Comparison⁻¹ .F₀ = coapex ⊙ has-coeq
207+
Comparison⁻¹ .F₁ {X} {Y} alg-map =
208+
has-coeq X .coequalise {e′ = e′} path where
209+
e′ : D.Hom (F.F₀ (X .fst)) (Comparison⁻¹ .F₀ Y)
210+
e′ = has-coeq Y .coeq D.∘ F.₁ (alg-map .morphism)
211+
```
212+
<!--
213+
```agda
214+
abstract
215+
path : e′ D.∘ F.₁ (X .snd .ν) ≡ e′ D.∘ counit.ε (F.₀ (X .fst))
216+
path =
217+
(has-coeq Y .coeq D.∘ F.₁ (alg-map .morphism)) D.∘ F.₁ (X .snd .ν) ≡⟨ D.pullr (F.weave (alg-map .commutes)) ⟩
218+
has-coeq Y .coeq D.∘ F.₁ (Y .snd .ν) D.∘ F.₁ (T.M₁ (alg-map .morphism)) ≡⟨ D.extendl (has-coeq Y .coequal) ⟩
219+
has-coeq Y .coeq D.∘ counit.ε _ D.∘ F.₁ (T.M₁ (alg-map .morphism)) ≡⟨ D.pushr (counit.is-natural _ _ _) ⟩
220+
(has-coeq Y .coeq D.∘ F.₁ (alg-map .morphism)) D.∘ counit.ε _ ∎
221+
Comparison⁻¹ .F-id {X} = sym $ has-coeq X .unique (F.elimr refl ∙ D.introl refl)
222+
Comparison⁻¹ .F-∘ {X} f g = sym $ has-coeq X .unique $ sym $
223+
D.pullr (has-coeq X .universal)
224+
·· D.pulll (has-coeq _ .universal)
225+
·· F.pullr refl
226+
227+
open _⊣_
228+
```
229+
-->
230+
231+
The adjunction unit and counit are again very simple, and it's evident
232+
to a human looking at them that they satisfy the triangle identities
233+
(and are algebra homomorphisms). Agda is not as easy to convince,
234+
though, so we leave the computation folded up for the bravest of
235+
readers.
236+
237+
```agda
238+
Comparison⁻¹⊣Comparison : Comparison⁻¹ ⊣ Comparison F⊣G
239+
Comparison⁻¹⊣Comparison .unit .η x .morphism =
240+
G.₁ (has-coeq _ .coeq) C.∘ T.unit .η _
241+
Comparison⁻¹⊣Comparison .counit .η x =
242+
has-coeq _ .coequalise (F⊣G .counit.is-natural _ _ _)
243+
```
244+
245+
<details>
246+
<summary>Nah, really, it's quite ugly.</summary>
247+
248+
```agda
249+
Comparison⁻¹⊣Comparison .unit .η x .commutes =
250+
C.pullr (T.unit .is-natural _ _ _)
251+
∙ G.extendl (has-coeq _ .coequal)
252+
∙ C.elimr (F⊣G .zag)
253+
∙ G.intror (F⊣G .zig)
254+
∙ G.weave (D.pulll (sym (F⊣G .counit.is-natural _ _ _)) ∙ D.pullr (sym (F.F-∘ _ _)))
255+
Comparison⁻¹⊣Comparison .unit .is-natural x y f = Algebra-hom-path C $
256+
(G.₁ (has-coeq y .coeq) C.∘ T.unit.η _) C.∘ f .morphism ≡⟨ C.pullr (T.unit.is-natural _ _ _) ⟩
257+
G.₁ (has-coeq y .coeq) C.∘ T.M₁ (f .morphism) C.∘ T.unit .η (x .fst) ≡⟨ C.pulll (sym (G.F-∘ _ _)) ⟩
258+
G.₁ (has-coeq y .coeq D.∘ F.₁ (f .morphism)) C.∘ T.unit .η (x .fst) ≡⟨ ap G.₁ (sym (has-coeq _ .universal)) C.⟩∘⟨refl ⟩
259+
G.₁ (has-coeq x .coequalise _ D.∘ has-coeq x .coeq) C.∘ T.unit .η (x .fst) ≡⟨ C.pushl (G.F-∘ _ _) ⟩
260+
G.₁ (has-coeq x .coequalise _) C.∘ G.₁ (has-coeq x .coeq) C.∘ T.unit.η _ ∎
261+
Comparison⁻¹⊣Comparison .counit .is-natural x y f =
262+
has-coeq (F₀ (Comparison F⊣G) x) .unique
263+
{p = ap₂ D._∘_ (F⊣G .counit.is-natural _ _ _) refl
264+
·· D.pullr (F⊣G .counit.is-natural _ _ _)
265+
·· D.pulll (sym (F⊣G .counit.is-natural _ _ _))}
266+
(sym (D.pullr (has-coeq _ .universal) ∙ D.pulll (has-coeq _ .universal)))
267+
∙ sym (has-coeq _ .unique (F⊣G .counit.is-natural _ _ _ ∙ D.pushr (sym (has-coeq _ .universal))))
268+
Comparison⁻¹⊣Comparison .zig =
269+
has-coeq _ .unique {e′ = has-coeq _ .coeq} {p = has-coeq _ .coequal}
270+
(sym (D.pullr (has-coeq _ .universal)
271+
∙ D.pulll (has-coeq _ .universal)
272+
∙ ap₂ D._∘_ refl (F.F-∘ _ _) ∙ D.pulll (F⊣G .counit.is-natural _ _ _)
273+
∙ D.cancelr (F⊣G .zig)))
274+
∙ sym (has-coeq _ .unique (D.introl refl))
275+
Comparison⁻¹⊣Comparison .zag = Algebra-hom-path C $
276+
G.pulll (has-coeq _ .universal) ∙ F⊣G .zag
277+
```
278+
279+
</details>

0 commit comments

Comments
 (0)