open import Cat.Functor.Equivalence.Properties
open import Cat.Instances.Algebras.Limits
open import Cat.Functor.Adjoint.Monad
open import Cat.Functor.Equivalence
open import Cat.Diagram.Limit.Base
open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
open import Cat.Diagram.Monad
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

open Functor
open ∫Hom
open _=>_

Monadic adjunctions🔗

An adjunction $L⊣R$ between functors $L:C\to D$ and $R:D\to C$ is monadic if the induced comparison functor $D\to C^{R\circ L}$ (where the right-hand side is the Eilenberg-Moore category of the monad of the adjunction) is an equivalence of categories.

module
  Cat.Functor.Adjoint.Monadic
  {o₁ h₁ o₂ h₂ : _}
  {C : Precategory o₁ h₁}
  {D : Precategory o₂ h₂}
  {L : Functor C D} {R : Functor D C}
  (L⊣R : L ⊣ R)
  where

private
  module C = Cat.Reasoning C
  module D = Cat.Reasoning D
  module L = Cat.Functor.Reasoning L
  module R = Cat.Functor.Reasoning R
  module adj = _⊣_ L⊣R

R∘L : Monad-on _
R∘L = Adjunction→Monad L⊣R

open Monad-on R∘L

_ = Algebra

The composition of R.₁ with the adjunction counit natural transformation gives R an Algebra structure, thus extending R to a functor $D\to C^{R\circ L}\text{.}$

Comparison-EM : Functor D (Eilenberg-Moore R∘L)
Comparison-EM .F₀ x = R.₀ x , alg where
  alg : Algebra-on R∘L (R.₀ x)
  alg .Algebra-on.ν = R.₁ (adj.counit.ε _)
  alg .Algebra-on.ν-unit = adj.zag
  alg .Algebra-on.ν-mult = R.weave (sym $ adj.counit.is-natural _ _ _)

Comparison-EM .F₁ x .fst = R.₁ x
Comparison-EM .F₁ x .snd = R.weave (sym (adj.counit.is-natural _ _ _))
Comparison-EM .F-id    = ext R.F-id
Comparison-EM .F-∘ f g = ext (R.F-∘ _ _)

By construction, the composition of the comparison functor with the forgetful functor is equal to $R\text{.}$

Forget∘Comparison≡R : Forget-EM F∘ Comparison-EM ≡ R
Forget∘Comparison≡R = Functor-path (λ _ → refl) (λ _ → refl)

To summarise, we have the following triangle:

An adjunction is monadic if Comparison-EM is an equivalence of categories, thus exhibiting $C$ as the category of $(R\circ L)\text{-algebras:}$

is-monadic : Type _
is-monadic = is-equivalence Comparison-EM

We also say that the right adjoint $R$ is a monadic functor.

Monadic functors create limits🔗

By the description of limits in categories of algebras, Forget-EM creates limits. Furthermore, if the adjunction $L⊣R$ is monadic, then Comparison-EM is an equivalence of categories, so it also creates limits. Since this property is closed under composition, monadic functors creates limits.

module _ (monadic : is-monadic) where

  monadic→creates-limits
    : ∀ {oj ℓj} {J : Precategory oj ℓj} → creates-limits-of J R
  monadic→creates-limits = subst (creates-limits-of _) Forget∘Comparison≡R $
    F∘-creates-limits (equivalence→creates-limits monadic)
      (Forget-EM-creates-limits R∘L)