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}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(Y : C) :
@[simp]
theorem
category_theory.prod_comonad_coe
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C] :
noncomputable
def
category_theory.prod_comonad
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C] :
X ⨯ - has a comonad structure. This is sometimes called the writer comonad.
Equations
- category_theory.prod_comonad X = {to_functor := category_theory.limits.prod.functor.obj X, ε' := {app := λ (Y : C), category_theory.limits.prod.snd, naturality' := _}, δ' := {app := λ (Y : C), category_theory.limits.prod.lift category_theory.limits.prod.fst (𝟙 ((category_theory.limits.prod.functor.obj X).obj Y)), naturality' := _}, coassoc' := _, left_counit' := _, right_counit' := _}
@[simp]
theorem
category_theory.prod_comonad_ε_app
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(Y : C) :
@[simp]
theorem
category_theory.coalgebra_to_over_obj
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(A : (category_theory.prod_comonad X).coalgebra) :
noncomputable
def
category_theory.coalgebra_to_over
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C] :
The forward direction of the equivalence from coalgebras for the product comonad to the over category.
Equations
- category_theory.coalgebra_to_over X = {obj := λ (A : (category_theory.prod_comonad X).coalgebra), category_theory.over.mk (A.a ≫ category_theory.limits.prod.fst), map := λ (A₁ A₂ : (category_theory.prod_comonad X).coalgebra) (f : A₁ ⟶ A₂), category_theory.over.hom_mk f.f _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.coalgebra_to_over_map
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(A₁ A₂ : (category_theory.prod_comonad X).coalgebra)
(f : A₁ ⟶ A₂) :
@[simp]
theorem
category_theory.over_to_coalgebra_map_f
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(f₁ f₂ : category_theory.over X)
(g : f₁ ⟶ f₂) :
((category_theory.over_to_coalgebra X).map g).f = g.left
@[simp]
theorem
category_theory.over_to_coalgebra_obj_a
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(f : category_theory.over X) :
((category_theory.over_to_coalgebra X).obj f).a = category_theory.limits.prod.lift f.hom (𝟙 f.left)
@[simp]
theorem
category_theory.over_to_coalgebra_obj_A
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C]
(f : category_theory.over X) :
((category_theory.over_to_coalgebra X).obj f).A = f.left
noncomputable
def
category_theory.over_to_coalgebra
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C] :
The backward direction of the equivalence from coalgebras for the product comonad to the over category.
@[simp]
theorem
category_theory.coalgebra_equiv_over_unit_iso
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C] :
@[simp]
noncomputable
def
category_theory.coalgebra_equiv_over
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C] :
The equivalence from coalgebras for the product comonad to the over category.
Equations
- category_theory.coalgebra_equiv_over X = {functor := category_theory.coalgebra_to_over X _inst_2, inverse := category_theory.over_to_coalgebra X _inst_2, unit_iso := category_theory.nat_iso.of_components (λ (A : (category_theory.prod_comonad X).coalgebra), category_theory.comonad.coalgebra.iso_mk (category_theory.iso.refl ((𝟭 (category_theory.prod_comonad X).coalgebra).obj A).A) _) _, counit_iso := category_theory.nat_iso.of_components (λ (f : category_theory.over X), category_theory.over.iso_mk (category_theory.iso.refl ((category_theory.over_to_coalgebra X ⋙ category_theory.coalgebra_to_over X).obj f).left) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.coalgebra_equiv_over_counit_iso
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_products C] :
@[simp]
@[simp]
theorem
category_theory.coprod_monad_μ_app
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C]
(Y : C) :
noncomputable
def
category_theory.coprod_monad
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C] :
X ⨿ - has a monad structure. This is sometimes called the either monad.
Equations
- category_theory.coprod_monad X = {to_functor := category_theory.limits.coprod.functor.obj X, η' := {app := λ (Y : C), category_theory.limits.coprod.inr, naturality' := _}, μ' := {app := λ (Y : C), category_theory.limits.coprod.desc category_theory.limits.coprod.inl (𝟙 ((category_theory.limits.coprod.functor.obj X).obj Y)), naturality' := _}, assoc' := _, left_unit' := _, right_unit' := _}
@[simp]
theorem
category_theory.coprod_monad_η_app
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C]
(Y : C) :
@[simp]
theorem
category_theory.coprod_monad_coe
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C] :
noncomputable
def
category_theory.algebra_to_under
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C] :
The forward direction of the equivalence from algebras for the coproduct monad to the under category.
Equations
- category_theory.algebra_to_under X = {obj := λ (A : (category_theory.coprod_monad X).algebra), category_theory.under.mk (category_theory.limits.coprod.inl ≫ A.a), map := λ (A₁ A₂ : (category_theory.coprod_monad X).algebra) (f : A₁ ⟶ A₂), category_theory.under.hom_mk f.f _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.algebra_to_under_obj
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C]
(A : (category_theory.coprod_monad X).algebra) :
@[simp]
theorem
category_theory.algebra_to_under_map
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C]
(A₁ A₂ : (category_theory.coprod_monad X).algebra)
(f : A₁ ⟶ A₂) :
noncomputable
def
category_theory.under_to_algebra
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts 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}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C]
(f₁ f₂ : category_theory.under X)
(g : f₁ ⟶ f₂) :
((category_theory.under_to_algebra X).map g).f = g.right
@[simp]
theorem
category_theory.under_to_algebra_obj_a
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C]
(f : category_theory.under X) :
((category_theory.under_to_algebra X).obj f).a = category_theory.limits.coprod.desc f.hom (𝟙 f.right)
@[simp]
theorem
category_theory.under_to_algebra_obj_A
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C]
(f : category_theory.under X) :
((category_theory.under_to_algebra X).obj f).A = f.right
noncomputable
def
category_theory.algebra_equiv_under
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C] :
The equivalence from algebras for the coproduct monad to the under category.
Equations
- category_theory.algebra_equiv_under X = {functor := category_theory.algebra_to_under X _inst_2, inverse := category_theory.under_to_algebra X _inst_2, unit_iso := category_theory.nat_iso.of_components (λ (A : (category_theory.coprod_monad X).algebra), category_theory.monad.algebra.iso_mk (category_theory.iso.refl ((𝟭 (category_theory.coprod_monad X).algebra).obj A).A) _) _, counit_iso := category_theory.nat_iso.of_components (λ (f : category_theory.under X), category_theory.under.iso_mk (category_theory.iso.refl ((category_theory.under_to_algebra X ⋙ category_theory.algebra_to_under X).obj f).right) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.algebra_equiv_under_unit_iso
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C] :
@[simp]
@[simp]
@[simp]
theorem
category_theory.algebra_equiv_under_counit_iso
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproducts C] :