mathlib documentation

category_theory.monad.adjunction

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]

@[simp]

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
@[class]
structure category_theory.monadic_right_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D C) :
Type (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]
structure category_theory.comonadic_left_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (L : C D) :
Type (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.