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]

@[class]
structure category_theory.reflective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] :
D CType (max u₁ u₂ v₁ v₂)

A functor is reflective, or a reflective inclusion, if it is fully faithful and right adjoint.

Instances
@[class]
structure category_theory.monadic_right_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] :
D CType (max u₁ u₂ v₁ v₂)

A right adjoint functor R : D ⥤ C is monadic if the comparison function monad.comparison R from D to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.

Instances