The Hopf algebra of Galois-invariant group-algebra elements

For a finite Galois extension L/k, the invariant algebra of the simultaneous action on coefficients and exponents of L[M] is a Hopf algebra over k. Its comultiplication is obtained from the tensor descent equivalence, its counit takes values in k, and its antipode is the restriction of the split antipode. These are the coordinate Hopf algebras used to construct groups of multiplicative type, and non-split tori when M is a lattice.

No finite generation of M or restriction on the characteristic is needed.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.23 and Appendix A.64.

@[instance_reducible]

noncomputable instance TauCeti.GaloisDescent.groupAlgebraInvariantsBialgebra {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) : Bialgebra k ↥(groupAlgebraInvariants rho)

The invariant group algebra is a bialgebra over the ground field.

Equations

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

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsTensorEquiv_comul {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) (x : ↥(groupAlgebraInvariants rho)) : (groupAlgebraInvariantsTensorEquiv rho) (CoalgebraStruct.comul x) = (groupAlgebraInvariantsComul rho) x

Under tensor descent, the comultiplication is the original invariant-valued map.

@[simp]

theorem TauCeti.GaloisDescent.counit_groupAlgebraInvariants {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) (x : ↥(groupAlgebraInvariants rho)) : CoalgebraStruct.counit x = (groupAlgebraInvariantsCounit rho) x

The counit on the invariant Hopf algebra is the descended counit.

@[instance_reducible]

noncomputable instance TauCeti.GaloisDescent.groupAlgebraInvariantsHopfAlgebra {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) : HopfAlgebra k ↥(groupAlgebraInvariants rho)

The coordinate Hopf algebra descended from the split group algebra along L/k.

Equations

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

@[simp]

theorem TauCeti.GaloisDescent.antipode_groupAlgebraInvariants {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) (x : ↥(groupAlgebraInvariants rho)) : (HopfAlgebraStruct.antipode k) x = (groupAlgebraInvariantsAntipode rho) x

The antipode on the descended Hopf algebra is the restricted split antipode.