open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Adjoint.Monad
open import Cat.Diagram.Coequaliser
open import Cat.Functor.Adjoint
open import Cat.Diagram.Monad
open import Cat.Prelude

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

module
  Cat.Functor.Monadic.Beck
  {o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
  {F : Functor C D} {G : Functor D C}
  (F⊣G : F ⊣ G)
  where

Beck’s coequaliserπŸ”—

Let F:Cβ†’DF : \ca{C} \to \ca{D} be a functor admitting a right adjoint U:Dβ†’CU : \ca{D} \to \ca{C}. Recall that every adjunction induces a monad UFUF (which we will call TT for short) on the category C\ca{C}, and a β€œcomparison” functor K:Dβ†’CTK : \ca{D} \to \ca{C}^{T} into the Eilenberg-Moore category of TT. In this module we will lay out a sufficient condition for the functor KK to have a left adjoint, which we call Kβˆ’1K^{-1} (Comparison⁻¹). Let us first establish a result about the presentation of TT-algebras by β€œgenerators and relations”.

Suppose that we are given a TT-algebra (A,Ξ½)(A, \nu). Note that (TA,ΞΌ)(TA, \mu) is also a TT-algebra, namely the free TT-algebra on the object AA. Let us illustrate this with a concrete example: Suppose we have the cyclic group Z/nZ\bb{Z}/n\bb{Z}, for some natural number nn, which we regard as a subgroup of Z\bb{Z}. The corresponding algebra (TA,ΞΌ)(TA, \mu) would be the free group on one generator1 whence2 we conclude that, in general, this β€œfree-on-underlying” (TA,ΞΌ)(TA, \mu) algebra is very far from being the (A,Ξ½)(A, \nu) algebra we started with.

Still, motivated by our Z/nZ\bb{Z}/n\bb{Z} example, it feels like we should be able to quotient the algebra (TA,ΞΌ)(TA, \mu) by some set of relations and get back the algebra (A,Ξ½)(A, \nu) we started with. This is absolutely true, and it’s true even when the category of TT-algebras is lacking in quotients! In particular, we have the following theorem:

Theorem. Every TT-algebra (A,Ξ½)(A, \nu) is the coequaliser of the diagram

called the Beck coequaliser (of AA). Furthermore, this coequaliser is reflexive in CT\ca{C}^T, meaning that the arrows ΞΌ\mu and TΞ½T\nu have a common right inverse. Elaborating a bit, this theorem lets us decompose any TT-algebra (A,Ξ½)(A, \nu) into a canonical presentation of AA by generators and relations, as a quotient of a free algebra by a relation (induced by) the fold Ξ½\nu.

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

  open is-coequaliser
  algebra-is-coequaliser
    : is-coequaliser C^T {A = TTA} {B = TA} {E = Aalg}
      mult fold (record { morphism = A.Ξ½ ; commutes = sym A.Ξ½-mult })
  algebra-is-coequaliser .coequal = Algebra-hom-path C $
    A.Ξ½ C.∘ T.mult .Ξ· _ β‰‘Λ˜βŸ¨ A.Ξ½-mult βŸ©β‰‘Λ˜
    A.Ξ½ C.∘ T.M₁ A.Ξ½    ∎

The colimiting map from (A,Ξ½)(A, \nu) to some other algebra (F,Ξ½β€²)(F, \nu') which admits a map eβ€²:(TA,ΞΌ)β†’(F,Ξ½β€²)e' : (TA, \mu) \to (F, \nu') is given by the composite

A→ηTA→e′F, A \xto{\eta} TA \xto{e'} F\text{,}

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 .coequalise {F = F} {e'} p .morphism =
    e' .morphism C.∘ T.unit .η A
  algebra-is-coequaliser .coequalise {F = F} {e'} p .commutes =
    (e' .morphism C.∘ unit.Ξ· A) C.∘ A.Ξ½                   β‰‘βŸ¨ C.extendr (unit.is-natural _ _ _) βŸ©β‰‘
    (e' .morphism C.∘ T.M₁ A.Ξ½) C.∘ unit.Ξ·  (T.Mβ‚€ A)      β‰‘Λ˜βŸ¨ ap morphism p C.⟩∘⟨refl βŸ©β‰‘Λ˜
    (e' .morphism C.∘ T.mult .Ξ· A) C.∘ unit.Ξ·  (T.Mβ‚€ A)   β‰‘βŸ¨ C.cancelr T.right-ident βŸ©β‰‘
    e' .morphism                                          β‰‘βŸ¨ C.intror (sym (T.M-∘ _ _) βˆ™ ap T.M₁ A.Ξ½-unit βˆ™ T.M-id) βŸ©β‰‘
    e' .morphism C.∘ T.M₁ A.Ξ½ C.∘ T.M₁ (unit.Ξ· A)         β‰‘βŸ¨ C.pulll (sym (ap morphism p)) βŸ©β‰‘
    (e' .morphism C.∘ T.mult .Ξ· A) C.∘ T.M₁ (unit.Ξ· A)    β‰‘βŸ¨ C.pushl (e' .commutes) βŸ©β‰‘
    F .snd .Ξ½ C.∘ T.M₁ (e' .morphism) C.∘ T.M₁ (unit.Ξ· A) β‰‘Λ˜βŸ¨ C.refl⟩∘⟨ T.M-∘ _ _ βŸ©β‰‘Λ˜
    F .snd .Ξ½ C.∘ T.M₁ (e' .morphism C.∘ unit.Ξ· A)        ∎
  algebra-is-coequaliser .universal {F = F} {e'} {p} = Algebra-hom-path C $
    (e' .morphism C.∘ unit.Ξ· _) C.∘ A.Ξ½          β‰‘βŸ¨ C.extendr (unit.is-natural _ _ _) βŸ©β‰‘
    (e' .morphism C.∘ T.M₁ A.Ξ½) C.∘ unit.Ξ·  _    β‰‘Λ˜βŸ¨ ap morphism p C.⟩∘⟨refl βŸ©β‰‘Λ˜
    (e' .morphism C.∘ T.mult .Ξ· _) C.∘ unit.Ξ·  _ β‰‘βŸ¨ C.cancelr T.right-ident βŸ©β‰‘
    e' .morphism                                 ∎
  algebra-is-coequaliser .unique {F = F} {e'} {p} {colim} q =
    Algebra-hom-path C $ sym $
      e' .morphism C.∘ unit.Ξ· A              β‰‘βŸ¨ ap morphism q C.⟩∘⟨refl βŸ©β‰‘
      (colim .morphism C.∘ A.Ξ½) C.∘ unit.Ξ· A β‰‘βŸ¨ C.cancelr A.Ξ½-unit βŸ©β‰‘
      colim .morphism                        ∎

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 T2A⇉TAT^2A \tto TA 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 T2A⇉TAT^2A \tto TA) has a coequaliser in D\ca{D}, then the comparison functor Dβ†’CT\ca{D} \to \ca{C}^T has a left adjoint.

On objects, this left adjoint acts by sending each algebra MM to the coequaliser of (the diagram underlying) its Beck coequaliser. In a sense, this is β€œthe best approximation in D\ca{D} 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 TT-algebra underlying an object of D\ca{D}”, then the functor we construct below is the β€œfree object of D\ca{D} on a TT-algebra”. 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 D\ca{D} is from being the category of TT-algebras.

  Comparison⁻¹ : Functor (Eilenberg-Moore C T) D
  Comparison⁻¹ .Fβ‚€ = coapex βŠ™ has-coeq
  Comparison⁻¹ .F₁ {X} {Y} alg-map =
    has-coeq X .coequalise {eβ€² = eβ€²} path where
      eβ€² : D.Hom (F.Fβ‚€ (X .fst)) (Comparison⁻¹ .Fβ‚€ Y)
      eβ€² = has-coeq Y .coeq D.∘ F.₁ (alg-map .morphism)

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⁻¹⊣Comparison : Comparison⁻¹ ⊣ Comparison F⊣G
  Comparison⁻¹⊣Comparison .unit .η x .morphism =
    G.₁ (has-coeq _ .coeq) C.∘ T.unit .Ξ· _
  Comparison⁻¹⊣Comparison .counit .η x =
    has-coeq _ .coequalise (F⊣G .counit.is-natural _ _ _)
Nah, really, it’s quite ugly.
  Comparison⁻¹⊣Comparison .unit .η x .commutes =
      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⁻¹⊣Comparison .unit .is-natural x y f = Algebra-hom-path C $
    (G.₁ (has-coeq y .coeq) C.∘ T.unit.Ξ· _) C.∘ f .morphism                    β‰‘βŸ¨ C.pullr (T.unit.is-natural _ _ _) βŸ©β‰‘
    G.₁ (has-coeq y .coeq) C.∘ T.M₁ (f .morphism) C.∘ T.unit .Ξ· (x .fst)       β‰‘βŸ¨ C.pulll (sym (G.F-∘ _ _)) βŸ©β‰‘
    G.₁ (has-coeq y .coeq D.∘ F.₁ (f .morphism)) C.∘ T.unit .Ξ· (x .fst)        β‰‘βŸ¨ ap G.₁ (sym (has-coeq _ .universal)) C.⟩∘⟨refl βŸ©β‰‘
    G.₁ (has-coeq x .coequalise _ D.∘ has-coeq x .coeq) C.∘ T.unit .Ξ· (x .fst) β‰‘βŸ¨ C.pushl (G.F-∘ _ _) βŸ©β‰‘
    G.₁ (has-coeq x .coequalise _) C.∘ G.₁ (has-coeq x .coeq) C.∘ T.unit.Ξ· _   ∎
  Comparison⁻¹⊣Comparison .counit .is-natural x y f =
      has-coeq (Fβ‚€ (Comparison 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 _ _ _))}
        (sym (D.pullr (has-coeq _ .universal) βˆ™ D.pulll (has-coeq _ .universal)))
    βˆ™ sym (has-coeq _ .unique (F⊣G .counit.is-natural _ _ _ βˆ™ D.pushr (sym (has-coeq _ .universal))))
  Comparison⁻¹⊣Comparison .zig =
    has-coeq _ .unique {eβ€² = has-coeq _ .coeq} {p = has-coeq _ .coequal}
      (sym (D.pullr (has-coeq _ .universal)
          βˆ™ D.pulll (has-coeq _ .universal)
          βˆ™ apβ‚‚ D._∘_ refl (F.F-∘ _ _) βˆ™ D.pulll (F⊣G .counit.is-natural _ _ _)
          βˆ™ D.cancelr (F⊣G .zig)))
    βˆ™ sym (has-coeq _ .unique (D.introl refl))
  Comparison⁻¹⊣Comparison .zag = Algebra-hom-path C $
    G.pulll (has-coeq _ .universal) βˆ™ F⊣G .zag

  1. the group of integersβ†©οΈŽ

  2. I was feeling pretentious when I wrote this sentenceβ†©οΈŽ