Equations
- category_theory.adjunction.monad R = {η := (category_theory.adjunction.of_right_adjoint R).unit, μ := category_theory.whisker_right (category_theory.whisker_left (category_theory.left_adjoint R) (category_theory.adjunction.of_right_adjoint R).counit) R, assoc' := _, left_unit' := _, right_unit' := _}
Equations
- category_theory.adjunction.comonad L = {ε := (category_theory.adjunction.of_left_adjoint L).counit, δ := category_theory.whisker_right (category_theory.whisker_left (category_theory.right_adjoint L) (category_theory.adjunction.of_left_adjoint L).unit) L, coassoc' := _, left_counit' := _, right_counit' := _}
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.
The underlying object of (monad.comparison R).obj X
is just R.obj X
.
Equations
- category_theory.monad.comparison_forget R = {hom := {app := λ (X : D), 𝟙 ((category_theory.monad.comparison R ⋙ category_theory.monad.forget (category_theory.left_adjoint R ⋙ R)).obj X), naturality' := _}, inv := {app := λ (X : D), 𝟙 (R.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
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
.
The underlying object of (comonad.comparison L).obj X
is just L.obj X
.
Equations
- category_theory.comonad.comparison_forget L = {hom := {app := λ (X : C), 𝟙 ((category_theory.comonad.comparison L ⋙ category_theory.comonad.forget (category_theory.right_adjoint L ⋙ L)).obj X), naturality' := _}, inv := {app := λ (X : C), 𝟙 (L.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
- to_is_right_adjoint : category_theory.is_right_adjoint R
- eqv : category_theory.is_equivalence (category_theory.monad.comparison R)
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
- to_is_left_adjoint : category_theory.is_left_adjoint L
- eqv : category_theory.is_equivalence (category_theory.comonad.comparison L)
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.
Equations
- category_theory.reflective.app.category_theory.is_iso R X = {inv := X.a, hom_inv_id' := _, inv_hom_id' := _}
Equations
- category_theory.reflective.comparison_full R = {preimage := λ (X Y : D) (f : (category_theory.monad.comparison R).obj X ⟶ (category_theory.monad.comparison R).obj Y), R.preimage f.f, witness' := _}
Any reflective inclusion has a monadic right adjoint. cf Prop 5.3.3 of [Riehl][riehl2017]