mathlib docs: category_theory.monad.adjunction

@[simp]

theorem category_theory.adjunction.monad_μ {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D ⥤ C) [category_theory.is_right_adjoint R] :

μ_ (category_theory.left_adjoint R ⋙ R) = category_theory.whisker_right (category_theory.whisker_left (category_theory.left_adjoint R) (category_theory.adjunction.of_right_adjoint R).counit) R

source

@[simp]

theorem category_theory.adjunction.monad_η {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D ⥤ C) [category_theory.is_right_adjoint R] :

η_ (category_theory.left_adjoint R ⋙ R) = (category_theory.adjunction.of_right_adjoint R).unit

source

@[instance]

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

category_theory.monad (category_theory.left_adjoint R ⋙ R)

Equations

category_theory.adjunction.monad R = {η := (category_theory.adjunction.of_right_adjoint R).unit, μ := category_theory.whisker_right (category_theory.whisker_left (category_theory.left_adjoint R) (category_theory.adjunction.of_right_adjoint R).counit) R, assoc' := _, left_unit' := _, right_unit' := _}

source

@[instance]

def category_theory.adjunction.comonad {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (L : C ⥤ D) [category_theory.is_left_adjoint L] :

category_theory.comonad (category_theory.right_adjoint L ⋙ L)

Equations

category_theory.adjunction.comonad L = {ε := (category_theory.adjunction.of_left_adjoint L).counit, δ := category_theory.whisker_right (category_theory.whisker_left (category_theory.right_adjoint L) (category_theory.adjunction.of_left_adjoint L).unit) L, coassoc' := _, left_counit' := _, right_counit' := _}

source

@[simp]

theorem category_theory.adjunction.comonad_δ {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (L : C ⥤ D) [category_theory.is_left_adjoint L] :

δ_ (category_theory.right_adjoint L ⋙ L) = category_theory.whisker_right (category_theory.whisker_left (category_theory.right_adjoint L) (category_theory.adjunction.of_left_adjoint L).unit) L

source

@[simp]

theorem category_theory.adjunction.comonad_ε {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (L : C ⥤ D) [category_theory.is_left_adjoint L] :

ε_ (category_theory.right_adjoint L ⋙ L) = (category_theory.adjunction.of_left_adjoint L).counit

source

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

D ⥤ category_theory.monad.algebra (category_theory.left_adjoint R ⋙ 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

category_theory.monad.comparison R = {obj := λ (X : D), {A := R.obj X, a := R.map ((category_theory.adjunction.of_right_adjoint R).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] (R : D ⥤ C) [category_theory.is_right_adjoint R] (X : D) :

((category_theory.monad.comparison R).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] (R : D ⥤ C) [category_theory.is_right_adjoint R] (X : D) :

((category_theory.monad.comparison R).obj X).a = R.map ((category_theory.adjunction.of_right_adjoint R).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] (R : D ⥤ C) [category_theory.is_right_adjoint R] (X Y : D) (f : X ⟶ Y) :

((category_theory.monad.comparison R).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] (R : D ⥤ C) [category_theory.is_right_adjoint R] (X : D) :

(category_theory.monad.comparison_forget R).hom.app X = 𝟙 ((category_theory.monad.comparison R ⋙ category_theory.monad.forget (category_theory.left_adjoint R ⋙ R)).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] (R : D ⥤ C) [category_theory.is_right_adjoint R] (X : D) :

(category_theory.monad.comparison_forget R).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] (R : D ⥤ C) [category_theory.is_right_adjoint R] :

category_theory.monad.comparison R ⋙ category_theory.monad.forget (category_theory.left_adjoint R ⋙ R) ≅ R

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

Equations

category_theory.monad.comparison_forget R = {hom := {app := λ (X : D), 𝟙 ((category_theory.monad.comparison R ⋙ category_theory.monad.forget (category_theory.left_adjoint R ⋙ R)).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) [category_theory.is_left_adjoint L] (X : C) :

((category_theory.comonad.comparison L).obj X).a = L.map ((category_theory.adjunction.of_left_adjoint L).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) [category_theory.is_left_adjoint L] (X Y : C) (f : X ⟶ Y) :

((category_theory.comonad.comparison L).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) [category_theory.is_left_adjoint L] :

C ⥤ category_theory.comonad.coalgebra (category_theory.right_adjoint L ⋙ L)

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 L = {obj := λ (X : C), {A := L.obj X, a := L.map ((category_theory.adjunction.of_left_adjoint L).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) [category_theory.is_left_adjoint L] (X : C) :

((category_theory.comonad.comparison L).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) [category_theory.is_left_adjoint L] (X : C) :

(category_theory.comonad.comparison_forget L).hom.app X = 𝟙 ((category_theory.comonad.comparison L ⋙ category_theory.comonad.forget (category_theory.right_adjoint L ⋙ L)).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) [category_theory.is_left_adjoint L] :

category_theory.comonad.comparison L ⋙ category_theory.comonad.forget (category_theory.right_adjoint L ⋙ L) ≅ L

The underlying object of (comonad.comparison L).obj X is just L.obj X.

Equations

category_theory.comonad.comparison_forget L = {hom := {app := λ (X : C), 𝟙 ((category_theory.comonad.comparison L ⋙ category_theory.comonad.forget (category_theory.right_adjoint L ⋙ L)).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) [category_theory.is_left_adjoint L] (X : C) :

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

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 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 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.left_adjoint R ⋙ R))

Equations

category_theory.μ_iso_of_reflective R = id (category_theory.is_iso_whisker_right (category_theory.whisker_left (category_theory.left_adjoint R) (category_theory.adjunction.of_right_adjoint R).counit) R)

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.monad.algebra (category_theory.left_adjoint R ⋙ R)) :

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

Equations

category_theory.reflective.app.category_theory.is_iso R X = {inv := X.a, hom_inv_id' := _, inv_hom_id' := _}

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

Equations

category_theory.reflective.comparison_full R = {preimage := λ (X Y : D) (f : (category_theory.monad.comparison R).obj X ⟶ (category_theory.monad.comparison 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 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][riehl2017]

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