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.
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 = Precategory C module D = Precategory D module L = Functor L module R = Functor R module adj = _β£_ Lβ£R LβR : Monad C LβR = AdjunctionβMonad Lβ£R open Monad 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.β (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
as the category of
-algebras:
is-monadic : Type _ is-monadic = is-equivalence Comparison