The bialgebra structure on monoid algebras

Given a monoid X, a commutative semiring R and an R-bialgebra A, this file collects results about the R-bialgebra instance on A[X] inherited from the corresponding structure on its coefficients, building upon results in Mathlib/RingTheory/Coalgebra/MonoidAlgebra.lean about the coalgebra structure.

Main definitions

• (Add)MonoidAlgebra.instBialgebra: the R-bialgebra structure on A[X] when X is an (add) monoid and A is an R-bialgebra.
• LaurentPolynomial.instBialgebra: the R-bialgebra structure on the Laurent polynomials A[T;T⁻¹] when A is an R-bialgebra.

noncomputable instance MonoidAlgebra.instBialgebra (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] (X : Type u_3) [Bialgebra R A] [Monoid X] : Bialgebra R (MonoidAlgebra A X)

Equations

• MonoidAlgebra.instBialgebra R A X = Bialgebra.mk ⋯ ⋯ ⋯ ⋯

noncomputable instance AddMonoidAlgebra.instBialgebra (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] (X : Type u_3) [Bialgebra R A] [AddMonoid X] : Bialgebra R (AddMonoidAlgebra A X)

Equations

• AddMonoidAlgebra.instBialgebra R A X = Bialgebra.mk ⋯ ⋯ ⋯ ⋯

noncomputable instance LaurentPolynomial.instBialgebra {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Bialgebra R A] : Bialgebra R (LaurentPolynomial A)

Equations

• LaurentPolynomial.instBialgebra = inferInstanceAs (Bialgebra R (AddMonoidAlgebra A ℤ))

@[simp]

theorem LaurentPolynomial.comul_T {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Bialgebra R A] (n : ℤ) : CoalgebraStruct.comul (T n) = T n ⊗ₜ[R] T n

@[simp]

theorem LaurentPolynomial.counit_T {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Bialgebra R A] (n : ℤ) : CoalgebraStruct.counit (T n) = 1