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.
def
CategoryTheory.Adjunction.toMonad
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
Monad C
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 := ⋯ }
@[simp]
theorem
CategoryTheory.Adjunction.toMonad_coe
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
@[simp]
theorem
CategoryTheory.Adjunction.toMonad_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
@[simp]
theorem
CategoryTheory.Adjunction.toMonad_η
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
def
CategoryTheory.Adjunction.toComonad
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
Comonad D
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 := ⋯ }
@[simp]
theorem
CategoryTheory.Adjunction.toComonad_coe
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
@[simp]
theorem
CategoryTheory.Adjunction.toComonad_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
@[simp]
theorem
CategoryTheory.Adjunction.toComonad_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
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)) ⋯) ⋯ ⋯
@[simp]
theorem
CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(T : Monad C)
(X : C)
:
@[simp]
theorem
CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(T : Monad C)
(X : C)
:
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)) ⋯) ⋯ ⋯
@[simp]
theorem
CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(G : Comonad C)
(X : C)
:
@[simp]
theorem
CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app
{C : Type u₁}
[Category.{v₁, u₁} C]
(G : Comonad C)
(X : C)
:
def
CategoryTheory.Adjunction.unitAsIsoOfIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
(i : L.comp R ≅ Functor.id C)
:
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 := ⋯ }
theorem
CategoryTheory.Adjunction.isIso_unit_of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
(i : L.comp R ≅ Functor.id C)
:
noncomputable def
CategoryTheory.Adjunction.fullyFaithfulLOfCompIsoId
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
(i : L.comp R ≅ Functor.id C)
:
Given an adjunction L ⊣ R, if L ⋙ R is isomorphic to the identity functor, then L is
fully faithful.
Equations
def
CategoryTheory.Adjunction.counitAsIsoOfIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
(j : R.comp L ≅ Functor.id D)
:
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 := ⋯ }
theorem
CategoryTheory.Adjunction.isIso_counit_of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
(j : R.comp L ≅ Functor.id D)
:
noncomputable def
CategoryTheory.Adjunction.fullyFaithfulROfCompIsoId
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
(j : R.comp L ≅ Functor.id D)
:
Given an adjunction L ⊣ R, if R ⋙ L is isomorphic to the identity functor, then R is
fully faithful.
Equations
def
CategoryTheory.Monad.comparison
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
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.
@[simp]
theorem
CategoryTheory.Monad.comparison_obj_a
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
(X : D)
:
@[simp]
theorem
CategoryTheory.Monad.comparison_obj_A
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
(X : D)
:
@[simp]
theorem
CategoryTheory.Monad.comparison_map_f
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
{X✝ Y✝ : D}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.Monad.comparisonForget
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
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.
@[simp]
theorem
CategoryTheory.Monad.comparisonForget_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
(x✝ : D)
:
@[simp]
theorem
CategoryTheory.Monad.comparisonForget_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
(x✝ : D)
:
theorem
CategoryTheory.Monad.left_comparison
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
instance
CategoryTheory.instFaithfulAlgebraToMonadComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
[R.Faithful]
(h : L ⊣ R)
:
instance
CategoryTheory.instFullAlgebraToMonadAdjComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
(T : Monad C)
:
(Monad.comparison T.adj).Full
instance
CategoryTheory.instEssSurjAlgebraToMonadAdjComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
(T : Monad C)
:
def
CategoryTheory.Comonad.comparison
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
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.
@[simp]
theorem
CategoryTheory.Comonad.comparison_obj_A
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
(X : C)
:
@[simp]
theorem
CategoryTheory.Comonad.comparison_obj_a
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
(X : C)
:
@[simp]
theorem
CategoryTheory.Comonad.comparison_map_f
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
:
def
CategoryTheory.Comonad.comparisonForget
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
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.
@[simp]
theorem
CategoryTheory.Comonad.comparisonForget_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
(x✝ : C)
:
@[simp]
theorem
CategoryTheory.Comonad.comparisonForget_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
(x✝ : C)
:
(comparisonForget h).hom.app x✝ = CategoryStruct.id (((comparison h).comp h.toComonad.forget).obj x✝)
theorem
CategoryTheory.Comonad.left_comparison
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(h : L ⊣ R)
:
instance
CategoryTheory.Comonad.comparison_faithful_of_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
[L.Faithful]
(h : L ⊣ R)
:
(comparison h).Faithful
instance
CategoryTheory.instFullCoalgebraToComonadAdjComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
(G : Comonad C)
:
instance
CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
(G : Comonad C)
:
class
CategoryTheory.MonadicRightAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(R : Functor D C)
:
Type (max (max (max u₁ u₂) v₁) v₂)
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 : Functor C D
a choice of left adjoint for
R Ris a right adjoint- eqv : (Monad.comparison adj).IsEquivalence
Instances
def
CategoryTheory.monadicLeftAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(R : Functor D C)
[MonadicRightAdjoint R]
:
Functor C D
The left adjoint functor to R given by [MonadicRightAdjoint R].
def
CategoryTheory.monadicAdjunction
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(R : Functor D C)
[MonadicRightAdjoint R]
:
The adjunction monadicLeftAdjoint R ⊣ R given by [MonadicRightAdjoint R].
instance
CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(R : Functor D C)
[MonadicRightAdjoint R]
:
instance
CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(R : Functor D C)
[MonadicRightAdjoint R]
:
noncomputable instance
CategoryTheory.instMonadicRightAdjointAlgebraForget
{C : Type u₁}
[Category.{v₁, u₁} C]
(T : Monad C)
:
Equations
- CategoryTheory.instMonadicRightAdjointAlgebraForget T = { L := T.free, adj := T.adj, eqv := ⋯ }
class
CategoryTheory.ComonadicLeftAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(L : Functor C D)
:
Type (max (max (max u₁ u₂) v₁) v₂)
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 : Functor D C
a choice of right adjoint for
L Lis a left adjoint- eqv : (Comonad.comparison adj).IsEquivalence
Instances
def
CategoryTheory.comonadicRightAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(L : Functor C D)
[ComonadicLeftAdjoint L]
:
Functor D C
The right adjoint functor to L given by [ComonadicLeftAdjoint L].
def
CategoryTheory.comonadicAdjunction
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(L : Functor C D)
[ComonadicLeftAdjoint L]
:
The adjunction L ⊣ comonadicRightAdjoint L given by [ComonadicLeftAdjoint L].
instance
CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(L : Functor C D)
[ComonadicLeftAdjoint L]
:
instance
CategoryTheory.instIsLeftAdjointOfComonadicLeftAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(L : Functor C D)
[ComonadicLeftAdjoint L]
:
noncomputable instance
CategoryTheory.instComonadicLeftAdjointCoalgebraForget
{C : Type u₁}
[Category.{v₁, u₁} C]
(G : Comonad C)
:
Equations
- CategoryTheory.instComonadicLeftAdjointCoalgebraForget G = { R := G.cofree, adj := G.adj, eqv := ⋯ }
instance
CategoryTheory.μ_iso_of_reflective
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[Reflective R]
:
instance
CategoryTheory.δ_iso_of_coreflective
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[Coreflective R]
:
instance
CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[Reflective R]
(X : (reflectorAdjunction R).toMonad.Algebra)
:
IsIso ((reflectorAdjunction R).unit.app X.A)
instance
CategoryTheory.Reflective.comparison_essSurj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[Reflective R]
:
theorem
CategoryTheory.Reflective.comparison_full
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[R.Full]
{L : Functor C D}
(adj : L ⊣ R)
:
(Monad.comparison adj).Full
instance
CategoryTheory.Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[Coreflective R]
(X : (coreflectorAdjunction R).toComonad.Coalgebra)
:
IsIso ((coreflectorAdjunction R).counit.app X.A)
instance
CategoryTheory.Coreflective.comparison_essSurj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[Coreflective R]
:
theorem
CategoryTheory.Coreflective.comparison_full
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[R.Full]
{L : Functor C D}
(adj : R ⊣ L)
:
(Comonad.comparison adj).Full
@[instance 100]
instance
CategoryTheory.monadicOfReflective
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[Reflective R]
:
Any reflective inclusion has a monadic right adjoint. cf Prop 5.3.3 of [Riehl][riehl2017]
Equations
- CategoryTheory.monadicOfReflective = { L := CategoryTheory.reflector R, adj := CategoryTheory.reflectorAdjunction R, eqv := ⋯ }
@[instance 100]
instance
CategoryTheory.comonadicOfCoreflective
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{R : Functor D C}
[Coreflective R]
:
Any coreflective inclusion has a comonadic left adjoint. cf Dual statement of Prop 5.3.3 of [Riehl][riehl2017]
Equations
- CategoryTheory.comonadicOfCoreflective = { R := CategoryTheory.coreflector R, adj := CategoryTheory.coreflectorAdjunction R, eqv := ⋯ }