open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Conservative
open import Cat.Diagram.Coequaliser
open import Cat.Functor.Equivalence
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} {U : Functor D C}
(Fβ£U : F β£ U)
where

private
module F = F-r F
module U = F-r U
module C = C-r C
module D = C-r D
module UF = F-r (U Fβ F)

C^T : Precategory _ _
C^T = Eilenberg-Moore T

module C^T = C-r C^T

open _β£_ Fβ£U
open _=>_
open Algebra-on
open Total-hom


We present a refinement of the conditions laid out in Beckβs coequaliser for when an adjunction is monadic: The crude monadicity theorem. The proof we present is adapted from [Mac Lane and Moerdijk (1994), chap. IV; sect. 4], where it is applied to the setting of elementary topoi, but carried out in full generality.

Recall our setup. We have a left adjoint functor (call its right adjoint and weβre interested in characterising exactly when the comparison functor into the Eilenberg-Moore category of the monad from the adjunction is an equivalence. Our refinement here gives a sufficient condition.

Theorem (Crude monadicity). Let the functors be as in the paragraph above, and abbreviate the resulting monad by Denote the comparison functor by

1. If has Beckβs coequalisers for any then has a left adjoint

2. If, in addition, preserves coequalisers for any pair which has a common right inverse, then the unit of the adjunction is a natural isomorphism;

3. If, in addition, is conservative, then the counit of the adjunction is also a natural isomorphism, and is an equivalence of precategories.

Proof We already established (1) here.

Let us show (2). Suppose that has Beckβs coequalisers and that preserves coequalisers of pairs of morphisms with a common right inverse (we call these coequalisers reflexive):

private
U-preserves-reflexive-coeqs : Type _
U-preserves-reflexive-coeqs =
β {A B} {f g : D.Hom A B} (i : D.Hom B A)
β (f D.β i β‘ D.id) β (g D.β i β‘ D.id)
β (coequ : Coequaliser D f g)
β is-coequaliser C (U.β f) (U.β g) (U.β (coequ .Coequaliser.coeq))

module _
(has-coeq : (M : Algebra T) β Coequaliser D (F.β (M .snd .Ξ½)) (counit.Ξ΅ _))
(U-pres : U-preserves-reflexive-coeqs)
where

  open is-coequaliser
open Coequaliser
open Functor

private
Kβ»ΒΉ : Functor C^T D
Kβ»ΒΉ = Comparison-EMβ»ΒΉ Fβ£U has-coeq

Kβ»ΒΉβ£K : Kβ»ΒΉ β£ Comparison-EM Fβ£U
Kβ»ΒΉβ£K = Comparison-EMβ»ΒΉβ£Comparison-EM Fβ£U has-coeq


  -- N.B.: In the code we abbreviate "preserves reflexive coequalisers"
-- by "prcoeq".
prcoeqβunit-is-iso : β {o} β C^T.is-invertible (adj.unit.Ξ· o)
prcoeqβunit-is-iso {o} = C^T.make-invertible inverse
(ext Ξ·β»ΒΉΞ·) (ext Ξ·Ξ·β»ΒΉ) where


The first thing we note is that Beckβs coequaliser is reflexive: The common right inverse is Itβs straightforward to calculate that this map is a right inverse; let me point out that it follows from the triangle identities for and the algebra laws.

    abstract
preserved : is-coequaliser C
(UF.β (o .snd .Ξ½)) (U.β (counit.Ξ΅ (F.β (o .fst))))
(U.β (has-coeq o .coeq))
preserved =
U-pres (F.β (unit.Ξ· _)) (F.annihilate (o .snd .Ξ½-unit)) zig
(has-coeq o)


It follows, since preserves coequalisers, that both rows of the diagram

are coequalisers, hence there is a unique isomorphism making the diagram commute. This is precisely the inverse to weβre seeking.

    Ξ·β»ΒΉ : C.Hom (U.β (coapex (has-coeq o))) (o .fst)
Ξ·β»ΒΉΞ· : adj.unit.Ξ· _ .hom C.β Ξ·β»ΒΉ β‘ C.id
Ξ·Ξ·β»ΒΉ : Ξ·β»ΒΉ C.β adj.unit.Ξ· _ .hom β‘ C.id

Ξ·β»ΒΉ = preserved .universal {e' = o .snd .Ξ½} (o .snd .Ξ½-mult)

Ξ·β»ΒΉΞ· = is-coequaliser.uniqueβ preserved
{e' = U.β (has-coeq o .coeq)}
(preserved .coequal)
(C.pullr (preserved .factors)
β C.pullr (unit.is-natural _ _ _)
β C.pulll (preserved .coequal)
β C.cancelr zag)
(C.idl _)

Ξ·Ξ·β»ΒΉ = C.pulll (preserved .factors) β o .snd .Ξ½-unit


It remains to show that is a homomorphism of algebras. This is a calculation reusing the established proof that established using the universal property of coequalisers above.

    inverse : C^T.Hom (U.β _ , _) o
inverse .hom = Ξ·β»ΒΉ
inverse .preserves =
Ξ·β»ΒΉ C.β U.β (counit.Ξ΅ _)                                                              β‘β¨ C.reflβ©ββ¨ ap U.β (D.intror (F.annihilate (C.assoc _ _ _ β Ξ·β»ΒΉΞ·))) β©β‘
Ξ·β»ΒΉ C.β U.β (counit.Ξ΅ _ D.β F.β (U.β (has-coeq o .coeq)) D.β F.β (unit.Ξ· _ C.β Ξ·β»ΒΉ))  β‘β¨ C.reflβ©ββ¨ ap U.β (D.extendl (counit.is-natural _ _ _)) β©β‘
Ξ·β»ΒΉ C.β U.β (has-coeq o .coeq D.β counit.Ξ΅ _ D.β F.β (unit.Ξ· _ C.β Ξ·β»ΒΉ))              β‘β¨ C.reflβ©ββ¨ U.F-β _ _ β©β‘
Ξ·β»ΒΉ C.β U.β (has-coeq o .coeq) C.β U.β (counit.Ξ΅ _ D.β F.β (unit.Ξ· _ C.β Ξ·β»ΒΉ))        β‘β¨ C.pulll (preserved .factors) β©β‘
o .snd .Ξ½ C.β U.β (counit.Ξ΅ _ D.β F.β (unit.Ξ· _ C.β Ξ·β»ΒΉ))                             β‘β¨ C.reflβ©ββ¨ ap U.β (ap (counit.Ξ΅ _ D.β_) (F.F-β _ _) β D.cancell zig) β©β‘
o .snd .Ξ½ C.β UF.β Ξ·β»ΒΉ                                                                β


For (3), suppose additionally that is conservative. Recall that the counit for the adjunction is defined as the unique dotted map which fits into

But observe that the diagram

is also a coequaliser; Hence, since preserves the coequaliser the map But by assumption is conservative, so is an isomorphism, as desired.

  conservative-prcoeqβcounit-is-iso
: β {o} β is-conservative U β D.is-invertible (adj.counit.Ξ΅ o)
conservative-prcoeqβcounit-is-iso {o} reflect-iso = reflect-iso \$
C.make-invertible
(U.β (coequ .coeq) C.β unit.Ξ· _) (U.pulll (coequ .factors) β zag)
inversel
where

oalg = Comparison-EM Fβ£U .Fβ o
coequ = has-coeq oalg

abstract
preserved : is-coequaliser C
(UF.β (oalg .snd .Ξ½)) (U.β (counit.Ξ΅ (F.β (oalg .fst))))
(U.β (coequ .coeq))
preserved =
U-pres (F.β (unit.Ξ· _)) (F.annihilate (oalg .snd .Ξ½-unit)) zig coequ

inversel =
is-coequaliser.uniqueβ preserved
{e' = U.β (coequ .coeq)}
(preserved .coequal)
(C.pullr (U.collapse (coequ .factors))
β C.pullr (unit.is-natural _ _ _)
β C.pulll (preserved .coequal)
β C.cancelr zag)
(C.idl _)


Packaging it all up, we get the claimed theorem: If has Beckβs coequalisers, and is a conservative functor which preserves reflexive coequalisers, then the adjunction is monadic.

crude-monadicity
: (has-coeq : (M : Algebra T) β Coequaliser D (F.β (M .snd .Ξ½)) (counit.Ξ΅ _))
(U-pres : U-preserves-reflexive-coeqs)
(U-conservative : is-conservative U)