The bialgebra structure on monoid algebras

Given a monoid M, a commutative semiring R and an R-bialgebra A, this file collects results about the R-bialgebra instance on A[M] 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[M] when M 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.

@[implicit_reducible]

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

@[implicit_reducible]

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

noncomputable def AddMonoidAlgebra.mapDomainBialgHom (R : Type u_1) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddMonoid M] [AddMonoid N] (f : M →+ N) : AddMonoidAlgebra R M →ₐc[R] AddMonoidAlgebra R N

If f : M → N is a monoid hom, then AddMonoidAlgebra.mapDomain f is a bialgebra hom between their additive monoid algebras.

noncomputable def MonoidAlgebra.mapDomainBialgHom (R : Type u_1) {M : Type u_3} {N : Type u_4} [CommSemiring R] [Monoid M] [Monoid N] (f : M →* N) : MonoidAlgebra R M →ₐc[R] MonoidAlgebra R N

If f : M → N is a monoid hom, then MonoidAlgebra.mapDomain f is a bialgebra hom between their monoid algebras.

@[simp]

theorem AddMonoidAlgebra.mapDomainBialgHom_apply (R : Type u_1) {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddMonoid M] [AddMonoid N] (f : M →+ N) (a✝ : AddMonoidAlgebra R M) : (mapDomainBialgHom R f) a✝ = mapDomain (⇑f) a✝

@[simp]

theorem MonoidAlgebra.mapDomainBialgHom_apply (R : Type u_1) {M : Type u_3} {N : Type u_4} [CommSemiring R] [Monoid M] [Monoid N] (f : M →* N) (a✝ : MonoidAlgebra R M) : (mapDomainBialgHom R f) a✝ = mapDomain (⇑f) a✝

@[simp]

theorem MonoidAlgebra.mapDomainBialgHom_id {R : Type u_1} {M : Type u_3} [CommSemiring R] [Monoid M] : mapDomainBialgHom R (MonoidHom.id M) = BialgHom.id R (MonoidAlgebra R M)

@[simp]

theorem AddMonoidAlgebra.mapDomainBialgHom_id {R : Type u_1} {M : Type u_3} [CommSemiring R] [AddMonoid M] : mapDomainBialgHom R (AddMonoidHom.id M) = BialgHom.id R (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.mapDomainBialgHom_comp {R : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [CommSemiring R] [Monoid M] [Monoid N] [Monoid O] (f : N →* O) (g : M →* N) : mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g)

@[simp]

theorem AddMonoidAlgebra.mapDomainBialgHom_comp {R : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [CommSemiring R] [AddMonoid M] [AddMonoid N] [AddMonoid O] (f : N →+ O) (g : M →+ N) : mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g)

theorem MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom {R : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [CommSemiring R] [Monoid M] [Monoid N] [Monoid O] (f : N →* O) (g : M →* N) (x : MonoidAlgebra R M) : (mapDomainBialgHom R f) ((mapDomainBialgHom R g) x) = (mapDomainBialgHom R (f.comp g)) x

theorem AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom {R : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [CommSemiring R] [AddMonoid M] [AddMonoid N] [AddMonoid O] (f : N →+ O) (g : M →+ N) (x : AddMonoidAlgebra R M) : (mapDomainBialgHom R f) ((mapDomainBialgHom R g) x) = (mapDomainBialgHom R (f.comp g)) x

@[implicit_reducible]

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

@[simp]

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

@[simp]

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