# Algebras for the coproduct monad #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 category_theory.prod_comonad_δ_app {C : Type u} (X : C) (Y : C) :
@[simp]
noncomputable def category_theory.prod_comonad {C : Type u} (X : C)  :

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

Equations
@[simp]
theorem category_theory.prod_comonad_ε_app {C : Type u} (X : C) (Y : C) :
@[simp]
noncomputable def category_theory.coalgebra_to_over {C : Type u} (X : C)  :

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

Equations
@[simp]
theorem category_theory.coalgebra_to_over_map {C : Type u} (X : C) (A₁ A₂ : .coalgebra) (f : A₁ A₂) :
@[simp]
theorem category_theory.over_to_coalgebra_map_f {C : Type u} (X : C) (f₁ f₂ : category_theory.over X) (g : f₁ f₂) :
.f = g.left
@[simp]
@[simp]
noncomputable def category_theory.over_to_coalgebra {C : Type u} (X : C)  :

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

Equations
@[simp]
@[simp]
noncomputable def category_theory.coalgebra_equiv_over {C : Type u} (X : C)  :

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

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.coprod_monad_μ_app {C : Type u} (X : C) (Y : C) :
noncomputable def category_theory.coprod_monad {C : Type u} (X : C)  :

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

Equations
@[simp]
theorem category_theory.coprod_monad_η_app {C : Type u} (X : C) (Y : C) :
@[simp]
noncomputable def category_theory.algebra_to_under {C : Type u} (X : C)  :

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

Equations
@[simp]
@[simp]
theorem category_theory.algebra_to_under_map {C : Type u} (X : C) (A₁ A₂ : .algebra) (f : A₁ A₂) :
noncomputable def category_theory.under_to_algebra {C : Type u} (X : C)  :

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

Equations
@[simp]
theorem category_theory.under_to_algebra_map_f {C : Type u} (X : C) (f₁ f₂ : category_theory.under X) (g : f₁ f₂) :
.f = g.right
@[simp]
@[simp]
noncomputable def category_theory.algebra_equiv_under {C : Type u} (X : C)  :

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

Equations
@[simp]
@[simp]
@[simp]
@[simp]