Monadic adjunctionsπŸ”—

An adjunction between functors and is monadic if the induced comparison functor (where the right-hand side is the Eilenberg-Moore category of the monad of the adjunction) is an equivalence of categories.

  {o₁ h₁ oβ‚‚ hβ‚‚ : _}
  {C : Precategory o₁ h₁}
  {D : Precategory oβ‚‚ hβ‚‚}
  {L : Functor C D} {R : Functor D C}
  (L⊣R : L ⊣ R)

The composition of R.₁ with the adjunction counit natural transformation gives R an Algebra structure, thus extending R to a functor

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.₁ ( _ _ _) βŸ©β‰‘
    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 ( _ _ _)) βŸ©β‰‘
    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 as the category of

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