Monadic adjunctions🔗

An adjunction $F ⊣ G$ between functors $F : C \to D$ and $G : 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

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

Comparison : Functor D (Eilenberg-Moore C L∘R)
Comparison .F₀ x = R.₀ x , alg where
  alg : Algebra-on C L∘R (R.₀ x)
  alg .Algebra-on.ν = R.₁ (adj.counit.ε _)
  alg .Algebra-on.ν-unit = adj.zag
  alg .Algebra-on.ν-mult =
    R.₁ (adj.counit.ε _) C.∘ M₁ (R.₁ (adj.counit.ε _))        ≡⟨ sym (R.F-∘ _ _) ⟩
    R.₁ (adj.counit.ε _ D.∘ L.₁ (R.₁ (adj.counit.ε _)))       ≡⟨ ap R.₁ (adj.counit.is-natural _ _ _) ⟩
    R.₁ (adj.counit.ε x D.∘ adj.counit.ε (L.₀ (R.₀ x)))       ≡⟨ R.F-∘ _ _ ⟩
    R.₁ (adj.counit.ε x) C.∘ R.₁ (adj.counit.ε (L.₀ (R.₀ x))) ∎

Construction of the functorial action of Comparison

Comparison .F₁ x = hom where
  open Algebra-hom
  hom : Algebra-hom C _ _ _
  hom .morphism = R.₁ x
  hom .commutes =
    R.₁ x C.∘ R.₁ (adj.counit.ε _)        ≡⟨ sym (R.F-∘ _ _) ⟩
    R.₁ (x D.∘ adj.counit.ε _)            ≡⟨ ap R.₁ (sym (adj.counit.is-natural _ _ _)) ⟩
    R.₁ (adj.counit.ε _ D.∘ L.₁ (R.₁ x))  ≡⟨ R.F-∘ _ _ ⟩
    R.₁ (adj.counit.ε _) C.∘ M₁ (R.₁ x)   ∎
Comparison .F-id    = ext R.F-id
Comparison .F-∘ f g = ext (R.F-∘ _ _)

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

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