# 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) :
@[simp]
theorem CategoryTheory.prodComonad_δ_app {C : Type u} (X : C) (Y : C) :
.app Y = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst ()
@[simp]
theorem CategoryTheory.prodComonad_ε_app {C : Type u} (X : C) (Y : C) :
.app Y = CategoryTheory.Limits.prod.snd
@[simp]
theorem CategoryTheory.prodComonad_obj {C : Type u} (X : C) (Y : C) :
.obj Y = (X Y)
def CategoryTheory.prodComonad {C : Type u} (X : C) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.coalgebraToOver_map {C : Type u} (X : C) :
∀ {X_1 Y : .Coalgebra} (f : X_1 Y), .map f =
@[simp]
theorem CategoryTheory.coalgebraToOver_obj {C : Type u} (X : C) (A : .Coalgebra) :
.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.

Equations
• One or more equations did not get rendered due to their size.
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_1 Y : } (g : X_1 Y), (.map g).f = g.left

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
def CategoryTheory.coalgebraEquivOver {C : Type u} (X : C) :
.Coalgebra

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.coprodMonad_obj {C : Type u} (X : C) (Y : C) :
.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) :
def CategoryTheory.coprodMonad {C : Type u} (X : C) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.algebraToUnder_obj {C : Type u} (X : C) (A : .Algebra) :
.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_1 Y : .Algebra} (f : X_1 Y), .map f =
def CategoryTheory.algebraToUnder {C : Type u} (X : C) :

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

Equations
• One or more equations did not get rendered due to their size.
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_1 Y : } (g : X_1 Y), (.map g).f = g.right
def CategoryTheory.underToAlgebra {C : Type u} (X : C) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
def CategoryTheory.algebraEquivUnder {C : Type u} (X : C) :
.Algebra

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

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