Sweedler representation of a product #
In a bialgebra, comul (x * y) = comul x * comul y, so Sweedler
representations of x and y multiply to one of x * y. [UPSTREAM]
candidate for Mathlib.RingTheory.Bialgebra.Basic, beside
Bialgebra.comul_mul.
noncomputable def
Coalgebra.Repr.mul
{R : Type u_1}
[CommSemiring R]
{H : Type u_2}
[Semiring H]
[Bialgebra R H]
{x y : H}
{ιx : Type u_3}
{ιy : Type u_4}
(𝓡x : Repr R x ιx)
(𝓡y : Repr R y ιy)
:
Repr R (x * y) (ιx × ιy)
Sweedler representation of a product x * y in a bialgebra, indexed by
pairs: left (i, j) = left i * left j and right (i, j) = right i * right j.
Equations
- 𝓡x.mul 𝓡y = { index := 𝓡x.index ×ˢ 𝓡y.index, left := fun (p : ιx × ιy) => 𝓡x.left p.1 * 𝓡y.left p.2, right := fun (p : ιx × ιy) => 𝓡x.right p.1 * 𝓡y.right p.2, eq := ⋯ }