mathlib3 documentation

category_theory.monad.adjunction

Adjunctions and monads #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We develop the basic relationship between adjunctions and monads.

Given an adjunction h : L ⊣ R, we have h.to_monad : monad C and h.to_comonad : comonad D. We then have monad.comparison (h : L ⊣ R) : D ⥤ h.to_monad.algebra sending Y : D to the Eilenberg-Moore algebra for L ⋙ R with underlying object R.obj X, and dually comonad.comparison.

We say R : D ⥤ C is monadic_right_adjoint, if it is a right adjoint and its monad.comparison is an equivalence of categories. (Similarly for monadic_left_adjoint.)

Finally we prove that reflective functors are monadic_right_adjoint.

@[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) :

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) :

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) :
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
Instances for category_theory.monad.comparison
@[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]

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₁} [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
Instances for category_theory.comonad.comparison
@[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
@[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 of this typeclass
Instances of other typeclasses for category_theory.monadic_right_adjoint
  • category_theory.monadic_right_adjoint.has_sizeof_inst
@[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 of this typeclass
Instances of other typeclasses for category_theory.comonadic_left_adjoint
  • category_theory.comonadic_left_adjoint.has_sizeof_inst