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

source

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

h.to_monad.η = h.unit

source

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

category_theory.monad C

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' := _}

source

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

h.to_monad.μ = category_theory.whisker_right (category_theory.whisker_left L h.counit) R

source

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

source

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

category_theory.comonad D

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' := _}

source

@[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.δ = category_theory.whisker_right (category_theory.whisker_left R h.unit) L

source

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

source

def category_theory.adjunction.adj_to_monad_iso {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

T.adj.to_monad ≅ T

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

source

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

source

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

source

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

category_theory.adjunction.adj_to_comonad_iso G = category_theory.comonad_iso.mk (category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl (↑(G.adj.to_comonad).obj X)) _) _ _

source

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

source

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

source

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

D ⥤ h.to_monad.algebra

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

category_theory.monad.comparison h = {obj := λ (X : D), {A := R.obj X, a := R.map (h.counit.app X), unit' := _, assoc' := _}, map := λ (X Y : D) (f : X ⟶ Y), {f := R.map f, h' := _}, map_id' := _, map_comp' := _}

source

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

source

@[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.map (h.counit.app X)

source

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

source

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

source

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

(category_theory.monad.comparison_forget h).inv.app X = 𝟙 (R.obj X)

source

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

category_theory.monad.comparison h ⋙ h.to_monad.forget ≅ 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' := _}

source

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

L ⋙ category_theory.monad.comparison h = h.to_monad.free

source

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

category_theory.faithful (category_theory.monad.comparison h)

source

@[protected, instance]

def category_theory.monad.comparison.full {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

category_theory.full (category_theory.monad.comparison T.adj)

Equations

category_theory.monad.comparison.full T = {preimage := λ (X Y : T.algebra) (f : (category_theory.monad.comparison T.adj).obj X ⟶ (category_theory.monad.comparison T.adj).obj Y), {f := f.f, h' := _}, witness' := _}

source

@[protected, instance]

def category_theory.monad.comparison.ess_surj {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

category_theory.ess_surj (category_theory.monad.comparison T.adj)

source

@[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.map (h.unit.app X)

source

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

source

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

category_theory.comonad.comparison h = {obj := λ (X : C), {A := L.obj X, a := L.map (h.unit.app X), counit' := _, coassoc' := _}, map := λ (X Y : C) (f : X ⟶ Y), {f := L.map f, h' := _}, map_id' := _, map_comp' := _}

source

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

source

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

(category_theory.comonad.comparison_forget h).hom.app X = 𝟙 ((category_theory.comonad.comparison h ⋙ h.to_comonad.forget).obj X)

source

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

category_theory.comonad.comparison h ⋙ h.to_comonad.forget ≅ L

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' := _}

source

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

(category_theory.comonad.comparison_forget h).inv.app X = 𝟙 (L.obj X)

source

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

R ⋙ category_theory.comonad.comparison h = h.to_comonad.cofree

source

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

category_theory.faithful (category_theory.comonad.comparison h)

source

@[protected, instance]

def category_theory.comonad.comparison.full {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

category_theory.full (category_theory.comonad.comparison G.adj)

Equations

category_theory.comonad.comparison.full G = {preimage := λ (X Y : G.coalgebra) (f : (category_theory.comonad.comparison G.adj).obj X ⟶ (category_theory.comonad.comparison G.adj).obj Y), {f := f.f, h' := _}, witness' := _}

source

@[protected, instance]

def category_theory.comonad.comparison.ess_surj {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

category_theory.ess_surj (category_theory.comonad.comparison G.adj)

source

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

source

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

category_theory.comonad.forget.comonadic_left_adjoint

source

@[protected, instance]

noncomputable def category_theory.monad.forget.monadic_right_adjoint {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

category_theory.monadic_right_adjoint T.forget

Equations

category_theory.monad.forget.monadic_right_adjoint T = {to_is_right_adjoint := category_theory.monad.forget.category_theory.is_right_adjoint T, eqv := category_theory.equivalence.of_fully_faithfully_ess_surj (category_theory.monad.comparison T.adj) _}

source

@[protected, instance]

noncomputable def category_theory.comonad.forget.comonadic_left_adjoint {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

category_theory.comonadic_left_adjoint G.forget

Equations

category_theory.comonad.forget.comonadic_left_adjoint G = {to_is_left_adjoint := category_theory.comonad.forget.category_theory.is_left_adjoint G, eqv := category_theory.equivalence.of_fully_faithfully_ess_surj (category_theory.comonad.comparison G.adj) _}

source

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

category_theory.is_iso (category_theory.adjunction.of_right_adjoint R).to_monad.μ

source

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

category_theory.is_iso ((category_theory.adjunction.of_right_adjoint R).unit.app X.A)

source

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

category_theory.ess_surj (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint R))

source

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

category_theory.full (category_theory.monad.comparison (category_theory.adjunction.of_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' := _}

source

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

category_theory.monadic_right_adjoint 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}