# Documentation

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₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
().toFunctor =
@[simp]
theorem CategoryTheory.Adjunction.toMonad_μ {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
@[simp]
theorem CategoryTheory.Adjunction.toMonad_η {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
def CategoryTheory.Adjunction.toMonad {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :

For a pair of functors L : C ⥤ D, R : D ⥤ C, an adjunction h : L ⊣ R induces a monad on the category C.

Instances For
@[simp]
theorem CategoryTheory.Adjunction.toComonad_coe {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
().toFunctor =
@[simp]
theorem CategoryTheory.Adjunction.toComonad_δ {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
@[simp]
theorem CategoryTheory.Adjunction.toComonad_ε {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
def CategoryTheory.Adjunction.toComonad {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :

For a pair of functors L : C ⥤ D, R : D ⥤ C, an adjunction h : L ⊣ R induces a comonad on the category D.

Instances For

Instances For

Instances For
@[simp]
theorem CategoryTheory.Monad.comparison_obj_a {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : D) :
(().obj X).a = R.map (h.counit.app X)
@[simp]
theorem CategoryTheory.Monad.comparison_map_f {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
∀ {X Y : D} (f : X Y), (().map f).f = R.map f
@[simp]
theorem CategoryTheory.Monad.comparison_obj_A {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : D) :
(().obj X).A = R.obj X
def CategoryTheory.Monad.comparison {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (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.

Instances For
@[simp]
theorem CategoryTheory.Monad.comparisonForget_hom_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : D) :
@[simp]
theorem CategoryTheory.Monad.comparisonForget_inv_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : D) :
def CategoryTheory.Monad.comparisonForget {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :

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

Instances For
theorem CategoryTheory.Monad.left_comparison {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
instance CategoryTheory.instFaithfulAlgebraToMonadEilenbergMooreComparison {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
@[simp]
theorem CategoryTheory.Comonad.comparison_obj_A {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : C) :
(().obj X).A = L.obj X
@[simp]
theorem CategoryTheory.Comonad.comparison_obj_a {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : C) :
(().obj X).a = L.map (h.unit.app X)
@[simp]
theorem CategoryTheory.Comonad.comparison_map_f {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
∀ {X Y : C} (f : X Y), (().map f).f = L.map f
def CategoryTheory.Comonad.comparison {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (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.

Instances For
@[simp]
theorem CategoryTheory.Comonad.comparisonForget_hom_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : C) :
@[simp]
theorem CategoryTheory.Comonad.comparisonForget_inv_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : C) :
def CategoryTheory.Comonad.comparisonForget {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :

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

Instances For
theorem CategoryTheory.Comonad.left_comparison {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
instance CategoryTheory.Comonad.comparison_faithful_of_faithful {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
class CategoryTheory.MonadicRightAdjoint {C : Type u₁} [] {D : Type u₂} [] (R : ) extends :
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.

Instances
class CategoryTheory.ComonadicLeftAdjoint {C : Type u₁} [] {D : Type u₂} [] (L : ) extends :
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.

Instances
instance CategoryTheory.μ_iso_of_reflective {C : Type u₁} [] {D : Type u₂} [] {R : } :
instance CategoryTheory.Reflective.comparison_essSurj {C : Type u₁} [] {D : Type u₂} [] {R : } :
instance CategoryTheory.Reflective.comparisonFull {C : Type u₁} [] {D : Type u₂} [] {R : } :
noncomputable instance CategoryTheory.monadicOfReflective {C : Type u₁} [] {D : Type u₂} [] {R : } :

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