# mathlibdocumentation

@[simp]
theorem category_theory.adjunction.monad_μ {C : Type u₁} {D : Type u₂} (R : D C)  :

@[simp]
theorem category_theory.adjunction.monad_η {C : Type u₁} {D : Type u₂} (R : D C)  :

@[instance]
def category_theory.adjunction.monad {C : Type u₁} {D : Type u₂} (R : D C)  :

Equations
@[instance]
def category_theory.adjunction.comonad {C : Type u₁} {D : Type u₂} (L : C D)  :

Equations
@[simp]
theorem category_theory.adjunction.comonad_δ {C : Type u₁} {D : Type u₂} (L : C D)  :

@[simp]
theorem category_theory.adjunction.comonad_ε {C : Type u₁} {D : Type u₂} (L : C D)  :

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

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
@[simp]
theorem category_theory.monad.comparison_obj_A {C : Type u₁} {D : Type u₂} (R : D C) (X : D) :
.A = R.obj X

@[simp]
theorem category_theory.monad.comparison_obj_a {C : Type u₁} {D : Type u₂} (R : D C) (X : D) :
.a =

@[simp]
theorem category_theory.monad.comparison_map_f {C : Type u₁} {D : Type u₂} (R : D C) (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₂} (R : D C) (X : D) :

@[simp]
theorem category_theory.monad.comparison_forget_inv_app {C : Type u₁} {D : Type u₂} (R : D C) (X : D) :
= 𝟙 (R.obj X)

def category_theory.monad.comparison_forget {C : Type u₁} {D : Type u₂} (R : D C)  :

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

Equations
@[simp]
theorem category_theory.comonad.comparison_obj_a {C : Type u₁} {D : Type u₂} (L : C D) (X : C) :
.a =

@[simp]
theorem category_theory.comonad.comparison_map_f {C : Type u₁} {D : Type u₂} (L : C D) (X Y : C) (f : X Y) :
.f = L.map f

def category_theory.comonad.comparison {C : Type u₁} {D : Type u₂} (L : C D)  :

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
@[simp]
theorem category_theory.comonad.comparison_obj_A {C : Type u₁} {D : Type u₂} (L : C D) (X : C) :
.A = L.obj X

@[simp]
theorem category_theory.comonad.comparison_forget_hom_app {C : Type u₁} {D : Type u₂} (L : C D) (X : C) :

def category_theory.comonad.comparison_forget {C : Type u₁} {D : Type u₂} (L : C D)  :

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) (X : C) :
= 𝟙 (L.obj X)

@[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
@[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.

@[instance]
def category_theory.μ_iso_of_reflective {C : Type u₁} {D : Type u₂} (R : D C)  :

Equations
@[instance]
def category_theory.reflective.app.category_theory.is_iso {C : Type u₁} {D : Type u₂} (R : D C)  :

Equations
@[instance]
def category_theory.reflective.comparison_ess_surj {C : Type u₁} {D : Type u₂} (R : D C)  :

@[instance]
def category_theory.reflective.comparison_full {C : Type u₁} {D : Type u₂} (R : D C)  :

Equations
@[instance]
def category_theory.reflective.comparison_faithful {C : Type u₁} {D : Type u₂} (R : D C)  :

@[instance]
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][riehl2017]

Equations