# mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given an adjunction h : L ⊣ R, we have h.to_monad : monad C and h.to_comonad : comonad D. We then have monad.comparison (h : L ⊣ R) : D ⥤ h.to_monad.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 monadic_right_adjoint, if it is a right adjoint and its monad.comparison is an equivalence of categories. (Similarly for monadic_left_adjoint.)

Finally we prove that reflective functors are monadic_right_adjoint.

@[simp]
theorem category_theory.adjunction.to_monad_coe {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
@[simp]
theorem category_theory.adjunction.to_monad_η {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
def category_theory.adjunction.to_monad {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (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
@[simp]
theorem category_theory.adjunction.to_monad_μ {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
@[simp]
theorem category_theory.adjunction.to_comonad_ε {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
def category_theory.adjunction.to_comonad {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (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
@[simp]
theorem category_theory.adjunction.to_comonad_δ {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
@[simp]
theorem category_theory.adjunction.to_comonad_coe {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :

Equations

Equations
def category_theory.monad.comparison {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :

Gven any adjunction L ⊣ R, there is a comparison functor category_theory.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
Instances for category_theory.monad.comparison
@[simp]
theorem category_theory.monad.comparison_obj_A {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X : D) :
.A = R.obj X
@[simp]
theorem category_theory.monad.comparison_obj_a {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X : D) :
.a = R.map (h.counit.app X)
@[simp]
theorem category_theory.monad.comparison_map_f {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X Y : D) (f : X Y) :
.f = R.map f
@[simp]
theorem category_theory.monad.comparison_forget_hom_app {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X : D) :
@[simp]
theorem category_theory.monad.comparison_forget_inv_app {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X : D) :
= 𝟙 (R.obj X)
def category_theory.monad.comparison_forget {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :

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

Equations
theorem category_theory.monad.left_comparison {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
@[protected, instance]
def category_theory.monad.comparison.faithful {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem category_theory.comonad.comparison_obj_a {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X : C) :
.a = L.map (h.unit.app X)
@[simp]
theorem category_theory.comonad.comparison_map_f {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X Y : C) (f : X Y) :
.f = L.map f
def category_theory.comonad.comparison {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :

Gven any adjunction L ⊣ R, there is a comparison functor category_theory.comonad.comparison L sending objects X : C to Eilenberg-Moore coalgebras for L ⋙ R with underlying object L.obj X.

Equations
Instances for category_theory.comonad.comparison
@[simp]
theorem category_theory.comonad.comparison_obj_A {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X : C) :
.A = L.obj X
@[simp]
theorem category_theory.comonad.comparison_forget_hom_app {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X : C) :
def category_theory.comonad.comparison_forget {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :

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

Equations
@[simp]
theorem category_theory.comonad.comparison_forget_inv_app {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) (X : C) :
= 𝟙 (L.obj X)
theorem category_theory.comonad.left_comparison {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
@[protected, instance]
def category_theory.comonad.comparison_faithful_of_faithful {C : Type u₁} {D : Type u₂} {L : C D} {R : D C} (h : L R) :
@[protected, instance]
Equations
@[protected, instance]
@[class]
structure category_theory.monadic_right_adjoint {C : Type u₁} {D : Type u₂} (R : D C) :
Type (max u₁ u₂ v₁ v₂)
• eqv :

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 of this typeclass
Instances of other typeclasses for category_theory.monadic_right_adjoint
@[class]
structure category_theory.comonadic_left_adjoint {C : Type u₁} {D : Type u₂} (L : C D) :
Type (max u₁ u₂ v₁ v₂)
• eqv :

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 of this typeclass
Instances of other typeclasses for category_theory.comonadic_left_adjoint
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def category_theory.μ_iso_of_reflective {C : Type u₁} {D : Type u₂} {R : D C}  :
@[protected, instance]
def category_theory.reflective.app.category_theory.is_iso {C : Type u₁} {D : Type u₂} {R : D C}  :
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
noncomputable def category_theory.monadic_of_reflective {C : Type u₁} {D : Type u₂} {R : D C}  :

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

Equations