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) :
@[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
- h.to_monad = {to_functor := L ⋙ R, η' := h.unit, μ' := category_theory.whisker_right (category_theory.whisker_left L h.counit) R, assoc' := _, left_unit' := _, right_unit' := _}
@[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) :
@[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) :
h.to_comonad.ε = h.counit
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
- h.to_comonad = {to_functor := R ⋙ L, ε' := h.counit, δ' := category_theory.whisker_right (category_theory.whisker_left R h.unit) L, coassoc' := _, left_counit' := _, right_counit' := _}
@[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) :
@[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) :
↑(h.to_comonad) = R ⋙ L
def
category_theory.adjunction.adj_to_monad_iso
{C : Type u₁}
[category_theory.category C]
(T : category_theory.monad C) :
The monad induced by the Eilenberg-Moore adjunction is the original monad.
Equations
- category_theory.adjunction.adj_to_monad_iso T = category_theory.monad_iso.mk (category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl (↑(T.adj.to_monad).obj X)) _) _ _
@[simp]
theorem
category_theory.adjunction.adj_to_monad_iso_hom_to_nat_trans_app
{C : Type u₁}
[category_theory.category C]
(T : category_theory.monad C)
(X : C) :
(category_theory.adjunction.adj_to_monad_iso T).hom.to_nat_trans.app X = 𝟙 (↑T.obj X)
@[simp]
theorem
category_theory.adjunction.adj_to_monad_iso_inv_to_nat_trans_app
{C : Type u₁}
[category_theory.category C]
(T : category_theory.monad C)
(X : C) :
(category_theory.adjunction.adj_to_monad_iso T).inv.to_nat_trans.app X = 𝟙 (↑T.obj X)
def
category_theory.adjunction.adj_to_comonad_iso
{C : Type u₁}
[category_theory.category C]
(G : category_theory.comonad C) :
G.adj.to_comonad ≅ G
The comonad induced by the Eilenberg-Moore adjunction is the original comonad.
Equations
@[simp]
theorem
category_theory.adjunction.adj_to_comonad_iso_inv_to_nat_trans_app
{C : Type u₁}
[category_theory.category C]
(G : category_theory.comonad C)
(X : C) :
(category_theory.adjunction.adj_to_comonad_iso G).inv.to_nat_trans.app X = 𝟙 (↑G.obj X)
@[simp]
theorem
category_theory.adjunction.adj_to_comonad_iso_hom_to_nat_trans_app
{C : Type u₁}
[category_theory.category C]
(G : category_theory.comonad C)
(X : C) :
(category_theory.adjunction.adj_to_comonad_iso G).hom.to_nat_trans.app X = 𝟙 (↑G.obj X)
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) :
((category_theory.monad.comparison h).obj X).A = R.obj X
@[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) :
((category_theory.monad.comparison h).map f).f = R.map f
@[simp]
theorem
category_theory.monad.comparison_forget_hom_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) :
(category_theory.monad.comparison_forget h).hom.app X = 𝟙 ((category_theory.monad.comparison h ⋙ h.to_monad.forget).obj X)
@[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) :
def
category_theory.monad.comparison_forget
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{L : C ⥤ D}
{R : D ⥤ C}
(h : L ⊣ R) :
The underlying object of (monad.comparison R).obj X is just R.obj X.
Equations
- category_theory.monad.comparison_forget h = {hom := {app := λ (X : D), 𝟙 ((category_theory.monad.comparison h ⋙ h.to_monad.forget).obj X), naturality' := _}, inv := {app := λ (X : D), 𝟙 (R.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
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) :
@[protected, instance]
def
category_theory.monad.comparison.faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{L : C ⥤ D}
{R : D ⥤ C}
[category_theory.faithful R]
(h : L ⊣ R) :
@[protected, instance]
def
category_theory.monad.comparison.full
{C : Type u₁}
[category_theory.category C]
(T : category_theory.monad C) :
@[protected, instance]
@[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) :
((category_theory.comonad.comparison h).map f).f = L.map f
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) :
C ⥤ h.to_comonad.coalgebra
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) :
((category_theory.comonad.comparison h).obj X).A = L.obj X
@[simp]
theorem
category_theory.comonad.comparison_forget_hom_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) :
def
category_theory.comonad.comparison_forget
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{L : C ⥤ D}
{R : D ⥤ C}
(h : L ⊣ R) :
The underlying object of (comonad.comparison L).obj X is just L.obj X.
Equations
- category_theory.comonad.comparison_forget h = {hom := {app := λ (X : C), 𝟙 ((category_theory.comonad.comparison h ⋙ h.to_comonad.forget).obj X), naturality' := _}, inv := {app := λ (X : C), 𝟙 (L.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
theorem
category_theory.comonad.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) :
@[protected, instance]
def
category_theory.comonad.comparison_faithful_of_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{L : C ⥤ D}
{R : D ⥤ C}
[category_theory.faithful L]
(h : L ⊣ R) :
@[protected, instance]
def
category_theory.comonad.comparison.full
{C : Type u₁}
[category_theory.category C]
(G : category_theory.comonad C) :
@[protected, instance]
@[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₂)
- to_is_right_adjoint : category_theory.is_right_adjoint R
- eqv : category_theory.is_equivalence (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint 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 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₂)
- to_is_left_adjoint : category_theory.is_left_adjoint L
- eqv : category_theory.is_equivalence (category_theory.comonad.comparison (category_theory.adjunction.of_left_adjoint 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.
Instances of this typeclass
Instances of other typeclasses for category_theory.comonadic_left_adjoint
- category_theory.comonadic_left_adjoint.has_sizeof_inst
@[protected, instance]
noncomputable
def
category_theory.monad.forget.monadic_right_adjoint
{C : Type u₁}
[category_theory.category C]
(T : category_theory.monad C) :
@[protected, instance]
noncomputable
def
category_theory.comonad.forget.comonadic_left_adjoint
{C : Type u₁}
[category_theory.category C]
(G : category_theory.comonad C) :
@[protected, instance]
def
category_theory.μ_iso_of_reflective
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{R : D ⥤ C}
[category_theory.reflective R] :
@[protected, instance]
def
category_theory.reflective.app.category_theory.is_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{R : D ⥤ C}
[category_theory.reflective R]
(X : (category_theory.adjunction.of_right_adjoint R).to_monad.algebra) :
@[protected, instance]
def
category_theory.reflective.comparison_ess_surj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{R : D ⥤ C}
[category_theory.reflective R] :
@[protected, instance]
def
category_theory.reflective.comparison_full
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{R : D ⥤ C}
[category_theory.full R]
[category_theory.is_right_adjoint R] :
Equations
- category_theory.reflective.comparison_full = {preimage := λ (X Y : D) (f : (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint R)).obj X ⟶ (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint R)).obj Y), R.preimage f.f, witness' := _}
@[protected, instance]
noncomputable
def
category_theory.monadic_of_reflective
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{R : D ⥤ C}
[category_theory.reflective R] :
Any reflective inclusion has a monadic right adjoint. cf Prop 5.3.3 of Riehl
Equations
- category_theory.monadic_of_reflective = {to_is_right_adjoint := category_theory.reflective.to_is_right_adjoint _inst_3, eqv := category_theory.equivalence.of_fully_faithfully_ess_surj (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint R)) category_theory.reflective.comparison_ess_surj}