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.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

@[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.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.comparison_forget h).hom.app X = 𝟙 ((category_theory.comonad.comparison h ⋙ h.to_comonad.forget).obj X)

source

@[simp]

theorem category_theory.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.comparison_forget h).inv.app X = 𝟙 (L.obj X)

source

def category_theory.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.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

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

category_theory.monadic_of_reflective

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.

source

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

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

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

@[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 R = {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

@[instance]

def category_theory.reflective.comparison_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D ⥤ C) [category_theory.faithful R] [category_theory.is_right_adjoint R] :

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

source

@[instance]

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 R = {to_is_right_adjoint := category_theory.reflective.to_is_right_adjoint _inst_3, eqv := category_theory.equivalence.equivalence_of_fully_faithfully_ess_surj (category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint R)) _}