# 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) :
@[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.

Equations
Instances For
@[simp]
theorem CategoryTheory.Adjunction.toComonad_δ {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
@[simp]
theorem CategoryTheory.Adjunction.toComonad_coe {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.

Equations
• h.toComonad = { toFunctor := R.comp L, ε' := h.counit, δ' := , coassoc' := , left_counit' := , right_counit' := }
Instances For

Equations
Instances For

Equations
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.obj 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.map (h.counit.app 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Monad.comparisonForget_inv_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : D) :
@[simp]
theorem CategoryTheory.Monad.comparisonForget_hom_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : D) :
.app X = CategoryTheory.CategoryStruct.id ((.comp h.toMonad.forget).obj X)
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Monad.left_comparison {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) :
instance CategoryTheory.instFaithfulAlgebraToMonadComparison {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } [R.Faithful] (h : L R) :
.Faithful
Equations
• =
().Full
Equations
• =
().EssSurj
Equations
• =
@[simp]
theorem CategoryTheory.Comonad.comparison_obj_a {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : C) :
( 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), ( f).f = L.map f
@[simp]
theorem CategoryTheory.Comonad.comparison_obj_A {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : C) :
( X).A = L.obj X
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Comonad.comparisonForget_inv_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : C) :
@[simp]
theorem CategoryTheory.Comonad.comparisonForget_hom_app {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (h : L R) (X : C) :
.app X = CategoryTheory.CategoryStruct.id ((.comp h.toComonad.forget).obj X)
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.

Equations
• One or more equations did not get rendered due to their size.
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 : } [L.Faithful] (h : L R) :
.Faithful
Equations
• =
Equations
• =
.EssSurj
Equations
• =
class CategoryTheory.MonadicRightAdjoint {C : Type u₁} [] {D : Type u₂} [] (R : ) :
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 :

a choice of left adjoint for R

R is a right adjoint

Instances
theorem CategoryTheory.MonadicRightAdjoint.eqv {C : Type u₁} [] {D : Type u₂} [] {R : } [self : ] :
def CategoryTheory.monadicLeftAdjoint {C : Type u₁} [] {D : Type u₂} [] (R : ) :

The left adjoint functor to R given by [MonadicRightAdjoint R].

Equations
Instances For
def CategoryTheory.monadicAdjunction {C : Type u₁} [] {D : Type u₂} [] (R : ) :

The adjunction monadicLeftAdjoint R ⊣ R given by [MonadicRightAdjoint R].

Equations
Instances For
.IsEquivalence
Equations
• =
Equations
• =
noncomputable instance CategoryTheory.instMonadicRightAdjointAlgebraForget {C : Type u₁} [] (T : ) :
Equations
• = { L := T.free, adj := T.adj, eqv := }
class CategoryTheory.ComonadicLeftAdjoint {C : Type u₁} [] {D : Type u₂} [] (L : ) :
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 :

a choice of right adjoint for L

L is a right adjoint

Instances
theorem CategoryTheory.ComonadicLeftAdjoint.eqv {C : Type u₁} [] {D : Type u₂} [] {L : } [self : ] :
def CategoryTheory.comonadicRightAdjoint {C : Type u₁} [] {D : Type u₂} [] (L : ) :

The right adjoint functor to L given by [ComonadicLeftAdjoint L].

Equations
Instances For
def CategoryTheory.comonadicAdjunction {C : Type u₁} [] {D : Type u₂} [] (L : ) :

The adjunction L ⊣ comonadicRightAdjoint L given by [ComonadicLeftAdjoint L].

Equations
Instances For
.IsEquivalence
Equations
• =
Equations
• =
noncomputable instance CategoryTheory.instComonadicLeftAdjointCoalgebraForget {C : Type u₁} [] (G : ) :
Equations
• = { R := G.cofree, adj := G.adj, eqv := }
instance CategoryTheory.μ_iso_of_reflective {C : Type u₁} [] {D : Type u₂} [] {R : } :
Equations
• =
instance CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA {C : Type u₁} [] {D : Type u₂} [] {R : } (X : .toMonad.Algebra) :
CategoryTheory.IsIso (.unit.app X.A)
Equations
• =
instance CategoryTheory.Reflective.comparison_essSurj {C : Type u₁} [] {D : Type u₂} [] {R : } :
Equations
• =
theorem CategoryTheory.Reflective.comparison_full {C : Type u₁} [] {D : Type u₂} [] {R : } [R.Full] {L : } (adj : L R) :
.Full
@[instance 100]
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]

Equations
• CategoryTheory.monadicOfReflective = { L := , adj := , eqv := }