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 an adjunction LR, if LR is abstractly isomorphic to the identity functor, then the unit is an isomorphism.

          Equations
          Instances For

            Given an adjunction LR, if LR is isomorphic to the identity functor, then L is fully faithful.

            Equations
            • adj.fullyFaithfulLOfCompIsoId i = adj.fullyFaithfulLOfIsIsoUnit
            Instances For

              Given an adjunction LR, if RL is abstractly isomorphic to the identity functor, then the counit is an isomorphism.

              Equations
              Instances For

                Given an adjunction LR, if RL is isomorphic to the identity functor, then R is fully faithful.

                Equations
                • adj.fullyFaithfulROfCompIsoId j = adj.fullyFaithfulROfIsIsoCounit
                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