# Algebras for the coproduct monad #

The functor Y ↦ X ⨿ Y forms a monad, whose category of monads is equivalent to the under category of X. Similarly, Y ↦ X ⨯ Y forms a comonad, whose category of comonads is equivalent to the over category of X.

## TODO #

Show that Over.forget X : Over X ⥤ C is a comonadic left adjoint and Under.forget : Under X ⥤ C is a monadic right adjoint.

@[simp]
theorem CategoryTheory.prodComonad_map {C : Type u} (X : C) {Y : C} {Z : C} (g : Y Z) :
().toFunctor.map g =
@[simp]
theorem CategoryTheory.prodComonad_δ_app {C : Type u} (X : C) (Y : C) :
= CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst ()
@[simp]
theorem CategoryTheory.prodComonad_ε_app {C : Type u} (X : C) (Y : C) :
= CategoryTheory.Limits.prod.snd
@[simp]
theorem CategoryTheory.prodComonad_obj {C : Type u} (X : C) (Y : C) :
().toFunctor.obj Y = (X Y)
def CategoryTheory.prodComonad {C : Type u} (X : C) :

X ⨯ - has a comonad structure. This is sometimes called the writer comonad.

Instances For
@[simp]
theorem CategoryTheory.coalgebraToOver_map {C : Type u} (X : C) :
∀ {X Y : } (f : X Y), ().map f =
@[simp]
theorem CategoryTheory.coalgebraToOver_obj {C : Type u} (X : C) :
().obj A = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)

The forward direction of the equivalence from coalgebras for the product comonad to the over category.

Instances For
@[simp]
theorem CategoryTheory.overToCoalgebra_obj_A {C : Type u} (X : C) (f : ) :
(().obj f).A = f.left
@[simp]
theorem CategoryTheory.overToCoalgebra_obj_a {C : Type u} (X : C) (f : ) :
(().obj f).a =
@[simp]
theorem CategoryTheory.overToCoalgebra_map_f {C : Type u} (X : C) :
∀ {X Y : } (g : X Y), (().map g).f = g.left

The backward direction of the equivalence from coalgebras for the product comonad to the over category.

Instances For
@[simp]
@[simp]

The equivalence from coalgebras for the product comonad to the over category.

Instances For
@[simp]
theorem CategoryTheory.coprodMonad_obj {C : Type u} (X : C) (Y : C) :
().toFunctor.obj Y = (X ⨿ Y)
@[simp]
theorem CategoryTheory.coprodMonad_μ_app {C : Type u} (X : C) (Y : C) :
().app Y = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl ()
@[simp]
theorem CategoryTheory.coprodMonad_η_app {C : Type u} (X : C) (Y : C) :
().app Y = CategoryTheory.Limits.coprod.inr
@[simp]
theorem CategoryTheory.coprodMonad_map {C : Type u} (X : C) {Y : C} {Z : C} (g : Y Z) :
().toFunctor.map g =
def CategoryTheory.coprodMonad {C : Type u} (X : C) :

X ⨿ - has a monad structure. This is sometimes called the either monad.

Instances For
@[simp]
theorem CategoryTheory.algebraToUnder_obj {C : Type u} (X : C) :
().obj A = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)
@[simp]
theorem CategoryTheory.algebraToUnder_map {C : Type u} (X : C) :
∀ {X Y : } (f : X Y), ().map f =

The forward direction of the equivalence from algebras for the coproduct monad to the under category.

Instances For
@[simp]
theorem CategoryTheory.underToAlgebra_obj_A {C : Type u} (X : C) (f : ) :
(().obj f).A = f.right
@[simp]
theorem CategoryTheory.underToAlgebra_obj_a {C : Type u} (X : C) (f : ) :
(().obj f).a =
@[simp]
theorem CategoryTheory.underToAlgebra_map_f {C : Type u} (X : C) :
∀ {X Y : } (g : X Y), (().map g).f = g.right

The backward direction of the equivalence from algebras for the coproduct monad to the under category.

Instances For
@[simp]
@[simp]
@[simp]

The equivalence from algebras for the coproduct monad to the under category.

Instances For