Adjunctions and (co)monads

We develop the basic relationship between adjunctions and (co)monads.

Given an adjunction h : L ⊣ R, we have h.toMonad : Monad C and h.toComonad : Comonad D. We then have Monad.comparison (h : L ⊣ R) : D ⥤ h.toMonad.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 MonadicRightAdjoint, if it is a right adjoint and its Monad.comparison is an equivalence of categories. (Similarly for ComonadicLeftAdjoint.)

Finally we prove that reflective functors are MonadicRightAdjoint and coreflective functors are ComonadicLeftAdjoint.

def CategoryTheory.Adjunction.toMonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.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.toMonad = { toFunctor := L.comp R, η := h.unit, μ := CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft L h.counit) R, assoc := ⋯, left_unit := ⋯, right_unit := ⋯ }

@[simp]

theorem CategoryTheory.Adjunction.toMonad_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : h.toMonad.toFunctor = L.comp R

@[simp]

theorem CategoryTheory.Adjunction.toMonad_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : h.toMonad.μ = CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft L h.counit) R

@[simp]

theorem CategoryTheory.Adjunction.toMonad_η {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : h.toMonad.η = h.unit

def CategoryTheory.Adjunction.toComonad {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.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.toComonad = { toFunctor := R.comp L, ε := h.counit, δ := CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft R h.unit) L, coassoc := ⋯, left_counit := ⋯, right_counit := ⋯ }

@[simp]

theorem CategoryTheory.Adjunction.toComonad_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : h.toComonad.toFunctor = R.comp L

@[simp]

theorem CategoryTheory.Adjunction.toComonad_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : h.toComonad.ε = h.counit

@[simp]

theorem CategoryTheory.Adjunction.toComonad_δ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : h.toComonad.δ = CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft R h.unit) L

def CategoryTheory.Adjunction.adjToMonadIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.adj.toMonad ≅ T

The monad induced by the Eilenberg-Moore adjunction is the original monad.

Equations

• CategoryTheory.Adjunction.adjToMonadIso T = CategoryTheory.MonadIso.mk (CategoryTheory.NatIso.ofComponents (fun (x : C) => CategoryTheory.Iso.refl (T.adj.toMonad.obj x)) ⋯) ⋯ ⋯

@[simp]

theorem CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : (CategoryTheory.Adjunction.adjToMonadIso T).inv.app X = CategoryTheory.CategoryStruct.id (T.obj X)

@[simp]

theorem CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : (CategoryTheory.Adjunction.adjToMonadIso T).hom.app X = CategoryTheory.CategoryStruct.id (T.obj X)

def CategoryTheory.Adjunction.adjToComonadIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.adj.toComonad ≅ G

The comonad induced by the Eilenberg-Moore adjunction is the original comonad.

Equations

• CategoryTheory.Adjunction.adjToComonadIso G = CategoryTheory.ComonadIso.mk (CategoryTheory.NatIso.ofComponents (fun (x : C) => CategoryTheory.Iso.refl (G.adj.toComonad.obj x)) ⋯) ⋯ ⋯

@[simp]

theorem CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) : (CategoryTheory.Adjunction.adjToComonadIso G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj X)

@[simp]

theorem CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) : (CategoryTheory.Adjunction.adjToComonadIso G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)

def CategoryTheory.Adjunction.unitAsIsoOfIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) (i : L.comp R ≅ CategoryTheory.Functor.id C) : CategoryTheory.Functor.id C ≅ L.comp R

Given an adjunction L ⊣ R, if L ⋙ R is abstractly isomorphic to the identity functor, then the unit is an isomorphism.

Equations

• adj.unitAsIsoOfIso i = { hom := adj.unit, inv := CategoryTheory.CategoryStruct.comp i.hom (adj.toMonad.transport i).μ, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem CategoryTheory.Adjunction.isIso_unit_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) (i : L.comp R ≅ CategoryTheory.Functor.id C) : CategoryTheory.IsIso adj.unit

noncomputable def CategoryTheory.Adjunction.fullyFaithfulLOfCompIsoId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) (i : L.comp R ≅ CategoryTheory.Functor.id C) : L.FullyFaithful

Given an adjunction L ⊣ R, if L ⋙ R is isomorphic to the identity functor, then L is fully faithful.

Equations

• adj.fullyFaithfulLOfCompIsoId i = adj.fullyFaithfulLOfIsIsoUnit

def CategoryTheory.Adjunction.counitAsIsoOfIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) (j : R.comp L ≅ CategoryTheory.Functor.id D) : R.comp L ≅ CategoryTheory.Functor.id D

Given an adjunction L ⊣ R, if R ⋙ L is abstractly isomorphic to the identity functor, then the counit is an isomorphism.

Equations

• adj.counitAsIsoOfIso j = { hom := adj.counit, inv := CategoryTheory.CategoryStruct.comp (adj.toComonad.transport j).δ j.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem CategoryTheory.Adjunction.isIso_counit_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) (j : R.comp L ≅ CategoryTheory.Functor.id D) : CategoryTheory.IsIso adj.counit

noncomputable def CategoryTheory.Adjunction.fullyFaithfulROfCompIsoId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) (j : R.comp L ≅ CategoryTheory.Functor.id D) : R.FullyFaithful

Given an adjunction L ⊣ R, if R ⋙ L is isomorphic to the identity functor, then R is fully faithful.

Equations

• adj.fullyFaithfulROfCompIsoId j = adj.fullyFaithfulROfIsIsoCounit

def CategoryTheory.Monad.comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor D h.toMonad.Algebra

Given any adjunction L ⊣ R, there is a comparison functor CategoryTheory.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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Monad.comparison_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D) : ((CategoryTheory.Monad.comparison h).obj X).a = R.map (h.counit.app X)

@[simp]

theorem CategoryTheory.Monad.comparison_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D) : ((CategoryTheory.Monad.comparison h).obj X).A = R.obj X

@[simp]

theorem CategoryTheory.Monad.comparison_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Monad.comparison h).map f).f = R.map f

def CategoryTheory.Monad.comparisonForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : (CategoryTheory.Monad.comparison h).comp h.toMonad.forget ≅ R

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Monad.comparisonForget_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x✝ : D) : (CategoryTheory.Monad.comparisonForget h).hom.app x✝ = CategoryTheory.CategoryStruct.id (((CategoryTheory.Monad.comparison h).comp h.toMonad.forget).obj x✝)

@[simp]

theorem CategoryTheory.Monad.comparisonForget_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x✝ : D) : (CategoryTheory.Monad.comparisonForget h).inv.app x✝ = CategoryTheory.CategoryStruct.id (R.obj x✝)

theorem CategoryTheory.Monad.left_comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : L.comp (CategoryTheory.Monad.comparison h) = h.toMonad.free

instance CategoryTheory.instFaithfulAlgebraToMonadComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} [R.Faithful] (h : L ⊣ R) : (CategoryTheory.Monad.comparison h).Faithful

Equations

• ⋯ = ⋯

instance CategoryTheory.instFullAlgebraToMonadAdjComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : (CategoryTheory.Monad.comparison T.adj).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instEssSurjAlgebraToMonadAdjComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : (CategoryTheory.Monad.comparison T.adj).EssSurj

Equations

• ⋯ = ⋯

def CategoryTheory.Comonad.comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor C h.toComonad.Coalgebra

Given any adjunction L ⊣ R, there is a comparison functor CategoryTheory.Comonad.comparison L sending objects X : C to Eilenberg-Moore coalgebras for L ⋙ R with underlying object L.obj X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Comonad.comparison_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : C) : ((CategoryTheory.Comonad.comparison h).obj X).A = L.obj X

@[simp]

theorem CategoryTheory.Comonad.comparison_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : C) : ((CategoryTheory.Comonad.comparison h).obj X).a = L.map (h.unit.app X)

@[simp]

theorem CategoryTheory.Comonad.comparison_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comonad.comparison h).map f).f = L.map f

def CategoryTheory.Comonad.comparisonForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : (CategoryTheory.Comonad.comparison h).comp h.toComonad.forget ≅ L

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Comonad.comparisonForget_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x✝ : C) : (CategoryTheory.Comonad.comparisonForget h).inv.app x✝ = CategoryTheory.CategoryStruct.id (L.obj x✝)

@[simp]

theorem CategoryTheory.Comonad.comparisonForget_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x✝ : C) : (CategoryTheory.Comonad.comparisonForget h).hom.app x✝ = CategoryTheory.CategoryStruct.id (((CategoryTheory.Comonad.comparison h).comp h.toComonad.forget).obj x✝)

theorem CategoryTheory.Comonad.left_comparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : R.comp (CategoryTheory.Comonad.comparison h) = h.toComonad.cofree

instance CategoryTheory.Comonad.comparison_faithful_of_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} [L.Faithful] (h : L ⊣ R) : (CategoryTheory.Comonad.comparison h).Faithful

Equations

• ⋯ = ⋯

instance CategoryTheory.instFullCoalgebraToComonadAdjComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : (CategoryTheory.Comonad.comparison G.adj).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : (CategoryTheory.Comonad.comparison G.adj).EssSurj

Equations

• ⋯ = ⋯

class CategoryTheory.MonadicRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) : Type (max (max (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.

• L : CategoryTheory.Functor C D

  a choice of left adjoint for R

• adj : CategoryTheory.MonadicRightAdjoint.L R ⊣ R

  R is a right adjoint

• eqv : (CategoryTheory.Monad.comparison CategoryTheory.MonadicRightAdjoint.adj).IsEquivalence

def CategoryTheory.monadicLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] : CategoryTheory.Functor C D

The left adjoint functor to R given by [MonadicRightAdjoint R].

Equations

• CategoryTheory.monadicLeftAdjoint R = CategoryTheory.MonadicRightAdjoint.L R

def CategoryTheory.monadicAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] : CategoryTheory.monadicLeftAdjoint R ⊣ R

The adjunction monadicLeftAdjoint R ⊣ R given by [MonadicRightAdjoint R].

Equations

• CategoryTheory.monadicAdjunction R = CategoryTheory.MonadicRightAdjoint.adj

instance CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] : (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R)).IsEquivalence

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] : R.IsRightAdjoint

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.instMonadicRightAdjointAlgebraForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.MonadicRightAdjoint T.forget

Equations

• CategoryTheory.instMonadicRightAdjointAlgebraForget T = { L := T.free, adj := T.adj, eqv := ⋯ }

class CategoryTheory.ComonadicLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) : Type (max (max (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.

• R : CategoryTheory.Functor D C

  a choice of right adjoint for L

• adj : L ⊣ CategoryTheory.ComonadicLeftAdjoint.R L

  L is a left adjoint

• eqv : (CategoryTheory.Comonad.comparison CategoryTheory.ComonadicLeftAdjoint.adj).IsEquivalence

def CategoryTheory.comonadicRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [CategoryTheory.ComonadicLeftAdjoint L] : CategoryTheory.Functor D C

The right adjoint functor to L given by [ComonadicLeftAdjoint L].

Equations

• CategoryTheory.comonadicRightAdjoint L = CategoryTheory.ComonadicLeftAdjoint.R L

def CategoryTheory.comonadicAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [CategoryTheory.ComonadicLeftAdjoint L] : L ⊣ CategoryTheory.comonadicRightAdjoint L

The adjunction L ⊣ comonadicRightAdjoint L given by [ComonadicLeftAdjoint L].

Equations

• CategoryTheory.comonadicAdjunction L = CategoryTheory.ComonadicLeftAdjoint.adj

instance CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [CategoryTheory.ComonadicLeftAdjoint L] : (CategoryTheory.Comonad.comparison (CategoryTheory.comonadicAdjunction L)).IsEquivalence

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsLeftAdjointOfComonadicLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [CategoryTheory.ComonadicLeftAdjoint L] : L.IsLeftAdjoint

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.instComonadicLeftAdjointCoalgebraForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.ComonadicLeftAdjoint G.forget

Equations

• CategoryTheory.instComonadicLeftAdjointCoalgebraForget G = { R := G.cofree, adj := G.adj, eqv := ⋯ }

instance CategoryTheory.μ_iso_of_reflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] : CategoryTheory.IsIso (CategoryTheory.reflectorAdjunction R).toMonad.μ

Equations

• ⋯ = ⋯

instance CategoryTheory.δ_iso_of_coreflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Coreflective R] : CategoryTheory.IsIso (CategoryTheory.coreflectorAdjunction R).toComonad.δ

Equations

• ⋯ = ⋯

instance CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] (X : (CategoryTheory.reflectorAdjunction R).toMonad.Algebra) : CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction R).unit.app X.A)

Equations

• ⋯ = ⋯

instance CategoryTheory.Reflective.comparison_essSurj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] : (CategoryTheory.Monad.comparison (CategoryTheory.reflectorAdjunction R)).EssSurj

Equations

• ⋯ = ⋯

theorem CategoryTheory.Reflective.comparison_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [R.Full] {L : CategoryTheory.Functor C D} (adj : L ⊣ R) : (CategoryTheory.Monad.comparison adj).Full

instance CategoryTheory.Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Coreflective R] (X : (CategoryTheory.coreflectorAdjunction R).toComonad.Coalgebra) : CategoryTheory.IsIso ((CategoryTheory.coreflectorAdjunction R).counit.app X.A)

Equations

• ⋯ = ⋯

instance CategoryTheory.Coreflective.comparison_essSurj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Coreflective R] : (CategoryTheory.Comonad.comparison (CategoryTheory.coreflectorAdjunction R)).EssSurj

Equations

• ⋯ = ⋯

theorem CategoryTheory.Coreflective.comparison_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [R.Full] {L : CategoryTheory.Functor C D} (adj : R ⊣ L) : (CategoryTheory.Comonad.comparison adj).Full

@[instance 100]

instance CategoryTheory.monadicOfReflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] : CategoryTheory.MonadicRightAdjoint R

Any reflective inclusion has a monadic right adjoint. cf Prop 5.3.3 of Riehl

Equations

• CategoryTheory.monadicOfReflective = { L := CategoryTheory.reflector R, adj := CategoryTheory.reflectorAdjunction R, eqv := ⋯ }

@[instance 100]

instance CategoryTheory.comonadicOfCoreflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Coreflective R] : CategoryTheory.ComonadicLeftAdjoint R

Any coreflective inclusion has a comonadic left adjoint. cf Dual statement of Prop 5.3.3 of Riehl

Equations

• CategoryTheory.comonadicOfCoreflective = { R := CategoryTheory.coreflector R, adj := CategoryTheory.coreflectorAdjunction R, eqv := ⋯ }