open import Cat.Functor.Adjoint.Monadic
open import Cat.Diagram.Coequaliser
open import Cat.Displayed.Total
open import Cat.Prelude

import Cat.Functor.Reasoning as F-r
import Cat.Reasoning as C-r

module
{o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
{F : Functor C D} {G : Functor D C}
(F⊣G : F ⊣ G)
where

private
module F = F-r F
module G = F-r G
module C = C-r C
module D = C-r D
module GF = F-r (G F∘ F)
private
C^T : Precategory _ _
C^T = Eilenberg-Moore T
open _⊣_ F⊣G
open _=>_
open Algebra-on
open Total-hom


# Beck’s coequaliser🔗

Let be a functor admitting a right adjoint Recall that every adjunction induces a monad (which we will call for short) on the category and a “comparison” functor into the Eilenberg-Moore category of In this module we will lay out a sufficient condition for the functor to have a left adjoint, which we call (Comparison-EM⁻¹). Let us first establish a result about the presentation of algebras by “generators and relations”.

Suppose that we are given a Note that is also a namely the free on the object Let us illustrate this with a concrete example: Suppose we have the cyclic group for some natural number which we regard as a quotient group of The corresponding algebra would be the free group on generators whence1 we conclude that, in general, this “free-on-underlying” algebra is very far from being the algebra we started with.

Still, motivated by our example, it feels like we should be able to quotient the algebra by some set of relations and get back the algebra we started with. This is absolutely true, and it’s true even when the category of is lacking in quotients! In particular, we have the following theorem:

Theorem. Every is the coequaliser of the diagram

called the Beck coequaliser (of Furthermore, this coequaliser is reflexive in meaning that the arrows and have a common right inverse. Elaborating a bit, this theorem lets us decompose any into a canonical presentation of by generators and relations, as a quotient of a free algebra by a relation (induced by) the fold

module _ (Aalg : Algebra T) where
private
A = Aalg .fst
module A = Algebra-on (Aalg .snd)

TA : Algebra T
TA = Free-EM .Functor.F₀ A

TTA : Algebra T
TTA = Free-EM .Functor.F₀ (T.M₀ A)

mult : Algebra-hom T TTA TA
mult .hom = T.mult .η _
mult .preserves = sym T.mult-assoc

fold : Algebra-hom T TTA TA
fold .hom = T.M₁ A.ν
fold .preserves =
T.M₁ A.ν C.∘ T.mult .η _        ≡˘⟨ T.mult .is-natural _ _ _ ⟩≡˘
T.mult .η _ C.∘ T.M₁ (T.M₁ A.ν) ∎


Proof. The proof is by calculation, applying the monad laws where applicable, so we present it without much further commentary. Observe that coequalises and essentially by the definition of being an algebra map. Note that we do not make use of the fact that the monad was given by a specified adjunction in the proof, and any adjunction presenting will do.

  open is-coequaliser
algebra-is-coequaliser
: is-coequaliser C^T {A = TTA} {B = TA} {E = Aalg}
mult fold (record { hom = A.ν ; preserves = sym A.ν-mult })
algebra-is-coequaliser .coequal = ext $A.ν C.∘ T.mult .η _ ≡˘⟨ A.ν-mult ⟩≡˘ A.ν C.∘ T.M₁ A.ν ∎  The colimiting map from to some other algebra which admits a map is given by the composite which is a map of algebras by a long computation, and satisfies the properties of a coequalising map by slightly shorter computations, which can be seen below. Uniqueness of this map follows almost immediately from the algebra laws.  algebra-is-coequaliser .universal {F = F} {e'} p .hom = e' .hom C.∘ T.unit .η A algebra-is-coequaliser .universal {F = F} {e'} p .preserves = (e' .hom C.∘ unit.η A) C.∘ A.ν ≡⟨ C.extendr (unit.is-natural _ _ _) ⟩≡ (e' .hom C.∘ T.M₁ A.ν) C.∘ unit.η (T.M₀ A) ≡˘⟨ ap hom p C.⟩∘⟨refl ⟩≡˘ (e' .hom C.∘ T.mult .η A) C.∘ unit.η (T.M₀ A) ≡⟨ C.cancelr T.right-ident ⟩≡ e' .hom ≡⟨ C.intror (sym (T.M-∘ _ _) ∙ ap T.M₁ A.ν-unit ∙ T.M-id) ⟩≡ e' .hom C.∘ T.M₁ A.ν C.∘ T.M₁ (unit.η A) ≡⟨ C.pulll (sym (ap hom p)) ⟩≡ (e' .hom C.∘ T.mult .η A) C.∘ T.M₁ (unit.η A) ≡⟨ C.pushl (e' .preserves) ⟩≡ F .snd .ν C.∘ T.M₁ (e' .hom) C.∘ T.M₁ (unit.η A) ≡˘⟨ C.refl⟩∘⟨ T.M-∘ _ _ ⟩≡˘ F .snd .ν C.∘ T.M₁ (e' .hom C.∘ unit.η A) ∎ algebra-is-coequaliser .factors {F = F} {e'} {p} = ext$
(e' .hom C.∘ unit.η _) C.∘ A.ν          ≡⟨ C.extendr (unit.is-natural _ _ _) ⟩≡
(e' .hom C.∘ T.M₁ A.ν) C.∘ unit.η  _    ≡˘⟨ ap hom p C.⟩∘⟨refl ⟩≡˘
(e' .hom C.∘ T.mult .η _) C.∘ unit.η  _ ≡⟨ C.cancelr T.right-ident ⟩≡
e' .hom                                 ∎
algebra-is-coequaliser .unique {F = F} {e'} {p} {colim} q = ext $sym$
e' .hom C.∘ unit.η A              ≡⟨ ap hom (sym q) C.⟩∘⟨refl ⟩≡
(colim .hom C.∘ A.ν) C.∘ unit.η A ≡⟨ C.cancelr A.ν-unit ⟩≡
colim .hom                        ∎


# Presented algebras🔗

The lemma above says that every algebra which exists can be presented by generators and relations; The relations are encoded by the pair of maps in Beck’s coequaliser, above. But what about the converse? The following lemma says that, if every algebra presented by generators-and-relations (encoded by a parallel pair has a coequaliser in , then the comparison functor has a left adjoint.

module _
(has-coeq : (M : Algebra T) → Coequaliser D (F.₁ (M .snd .ν)) (ε _))
where

open Coequaliser
open Functor


On objects, this left adjoint acts by sending each algebra to the coequaliser of (the diagram underlying) its Beck coequaliser. In a sense, this is “the best approximation in of the algebra”. The action on morphisms is uniquely determined since it’s a map out of a coequaliser.

If we consider the comparison functor as being “the underlying an object of ”, then the functor we construct below is the “free object of on a ”. Why is this adjunction relevant, though? Its failure to be an equivalence measures just how far our original adjunction is from being monadic, that is, how far is from being the category of

  Comparison-EM⁻¹ : Functor (Eilenberg-Moore T) D
Comparison-EM⁻¹ .F₀ = coapex ⊙ has-coeq
Comparison-EM⁻¹ .F₁ {X} {Y} alg-map =
has-coeq X .universal {e' = e'} path where
e' : D.Hom (F.F₀ (X .fst)) (Comparison-EM⁻¹ .F₀ Y)
e' = has-coeq Y .coeq D.∘ F.₁ (alg-map .hom)

      abstract
path : e' D.∘ F.₁ (X .snd .ν) ≡ e' D.∘ ε (F.₀ (X .fst))
path =
(has-coeq Y .coeq D.∘ F.₁ (alg-map .hom)) D.∘ F.₁ (X .snd .ν)      ≡⟨ D.pullr (F.weave (alg-map .preserves)) ⟩≡
has-coeq Y .coeq D.∘ F.₁ (Y .snd .ν) D.∘ F.₁ (T.M₁ (alg-map .hom)) ≡⟨ D.extendl (has-coeq Y .coequal) ⟩≡
has-coeq Y .coeq D.∘ ε _ D.∘ F.₁ (T.M₁ (alg-map .hom))             ≡⟨ D.pushr (counit.is-natural _ _ _) ⟩≡
(has-coeq Y .coeq D.∘ F.₁ (alg-map .hom)) D.∘ ε _                  ∎
Comparison-EM⁻¹ .F-id {X} = sym $has-coeq X .unique (D.idl _ ∙ D.intror F.F-id) Comparison-EM⁻¹ .F-∘ {X} f g = sym$ has-coeq X .unique $D.pullr (has-coeq X .factors) ·· D.pulll (has-coeq _ .factors) ·· F.pullr refl open _⊣_  The adjunction unit and counit are again very simple, and it’s evident to a human looking at them that they satisfy the triangle identities (and are algebra homomorphisms). Agda is not as easy to convince, though, so we leave the computation folded up for the bravest of readers.  Comparison-EM⁻¹⊣Comparison-EM : Comparison-EM⁻¹ ⊣ Comparison-EM F⊣G Comparison-EM⁻¹⊣Comparison-EM .unit .η x .hom = G.₁ (has-coeq _ .coeq) C.∘ T.unit .η _ Comparison-EM⁻¹⊣Comparison-EM .counit .η x = has-coeq _ .universal (F⊣G .counit.is-natural _ _ _)  Nah, really, it’s quite ugly.  Comparison-EM⁻¹⊣Comparison-EM .unit .η x .preserves = C.pullr (T.unit .is-natural _ _ _) ∙ G.extendl (has-coeq _ .coequal) ∙ C.elimr (F⊣G .zag) ∙ G.intror (F⊣G .zig) ∙ G.weave (D.pulll (sym (F⊣G .counit.is-natural _ _ _)) ∙ D.pullr (sym (F.F-∘ _ _))) Comparison-EM⁻¹⊣Comparison-EM .unit .is-natural x y f = ext$
(G.₁ (has-coeq y .coeq) C.∘ T.unit.η _) C.∘ f .hom                    ≡⟨ C.pullr (T.unit.is-natural _ _ _) ⟩≡
G.₁ (has-coeq y .coeq) C.∘ T.M₁ (f .hom) C.∘ T.unit .η (x .fst)       ≡⟨ C.pulll (sym (G.F-∘ _ _)) ⟩≡
G.₁ (has-coeq y .coeq D.∘ F.₁ (f .hom)) C.∘ T.unit .η (x .fst)        ≡⟨ ap G.₁ (sym (has-coeq _ .factors)) C.⟩∘⟨refl ⟩≡
G.₁ (has-coeq x .universal _ D.∘ has-coeq x .coeq) C.∘ T.unit .η (x .fst) ≡⟨ C.pushl (G.F-∘ _ _) ⟩≡
G.₁ (has-coeq x .universal _) C.∘ G.₁ (has-coeq x .coeq) C.∘ T.unit.η _   ∎
Comparison-EM⁻¹⊣Comparison-EM .counit .is-natural x y f =
has-coeq (F₀ (Comparison-EM F⊣G) x) .unique
{p = ap₂ D._∘_ (F⊣G .counit.is-natural _ _ _) refl
·· D.pullr (F⊣G .counit.is-natural _ _ _)
·· D.pulll (sym (F⊣G .counit.is-natural _ _ _))}
(D.pullr (has-coeq _ .factors) ∙ D.pulll (has-coeq _ .factors))
∙ sym (has-coeq _ .unique (D.pullr (has-coeq _ .factors) ∙ sym (F⊣G .counit.is-natural _ _ _)))
Comparison-EM⁻¹⊣Comparison-EM .zig =
unique₂ (has-coeq _)
(has-coeq _ .coequal)
(D.pullr (has-coeq _ .factors)
∙ D.pulll (has-coeq _ .factors)
∙ ap₂ D._∘_ refl (F.F-∘ _ _)
∙ D.pulll (F⊣G .counit.is-natural _ _ _)
∙ D.cancelr (F⊣G .zig))
(D.idl _)
Comparison-EM⁻¹⊣Comparison-EM .zag = ext \$
G.pulll (has-coeq _ .factors) ∙ F⊣G .zag


1. I was feeling pretentious when I wrote this sentence↩︎