mathlib documentation

category_theory.monad.adjunction

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

The monad induced by the Eilenberg-Moore adjunction is the original monad.

Equations
def category_theory.monad.comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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
@[simp]
theorem category_theory.monad.comparison_obj_A {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) (X : D) :
@[simp]
theorem category_theory.monad.comparison_obj_a {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) (X : D) :
@[simp]
theorem category_theory.monad.comparison_map_f {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) (X Y : D) (f : X Y) :
@[simp]
theorem category_theory.monad.comparison_forget_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) (X : D) :

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

Equations
theorem category_theory.monad.left_comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) :
@[simp]
theorem category_theory.comonad.comparison_obj_a {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) (X : C) :
@[simp]
theorem category_theory.comonad.comparison_map_f {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) (X Y : C) (f : X Y) :
def category_theory.comonad.comparison {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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
@[simp]
theorem category_theory.comonad.comparison_obj_A {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (h : L R) (X : C) :

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

Instances