open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Adjoint.Monad
open import Cat.Functor.Conservative
open import Cat.Functor.Monadic.Beck
open import Cat.Diagram.Coequaliser
open import Cat.Functor.Equivalence
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.Crude
  {o  o′ ℓ′} {C : Precategory o } {D : Precategory o′ ℓ′}
  {F : Functor C D} {U : Functor D C}
  (F⊣U : F  U)
  where

Crude monadicity🔗

We present a refinement of the conditions laid out in Beck’s coequaliser for when an adjunction FGF \dashv G 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 F:CDF : \ca{C} \to \ca{D} (call its right adjoint UU), and we’re interested in characterising exactly when the comparison functor K:DCUFK : \ca{D} \to \ca{C}^{UF} 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 FF, UU be as in the paragraph above, and abbreviate the resulting monad by TT; Denote the comparison functor by KK.

  1. If D\ca{D} has Beck’s coequalisers for any TT-algebra, then KK has a left adjoint K1KK^{-1} \dashv K;

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

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

Proof We already established (1) here.

Let us show (2). Suppose that D\ca{D} has Beck’s coequalisers and that UU 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 C T)  Coequaliser D (F.₁ (M .snd .ν)) (counit.ε _))
  (U-pres : U-preserves-reflexive-coeqs)
  where
  -- 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
    (Algebra-hom-path C η⁻¹η) (Algebra-hom-path C ηη⁻¹) where

The first thing we note is that Beck’s coequaliser is reflexive: The common right inverse is FηF\eta. It’s straightforward to calculate that this map is a right inverse; let me point out that it follows from the triangle identities for FUF \dashv U 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 UU preserves coequalisers, that both rows of the diagram

are coequalisers, hence there is a unique isomorphism ηo1\eta_o^{-1} making the diagram commute. This is precisely the inverse to ηo\eta_o we’re seeking.

    η⁻¹ : C.Hom (U.₀ (coapex (has-coeq o))) (o .fst)
    η⁻¹η : adj.unit.η _ .morphism C.∘ η⁻¹  C.id
    ηη⁻¹ : η⁻¹ C.∘ adj.unit.η _ .morphism  C.id

    η⁻¹ = preserved .coequalise {e′ = o .snd .ν} (o .snd .ν-mult)

    η⁻¹η = is-coequaliser.unique₂ preserved
      {e′ = U.₁ (has-coeq o .coeq)} {p = preserved .coequal}
      (sym (C.pullr (preserved .universal)
           C.pullr (unit.is-natural _ _ _)
           C.pulll (preserved .coequal)
           C.cancelr zag))
      (C.introl refl)

    ηη⁻¹ = C.pulll (preserved .universal)  o .snd .ν-unit

It remains to show that η1\eta^{-1} is a homomorphism of algebras. This is a calculation reusing the established proof that η1η=id\eta^{-1}\eta = \id{id} established using the universal property of coequalisers above.

    inverse : C^T.Hom (U.₀ _ , _) o
    inverse .morphism = η⁻¹
    inverse .commutes =
      η⁻¹ 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 .universal) 
      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 UU is conservative. Recall that the counit ε\epsilon for the K1KK^{-1} \dashv K adjunction is defined as the unique dotted map which fits into

But observe that the diagram

is also a coequaliser; Hence, since UU preserves the coequaliser FUAK1KAFUA \epi K^{-1}KA, the map Uε:UK1KAUAU\eps : UK^{-1}KA \cong UA; But by assumption UU is conservative, so ε\eps 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 .universal)  zag)
      inversel
    where

    oalg = Comparison 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)} {p = preserved .coequal}
        (sym (C.pullr (U.collapse (coequ .universal))
             C.pullr (unit.is-natural _ _ _)
             C.pulll (preserved .coequal)
             C.cancelr zag))
        (C.introl refl)

Packaging it all up, we get the claimed theorem: If D\ca{D} has Beck’s coequalisers, and UU is a conservative functor which preserves reflexive coequalisers, then the adjunction FUF \dashv U is monadic.

crude-monadicity
  : (has-coeq : (M : Algebra C T)  Coequaliser D (F.₁ (M .snd .ν)) (counit.ε _))
    (U-pres : U-preserves-reflexive-coeqs)
    (U-conservative : is-conservative U)
   is-monadic F⊣U
crude-monadicity coeq pres cons = eqv′ where
  open is-equivalence
  eqv : is-equivalence (Comparison⁻¹ F⊣U coeq)
  eqv .F⁻¹          = Comparison F⊣U
  eqv .F⊣F⁻¹        = Comparison⁻¹⊣Comparison F⊣U coeq
  eqv .unit-iso _   = prcoeq→unit-is-iso coeq pres
  eqv .counit-iso _ = conservative-prcoeq→counit-is-iso coeq pres cons
  eqv′ = inverse-equivalence eqv

References

  • Mac Lane, Saunders, and Ieke Moerdijk. 1994. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext. New York, NY: Springer New York. https://doi.org/10.1007/978-1-4612-0927-0.