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.Displayed.Total
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

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)
  module T = Monad (Adjunction→Monad F⊣U)

  T : Monad C
  T = Adjunction→Monad F⊣U
  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

Crude monadicity🔗

We present a refinement of the conditions laid out in Beck’s coequaliser for when an adjunction $F⊣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:\mathcal{C}\to \mathcal{D}$ (call its right adjoint $U\text{),}$ and we’re interested in characterising exactly when the comparison functor $K:\mathcal{D}\to {\mathcal{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 $F\text{,}$ $U$ be as in the paragraph above, and abbreviate the resulting monad by $T\text{;}$ Denote the comparison functor by $K\text{.}$

1. If $\mathcal{D}$ has Beck’s coequalisers for any $T\text{-algebra,}$ then $K$ has a left adjoint $K^{-1}⊣K\text{;}$

2. If, in addition, $U$ 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, $U$ is conservative, then the counit of the adjunction $\eta$ is also a natural isomorphism, and $K$ is an equivalence of precategories.

Proof We already established (1) here.

Let us show (2). Suppose that $\mathcal{D}$ has Beck’s coequalisers and that $U$ 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

    module adj = _⊣_ K⁻¹⊣K

  -- 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 $F\eta \text{.}$ It’s straightforward to calculate that this map is a right inverse; let me point out that it follows from the triangle identities for $F⊣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 $U$ preserves coequalisers, that both rows of the diagram

are coequalisers, hence there is a unique isomorphism ${\eta }_o^{-1}$ making the diagram commute. This is precisely the inverse to ${\eta }_o$ 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 ${\eta }^{-1}$ is a homomorphism of algebras. This is a calculation reusing the established proof that ${\eta }^{-1}\eta =\mathrm{id}$ 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 $U$ is conservative. Recall that the counit $\epsilon$ for the $K^{-1}⊣K$ adjunction is defined as the unique dotted map which fits into

But observe that the diagram

is also a coequaliser; Hence, since $U$ preserves the coequaliser $FUA\twoheadrightarrow K^{-1}KA\text{,}$ the map $U\epsilon :U{K}^{-1}KA\cong UA\text{;}$ But by assumption $U$ is conservative, so $\epsilon$ 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 $\mathcal{D}$ has Beck’s coequalisers, and $U$ is a conservative functor which preserves reflexive coequalisers, then the adjunction $F⊣U$ 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)
  → is-monadic F⊣U
crude-monadicity coeq pres cons = eqv' where
  open is-equivalence
  eqv : is-equivalence (Comparison-EM⁻¹ F⊣U coeq)
  eqv .F⁻¹          = Comparison-EM F⊣U
  eqv .F⊣F⁻¹        = Comparison-EM⁻¹⊣Comparison-EM 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