Characters of a descended group algebra

For a finite Galois extension L/k and an integral representation rho on an abelian group M, let B be the invariant algebra of L[M] under the simultaneous action on coefficients and exponents. The characters over L of the affine group with coordinate algebra B recover M, including its prescribed Galois action.

The characters are realized as the group-like elements of L ⊗[k] B. The canonical splitting sends each such element to a unique monomial X^m; the resulting equivalence intertwines the scalar-factor action with rho. In particular this comparison applies to the character lattices of tori obtained by Galois descent, without needing finite generation or torsion-freeness for the comparison itself.

The construction composes GroupLike.mapEquiv for the Hopf splitting with MonoidAlgebra.groupLikeEquiv for the split group algebra.

References

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

noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv {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) : GroupLike L (TensorProduct k L ↥(groupAlgebraInvariants rho)) ≃* Multiplicative M

The characters over the splitting field of the descended group recover its exponent group. The character indexed by m is the inverse image of X^m under the Hopf splitting.

Equations

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

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv_apply_eq_iff {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 : GroupLike L (TensorProduct k L ↥(groupAlgebraInvariants rho))) (m : Multiplicative M) : (groupAlgebraInvariantsCharacterEquiv rho) x = m ↔ (groupAlgebraInvariantsBaseChangeBialgEquiv rho) ↑x = MonoidAlgebra.single m 1

A character corresponds to m precisely when the splitting sends it to X^m.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv_symm_apply_val {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) (m : Multiplicative M) : ↑((groupAlgebraInvariantsCharacterEquiv rho).symm m) = (groupAlgebraInvariantsBaseChangeBialgEquiv rho).symm (MonoidAlgebra.single m 1)

The value of the character indexed by m is the inverse splitting of its monomial.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv_smul {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) (sigma : Gal(L/k)) (x : GroupLike L (TensorProduct k L ↥(groupAlgebraInvariants rho))) : (groupAlgebraInvariantsCharacterEquiv rho) (sigma • x) = Multiplicative.ofAdd ((rho sigma) (Multiplicative.toAdd ((groupAlgebraInvariantsCharacterEquiv rho) x)))

Recovering an exponent from a character intertwines the scalar-factor Galois action with the original action on exponents.

@[simp]

theorem TauCeti.GaloisDescent.smul_groupAlgebraInvariantsCharacterEquiv_symm_apply {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) (sigma : Gal(L/k)) (m : Multiplicative M) : sigma • (groupAlgebraInvariantsCharacterEquiv rho).symm m = (groupAlgebraInvariantsCharacterEquiv rho).symm (Multiplicative.ofAdd ((rho sigma) (Multiplicative.toAdd m)))

Galois conjugation of the character indexed by m gives the character indexed by rho sigma m.