Documentation

Mathlib.CategoryTheory.Monad.Adjunction

Adjunctions and monads #

We develop the basic relationship between adjunctions and monads.

Given an adjunction h : L ⊣ R, we have h.toMonad : Monad C and h.toComonad : Comonad D. We then have Monad.comparison (h : L ⊣ R) : D ⥤ h.toMonad.algebra sending Y : D to the Eilenberg-Moore algebra for L ⋙ R with underlying object R.obj X, and dually Comonad.comparison.

We say R : D ⥤ C is MonadicRightAdjoint, if it is a right adjoint and its Monad.comparison is an equivalence of categories. (Similarly for ComonadicLeftAdjoint.)

Finally we prove that reflective functors are MonadicRightAdjoint.

For a pair of functors L : C ⥤ D, R : D ⥤ C, an adjunction h : L ⊣ R induces a monad on the category C.

Instances For

    For a pair of functors L : C ⥤ D, R : D ⥤ C, an adjunction h : L ⊣ R induces a comonad on the category D.

    Instances For

      The monad induced by the Eilenberg-Moore adjunction is the original monad.

      Instances For

        The comonad induced by the Eilenberg-Moore adjunction is the original comonad.

        Instances For

          Given any adjunction L ⊣ R, there is a comparison functor CategoryTheory.Monad.comparison R sending objects Y : D to Eilenberg-Moore algebras for L ⋙ R with underlying object R.obj X.

          We later show that this is full when R is full, faithful when R is faithful, and essentially surjective when R is reflective.

          Instances For

            Given any adjunction L ⊣ R, there is a comparison functor CategoryTheory.Comonad.comparison L sending objects X : C to Eilenberg-Moore coalgebras for L ⋙ R with underlying object L.obj X.

            Instances For

              A right adjoint functor R : D ⥤ C is monadic if the comparison functor Monad.comparison R from D to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.

              Instances

                A left adjoint functor L : C ⥤ D is comonadic if the comparison functor Comonad.comparison L from C to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.

                Instances

                  Any reflective inclusion has a monadic right adjoint. cf Prop 5.3.3 of [Riehl][riehl2017]