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.

@[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) : h.toMonad.μ = Functor.whiskerRight (L.whiskerLeft h.counit) R

@[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) : h.toMonad.toFunctor = L.comp 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) : h.toMonad.η = h.unit

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.

@[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) : h.toComonad.δ = Functor.whiskerRight (R.whiskerLeft h.unit) L

@[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) : h.toComonad.ε = h.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) : h.toComonad.toFunctor = R.comp L

def CategoryTheory.Adjunction.adjToMonadIso {C : Type u₁} [Category.{v₁, u₁} C] (T : Monad C) : T.adj.toMonad ≅ T

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

@[simp]

theorem CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app {C : Type u₁} [Category.{v₁, u₁} C] (T : Monad C) (X : C) : (adjToMonadIso T).inv.app X = CategoryStruct.id (T.obj X)

@[simp]

theorem CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app {C : Type u₁} [Category.{v₁, u₁} C] (T : Monad C) (X : C) : (adjToMonadIso T).hom.app X = CategoryStruct.id (T.obj X)

def CategoryTheory.Adjunction.adjToComonadIso {C : Type u₁} [Category.{v₁, u₁} C] (G : Comonad C) : G.adj.toComonad ≅ G

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

@[simp]

theorem CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app {C : Type u₁} [Category.{v₁, u₁} C] (G : Comonad C) (X : C) : (adjToComonadIso G).hom.app X = CategoryStruct.id (G.obj X)

@[simp]

theorem CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app {C : Type u₁} [Category.{v₁, u₁} C] (G : Comonad C) (X : C) : (adjToComonadIso G).inv.app X = CategoryStruct.id (G.obj X)

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) : Functor.id C ≅ L.comp R

Given an adjunction L ⊣ R, if L ⋙ R is abstractly isomorphic to the identity functor, then the unit is an isomorphism.

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) : IsIso adj.unit

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) : L.FullyFaithful

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

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) : 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.

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) : IsIso adj.counit

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) : R.FullyFaithful

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

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) : Functor D h.toMonad.Algebra

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.

@[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) : ((comparison h).obj X).A = R.obj X

@[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) : ((comparison h).obj X).a = R.map (h.counit.app X)

@[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✝) : ((comparison h).map f).f = R.map f

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) : (comparison h).comp h.toMonad.forget ≅ R

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

@[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) : (comparisonForget h).inv.app x✝ = CategoryStruct.id (R.obj x✝)

@[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) : (comparisonForget h).hom.app x✝ = CategoryStruct.id (((comparison h).comp h.toMonad.forget).obj x✝)

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) : L.comp (comparison h) = h.toMonad.free

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) : (Monad.comparison h).Faithful

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) : (Monad.comparison T.adj).EssSurj

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) : Functor C h.toComonad.Coalgebra

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.

@[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) : ((comparison h).obj X).a = L.map (h.unit.app X)

@[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) : ((comparison h).obj X).A = L.obj X

@[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✝) : ((comparison h).map f).f = L.map f

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) : (comparison h).comp h.toComonad.forget ≅ L

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

@[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) : (comparisonForget h).inv.app x✝ = CategoryStruct.id (L.obj x✝)

@[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) : R.comp (comparison h) = h.toComonad.cofree

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) : (Comonad.comparison G.adj).Full

instance CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison {C : Type u₁} [Category.{v₁, u₁} C] (G : Comonad C) : (Comonad.comparison G.adj).EssSurj

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

• adj : L R ⊣ R

  R is a right adjoint

• eqv : (Monad.comparison adj).IsEquivalence

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] : monadicLeftAdjoint R ⊣ 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] : (Monad.comparison (monadicAdjunction R)).IsEquivalence

instance CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) [MonadicRightAdjoint R] : R.IsRightAdjoint

noncomputable instance CategoryTheory.instMonadicRightAdjointAlgebraForget {C : Type u₁} [Category.{v₁, u₁} C] (T : Monad C) : MonadicRightAdjoint T.forget

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

• adj : L ⊣ R L

  L is a left adjoint

• eqv : (Comonad.comparison adj).IsEquivalence

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] : L ⊣ comonadicRightAdjoint 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] : (Comonad.comparison (comonadicAdjunction L)).IsEquivalence

instance CategoryTheory.instIsLeftAdjointOfComonadicLeftAdjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor C D) [ComonadicLeftAdjoint L] : L.IsLeftAdjoint

noncomputable instance CategoryTheory.instComonadicLeftAdjointCoalgebraForget {C : Type u₁} [Category.{v₁, u₁} C] (G : Comonad C) : ComonadicLeftAdjoint G.forget

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] : IsIso (reflectorAdjunction R).toMonad.μ

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] : IsIso (coreflectorAdjunction R).toComonad.δ

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] : (Monad.comparison (reflectorAdjunction R)).EssSurj

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] : (Comonad.comparison (coreflectorAdjunction R)).EssSurj

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] : MonadicRightAdjoint R

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

@[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] : ComonadicLeftAdjoint R

Any coreflective inclusion has a comonadic left adjoint. cf Dual statement of Prop 5.3.3 of [Riehl][riehl2017]