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} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {Y : C} {Z : C} (g : Y ⟶ Z) : (CategoryTheory.prodComonad X).toFunctor.map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g

@[simp]

theorem CategoryTheory.prodComonad_δ_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (Y : C) : (CategoryTheory.Comonad.δ (CategoryTheory.prodComonad X)).app Y = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ Y))

@[simp]

theorem CategoryTheory.prodComonad_ε_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (Y : C) : (CategoryTheory.Comonad.ε (CategoryTheory.prodComonad X)).app Y = CategoryTheory.Limits.prod.snd

@[simp]

theorem CategoryTheory.prodComonad_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (Y : C) : (CategoryTheory.prodComonad X).toFunctor.obj Y = (X ⨯ Y)

def CategoryTheory.prodComonad {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Comonad C

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

@[simp]

theorem CategoryTheory.coalgebraToOver_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : ∀ {X Y : CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X)} (f : X ⟶ Y), (CategoryTheory.coalgebraToOver X).map f = CategoryTheory.Over.homMk f.f

@[simp]

theorem CategoryTheory.coalgebraToOver_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (A : CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X)) : (CategoryTheory.coalgebraToOver X).obj A = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)

def CategoryTheory.coalgebraToOver {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor (CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X)) (CategoryTheory.Over X)

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

@[simp]

theorem CategoryTheory.overToCoalgebra_obj_A {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (f : CategoryTheory.Over X) : ((CategoryTheory.overToCoalgebra X).obj f).A = f.left

@[simp]

theorem CategoryTheory.overToCoalgebra_obj_a {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (f : CategoryTheory.Over X) : ((CategoryTheory.overToCoalgebra X).obj f).a = CategoryTheory.Limits.prod.lift f.hom (CategoryTheory.CategoryStruct.id f.left)

@[simp]

theorem CategoryTheory.overToCoalgebra_map_f {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : ∀ {X Y : CategoryTheory.Over X} (g : X ⟶ Y), ((CategoryTheory.overToCoalgebra X).map g).f = g.left

def CategoryTheory.overToCoalgebra {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X))

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

@[simp]

theorem CategoryTheory.coalgebraEquivOver_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).functor = CategoryTheory.coalgebraToOver X

@[simp]

theorem CategoryTheory.coalgebraEquivOver_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).counitIso = CategoryTheory.NatIso.ofComponents fun f => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.overToCoalgebra X) (CategoryTheory.coalgebraToOver X)).obj f).left)

@[simp]

theorem CategoryTheory.coalgebraEquivOver_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).unitIso = CategoryTheory.NatIso.ofComponents fun A => CategoryTheory.Comonad.Coalgebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X))).obj A).A)

@[simp]

theorem CategoryTheory.coalgebraEquivOver_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).inverse = CategoryTheory.overToCoalgebra X

def CategoryTheory.coalgebraEquivOver {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Comonad.Coalgebra (CategoryTheory.prodComonad X) ≌ CategoryTheory.Over X

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

@[simp]

theorem CategoryTheory.coprodMonad_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (Y : C) : (CategoryTheory.coprodMonad X).toFunctor.obj Y = (X ⨿ Y)

@[simp]

theorem CategoryTheory.coprodMonad_μ_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (Y : C) : (CategoryTheory.Monad.μ (CategoryTheory.coprodMonad X)).app Y = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ Y))

@[simp]

theorem CategoryTheory.coprodMonad_η_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (Y : C) : (CategoryTheory.Monad.η (CategoryTheory.coprodMonad X)).app Y = CategoryTheory.Limits.coprod.inr

@[simp]

theorem CategoryTheory.coprodMonad_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {Y : C} {Z : C} (g : Y ⟶ Z) : (CategoryTheory.coprodMonad X).toFunctor.map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g

def CategoryTheory.coprodMonad {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Monad C

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

@[simp]

theorem CategoryTheory.algebraToUnder_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (A : CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X)) : (CategoryTheory.algebraToUnder X).obj A = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)

@[simp]

theorem CategoryTheory.algebraToUnder_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : ∀ {X Y : CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X)} (f : X ⟶ Y), (CategoryTheory.algebraToUnder X).map f = CategoryTheory.Under.homMk f.f

def CategoryTheory.algebraToUnder {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor (CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X)) (CategoryTheory.Under X)

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

@[simp]

theorem CategoryTheory.underToAlgebra_obj_A {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) : ((CategoryTheory.underToAlgebra X).obj f).A = f.right

@[simp]

theorem CategoryTheory.underToAlgebra_obj_a {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) : ((CategoryTheory.underToAlgebra X).obj f).a = CategoryTheory.Limits.coprod.desc f.hom (CategoryTheory.CategoryStruct.id f.right)

@[simp]

theorem CategoryTheory.underToAlgebra_map_f {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : ∀ {X Y : CategoryTheory.Under X} (g : X ⟶ Y), ((CategoryTheory.underToAlgebra X).map g).f = g.right

def CategoryTheory.underToAlgebra {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X))

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

@[simp]

theorem CategoryTheory.algebraEquivUnder_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).counitIso = CategoryTheory.NatIso.ofComponents fun f => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.underToAlgebra X) (CategoryTheory.algebraToUnder X)).obj f).right)

@[simp]

theorem CategoryTheory.algebraEquivUnder_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).inverse = CategoryTheory.underToAlgebra X

@[simp]

theorem CategoryTheory.algebraEquivUnder_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).functor = CategoryTheory.algebraToUnder X

@[simp]

theorem CategoryTheory.algebraEquivUnder_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).unitIso = CategoryTheory.NatIso.ofComponents fun A => CategoryTheory.Monad.Algebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X))).obj A).A)

def CategoryTheory.algebraEquivUnder {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Monad.Algebra (CategoryTheory.coprodMonad X) ≌ CategoryTheory.Under X

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