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.

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

• MonoidAlgebra.instHopfAlgebraStruct R A G = HopfAlgebraStruct.mk ((Finsupp.lsum R) fun (g : G) => Finsupp.lsingle g⁻¹ ∘ₗ HopfAlgebraStruct.antipode)

@[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 (single g a) = single g⁻¹ (HopfAlgebraStruct.antipode a)

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 = HopfAlgebra.mk ⋯ ⋯

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

• AddMonoidAlgebra.instHopfAlgebraStruct R A G = HopfAlgebraStruct.mk ((Finsupp.lsum R) fun (g : G) => Finsupp.lsingle (-g) ∘ₗ HopfAlgebraStruct.antipode)

@[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 (single g a) = single (-g) (HopfAlgebraStruct.antipode a)

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 = HopfAlgebra.mk ⋯ ⋯

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 = inferInstanceAs (HopfAlgebra R (AddMonoidAlgebra A ℤ))

@[simp]

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

@[simp]

theorem LaurentPolynomial.antipode_T {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (n : ℤ) : HopfAlgebraStruct.antipode (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 (C a * T n) = C (HopfAlgebraStruct.antipode a) * T (-n)