open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Conservative
open import Cat.Diagram.Coequaliser
open import Cat.Functor.Equivalence
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 C T

module C^T = C-r C^T

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


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


  -- 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)