Adjunctions and monads

We develop the basic relationship between adjunctions and 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.

@[simp]

theorem CategoryTheory.Adjunction.toMonad_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : (CategoryTheory.Adjunction.toMonad h).toFunctor = CategoryTheory.Functor.comp L R

@[simp]

theorem CategoryTheory.Adjunction.toMonad_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Monad.μ (CategoryTheory.Adjunction.toMonad h) = CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft L h.counit) R

@[simp]

theorem CategoryTheory.Adjunction.toMonad_η {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Monad.η (CategoryTheory.Adjunction.toMonad h) = h.unit

def CategoryTheory.Adjunction.toMonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.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.toComonad_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : (CategoryTheory.Adjunction.toComonad h).toFunctor = CategoryTheory.Functor.comp R L

@[simp]

theorem CategoryTheory.Adjunction.toComonad_δ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Comonad.δ (CategoryTheory.Adjunction.toComonad h) = CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft R h.unit) L

@[simp]

theorem CategoryTheory.Adjunction.toComonad_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Comonad.ε (CategoryTheory.Adjunction.toComonad h) = h.counit

def CategoryTheory.Adjunction.toComonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.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.adjToMonadIso_hom_toNatTrans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : (CategoryTheory.Adjunction.adjToMonadIso T).hom.app X = CategoryTheory.CategoryStruct.id (T.obj X)

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem CategoryTheory.Monad.comparison_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D) : ((CategoryTheory.Monad.comparison h).obj X).a = R.map (h.counit.app X)

@[simp]

theorem CategoryTheory.Monad.comparison_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : ∀ {X Y : D} (f : X ⟶ Y), ((CategoryTheory.Monad.comparison h).map f).f = R.map f

@[simp]

theorem CategoryTheory.Monad.comparison_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D) : ((CategoryTheory.Monad.comparison h).obj X).A = R.obj X

def CategoryTheory.Monad.comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor D (CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad h))

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.comparisonForget_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D) : (CategoryTheory.Monad.comparisonForget h).hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Monad.comparison h) (CategoryTheory.Monad.forget (CategoryTheory.Adjunction.toMonad h))).obj X)

@[simp]

theorem CategoryTheory.Monad.comparisonForget_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D) : (CategoryTheory.Monad.comparisonForget h).inv.app X = CategoryTheory.CategoryStruct.id (R.obj X)

def CategoryTheory.Monad.comparisonForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor.comp (CategoryTheory.Monad.comparison h) (CategoryTheory.Monad.forget (CategoryTheory.Adjunction.toMonad h)) ≅ R

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

theorem CategoryTheory.Monad.left_comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor.comp L (CategoryTheory.Monad.comparison h) = CategoryTheory.Monad.free (CategoryTheory.Adjunction.toMonad h)

instance CategoryTheory.instFaithfulAlgebraToMonadEilenbergMooreComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} [CategoryTheory.Faithful R] (h : L ⊣ R) : CategoryTheory.Faithful (CategoryTheory.Monad.comparison h)

instance CategoryTheory.instFullAlgebraEilenbergMooreToMonadFreeForgetAdjComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Full (CategoryTheory.Monad.comparison (CategoryTheory.Monad.adj T))

instance CategoryTheory.instEssSurjAlgebraToMonadEilenbergMooreFreeForgetAdjComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.EssSurj (CategoryTheory.Monad.comparison (CategoryTheory.Monad.adj T))

@[simp]

theorem CategoryTheory.Comonad.comparison_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : C) : ((CategoryTheory.Comonad.comparison h).obj X).A = L.obj X

@[simp]

theorem CategoryTheory.Comonad.comparison_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : C) : ((CategoryTheory.Comonad.comparison h).obj X).a = L.map (h.unit.app X)

@[simp]

theorem CategoryTheory.Comonad.comparison_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : ∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Comonad.comparison h).map f).f = L.map f

def CategoryTheory.Comonad.comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor C (CategoryTheory.Comonad.Coalgebra (CategoryTheory.Adjunction.toComonad h))

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.comparisonForget_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : C) : (CategoryTheory.Comonad.comparisonForget h).hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Comonad.comparison h) (CategoryTheory.Comonad.forget (CategoryTheory.Adjunction.toComonad h))).obj X)

@[simp]

theorem CategoryTheory.Comonad.comparisonForget_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : C) : (CategoryTheory.Comonad.comparisonForget h).inv.app X = CategoryTheory.CategoryStruct.id (L.obj X)

def CategoryTheory.Comonad.comparisonForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor.comp (CategoryTheory.Comonad.comparison h) (CategoryTheory.Comonad.forget (CategoryTheory.Adjunction.toComonad h)) ≅ L

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

theorem CategoryTheory.Comonad.left_comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor.comp R (CategoryTheory.Comonad.comparison h) = CategoryTheory.Comonad.cofree (CategoryTheory.Adjunction.toComonad h)

instance CategoryTheory.Comonad.comparison_faithful_of_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} [CategoryTheory.Faithful L] (h : L ⊣ R) : CategoryTheory.Faithful (CategoryTheory.Comonad.comparison h)

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

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

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

• left : CategoryTheory.Functor C D
• adj : CategoryTheory.IsRightAdjoint.left R ⊣ R
• eqv : CategoryTheory.IsEquivalence (CategoryTheory.Monad.comparison (CategoryTheory.Adjunction.ofRightAdjoint R))

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.

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

• right : CategoryTheory.Functor D C
• adj : L ⊣ CategoryTheory.IsLeftAdjoint.right L
• eqv : CategoryTheory.IsEquivalence (CategoryTheory.Comonad.comparison (CategoryTheory.Adjunction.ofLeftAdjoint L))

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.

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

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

instance CategoryTheory.μ_iso_of_reflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] : CategoryTheory.IsIso (CategoryTheory.Monad.μ (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint R)))

instance CategoryTheory.Reflective.instIsIsoObjToQuiverToCategoryStructToPrefunctorIdAToMonadLeftAdjointToIsRightAdjointOfRightAdjointCompAppUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] (X : CategoryTheory.Monad.Algebra (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint R))) : CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofRightAdjoint R).unit.app X.A)

instance CategoryTheory.Reflective.comparison_essSurj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] : CategoryTheory.EssSurj (CategoryTheory.Monad.comparison (CategoryTheory.Adjunction.ofRightAdjoint R))

instance CategoryTheory.Reflective.comparisonFull {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Full R] [CategoryTheory.IsRightAdjoint R] : CategoryTheory.Full (CategoryTheory.Monad.comparison (CategoryTheory.Adjunction.ofRightAdjoint R))

noncomputable instance CategoryTheory.monadicOfReflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] : CategoryTheory.MonadicRightAdjoint R

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