Adjunctions and (co)monads #
We develop the basic relationship between adjunctions and (co)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
and coreflective functors are
ComonadicLeftAdjoint
.
For a pair of functors L : C ⥤ D
, R : D ⥤ C
, an adjunction h : L ⊣ R
induces a monad on
the category C
.
Equations
- h.toMonad = { toFunctor := L.comp R, η := h.unit, μ := CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft L h.counit) R, assoc := ⋯, left_unit := ⋯, right_unit := ⋯ }
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
.
Equations
- h.toComonad = { toFunctor := R.comp L, ε := h.counit, δ := CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft R h.unit) L, coassoc := ⋯, left_counit := ⋯, right_counit := ⋯ }
Instances For
The monad induced by the Eilenberg-Moore adjunction is the original monad.
Equations
- CategoryTheory.Adjunction.adjToMonadIso T = CategoryTheory.MonadIso.mk (CategoryTheory.NatIso.ofComponents (fun (X : C) => CategoryTheory.Iso.refl (T.adj.toMonad.obj X)) ⋯) ⋯ ⋯
Instances For
The comonad induced by the Eilenberg-Moore adjunction is the original comonad.
Equations
- CategoryTheory.Adjunction.adjToComonadIso G = CategoryTheory.ComonadIso.mk (CategoryTheory.NatIso.ofComponents (fun (X : C) => CategoryTheory.Iso.refl (G.adj.toComonad.obj X)) ⋯) ⋯ ⋯
Instances For
Given an adjunction L ⊣ R
, if L ⋙ R
is abstractly isomorphic to the identity functor, then the
unit is an isomorphism.
Equations
- adj.unitAsIsoOfIso i = { hom := adj.unit, inv := CategoryTheory.CategoryStruct.comp i.hom (adj.toMonad.transport i).μ, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Given an adjunction L ⊣ R
, if L ⋙ R
is isomorphic to the identity functor, then L
is
fully faithful.
Equations
- adj.fullyFaithfulLOfCompIsoId i = adj.fullyFaithfulLOfIsIsoUnit
Instances For
Given an adjunction L ⊣ R
, if R ⋙ L
is abstractly isomorphic to the identity functor, then the
counit is an isomorphism.
Equations
- adj.counitAsIsoOfIso j = { hom := adj.counit, inv := CategoryTheory.CategoryStruct.comp (adj.toComonad.transport j).δ j.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Given an adjunction L ⊣ R
, if R ⋙ L
is isomorphic to the identity functor, then R
is
fully faithful.
Equations
- adj.fullyFaithfulROfCompIsoId j = adj.fullyFaithfulROfIsIsoCounit
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.
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
.
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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.
- L : CategoryTheory.Functor C D
a choice of left adjoint for
R
- adj : CategoryTheory.MonadicRightAdjoint.L R ⊣ R
R
is a right adjoint - eqv : (CategoryTheory.Monad.comparison CategoryTheory.MonadicRightAdjoint.adj).IsEquivalence
Instances
The left adjoint functor to R
given by [MonadicRightAdjoint R]
.
Instances For
The adjunction monadicLeftAdjoint R ⊣ R
given by [MonadicRightAdjoint R]
.
Equations
- CategoryTheory.monadicAdjunction R = CategoryTheory.MonadicRightAdjoint.adj
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- CategoryTheory.instMonadicRightAdjointAlgebraForget T = { L := T.free, adj := T.adj, eqv := ⋯ }
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.
- R : CategoryTheory.Functor D C
a choice of right adjoint for
L
- adj : L ⊣ CategoryTheory.ComonadicLeftAdjoint.R L
L
is a left adjoint - eqv : (CategoryTheory.Comonad.comparison CategoryTheory.ComonadicLeftAdjoint.adj).IsEquivalence
Instances
The right adjoint functor to L
given by [ComonadicLeftAdjoint L]
.
Instances For
The adjunction L ⊣ comonadicRightAdjoint L
given by [ComonadicLeftAdjoint L]
.
Equations
- CategoryTheory.comonadicAdjunction L = CategoryTheory.ComonadicLeftAdjoint.adj
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- CategoryTheory.instComonadicLeftAdjointCoalgebraForget G = { R := G.cofree, adj := G.adj, eqv := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Any reflective inclusion has a monadic right adjoint. cf Prop 5.3.3 of Riehl
Equations
- CategoryTheory.monadicOfReflective = { L := CategoryTheory.reflector R, adj := CategoryTheory.reflectorAdjunction R, eqv := ⋯ }
Any coreflective inclusion has a comonadic left adjoint. cf Dual statement of Prop 5.3.3 of Riehl
Equations
- CategoryTheory.comonadicOfCoreflective = { R := CategoryTheory.coreflector R, adj := CategoryTheory.coreflectorAdjunction R, eqv := ⋯ }