Documentation

Mathlib.CategoryTheory.Monad.Adjunction

Adjunctions and monads #

We develop the basic relationship between adjunctions and monads.

Given an adjunction h : LR, 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 LR 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.

@[simp]

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

Equations
Instances For
    @[simp]

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

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For

          Given any adjunction LR, there is a comparison functor CategoryTheory.Monad.comparison R sending objects Y : D to Eilenberg-Moore algebras for LR 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.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The underlying object of (Monad.comparison R).obj X is just R.obj X.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                The underlying object of (Comonad.comparison L).obj X is just L.obj X.

                Equations
                • One or more equations did not get rendered due to their size.
                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

                    The adjunction monadicLeftAdjoint RR given by [MonadicRightAdjoint R].

                    Equations
                    Instances For

                      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
                        @[instance 100]

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

                        Equations