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.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.prodComonad_map {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (prodComonad X).map g = Limits.prod.map (CategoryStruct.id X) g

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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