The Hopf algebra structure on group algebras

Given a group G, a commutative semiring R and an R-Hopf algebra A, this file collects results about the R-Hopf algebra instance on A[G], building upon results in Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean about the bialgebra structure.

Main definitions

• (Add)MonoidAlgebra.instHopfAlgebra: the R-Hopf algebra structure on A[G] when G is an (add) group and A is an R-Hopf algebra.
• LaurentPolynomial.instHopfAlgebra: the R-Hopf algebra structure on the Laurent polynomials A[T;T⁻¹] when A is an R-Hopf algebra. When A = R this corresponds to the fact that 𝔾ₘ/R is a group scheme.

@[instance_reducible]

noncomputable instance MonoidAlgebra.instHopfAlgebraStruct (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [HopfAlgebra R A] (G : Type u_3) [Group G] : HopfAlgebraStruct R (MonoidAlgebra A G)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance AddMonoidAlgebra.instHopfAlgebraStruct (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [HopfAlgebra R A] (G : Type u_3) [AddGroup G] : HopfAlgebraStruct R (AddMonoidAlgebra A G)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MonoidAlgebra.antipode_single {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {G : Type u_3} [Group G] (g : G) (a : A) : (HopfAlgebraStruct.antipode R) (single g a) = single g⁻¹ ((HopfAlgebraStruct.antipode R) a)

@[simp]

theorem AddMonoidAlgebra.antipode_single {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {G : Type u_3} [AddGroup G] (g : G) (a : A) : (HopfAlgebraStruct.antipode R) (single g a) = single (-g) ((HopfAlgebraStruct.antipode R) a)

@[instance_reducible]

noncomputable instance MonoidAlgebra.instHopfAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {G : Type u_3} [Group G] : HopfAlgebra R (MonoidAlgebra A G)

Equations

• MonoidAlgebra.instHopfAlgebra = { toHopfAlgebraStruct := MonoidAlgebra.instHopfAlgebraStruct R A G, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }

@[instance_reducible]

noncomputable instance AddMonoidAlgebra.instHopfAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {G : Type u_3} [AddGroup G] : HopfAlgebra R (AddMonoidAlgebra A G)

Equations

• AddMonoidAlgebra.instHopfAlgebra = { toHopfAlgebraStruct := AddMonoidAlgebra.instHopfAlgebraStruct R A G, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }

@[instance_reducible]

noncomputable instance LaurentPolynomial.instHopfAlgebra (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [HopfAlgebra R A] : HopfAlgebra R (LaurentPolynomial A)

Equations

• LaurentPolynomial.instHopfAlgebra R A = { toHopfAlgebraStruct := AddMonoidAlgebra.instHopfAlgebraStruct R A ℤ, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }

@[simp]

theorem LaurentPolynomial.antipode_C {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : A) : (HopfAlgebraStruct.antipode R) (C a) = C ((HopfAlgebraStruct.antipode R) a)

@[simp]

theorem LaurentPolynomial.antipode_T {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (n : ℤ) : (HopfAlgebraStruct.antipode R) (T n) = T (-n)

@[simp]

theorem LaurentPolynomial.antipode_C_mul_T {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : A) (n : ℤ) : (HopfAlgebraStruct.antipode R) (C a * T n) = C ((HopfAlgebraStruct.antipode R) a) * T (-n)