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

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 C T

  module C^T = C-r C^T

open _⊣_ F⊣U
open _=>_
open Algebra-hom
open Algebra-on

Crude monadicity🔗

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

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

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 C 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⁻¹ F⊣U has-coeq

    K⁻¹⊣K : K⁻¹ ⊣ Comparison F⊣U
    K⁻¹⊣K = Comparison⁻¹⊣Comparison 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$. 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 \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 $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.η _ .morphism C.∘ η⁻¹ ≡ C.id
    ηη⁻¹ : η⁻¹ C.∘ adj.unit.η _ .morphism ≡ 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 = \operatorname{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 .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 $\varepsilon$ for the $K^{-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 $U$ preserves the coequaliser $FUA \twoheadrightarrow K^{-1}KA$, the map $U\varepsilon : UK^{-1}KA \cong UA$; But by assumption $U$ is conservative, so $\varepsilon$ 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 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 \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