Commit 2025-02-17 16:56 f3066cd9

View on Github →

feat: Hopf algebra structure on monoid algebras (#13609) Given a commutative semiring R, an R-bialgebra (resp. R-Hopf algebra) A, and a(n) (additive) monoid (resp. (additive) group) G, this PR defines the R-bialgebra (resp. R-Hopf algebra) structure on (Add)MonoidAlgebra A G.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Bialgebra/Basic.lean

Created Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

added theorem LaurentPolynomial.comul_T

added theorem LaurentPolynomial.counit_T

Modified Mathlib/RingTheory/Coalgebra/Basic.lean

Created Mathlib/RingTheory/Coalgebra/MonoidAlgebra.lean

added theorem AddMonoidAlgebra.comul_single

added theorem AddMonoidAlgebra.counit_single

added theorem LaurentPolynomial.comul_C

added theorem LaurentPolynomial.comul_C_mul_T

added theorem LaurentPolynomial.comul_C_mul_T_self

added theorem LaurentPolynomial.counit_C

added theorem LaurentPolynomial.counit_C_mul_T

added theorem MonoidAlgebra.comul_single

added theorem MonoidAlgebra.counit_single

Modified Mathlib/RingTheory/HopfAlgebra/Basic.lean

added theorem HopfAlgebra.antipode_one

Created Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean

added theorem AddMonoidAlgebra.antipode_single

added theorem LaurentPolynomial.antipode_C

added theorem LaurentPolynomial.antipode_C_mul_T

added theorem LaurentPolynomial.antipode_T

added theorem MonoidAlgebra.antipode_single