Finiteness of descended group algebras

Let L/k be a finite Galois extension and let a finitely generated abelian group M carry an integral representation of Gal(L/k). The simultaneous semilinear action on L[Multiplicative M] has an invariant k-subalgebra. This file proves that the split group algebra is finite as a module over that invariant algebra and, by the Artin--Tate lemma, that the invariant algebra is finite type over k.

Finite type is necessary before the invariant algebra can serve as the coordinate algebra of the torus descended from the split torus D(M). The remaining Galois-descent step is to identify its scalar extension to L with L[Multiplicative M] and transport the Hopf structure through that identification.

Main declarations

• TauCeti.GaloisDescent.isIntegral_groupAlgebra_over_groupAlgebraInvariants: the split group algebra is integral over its invariant algebra.
• TauCeti.GaloisDescent.moduleFinite_groupAlgebra_over_groupAlgebraInvariants: for a finitely generated exponent group, the split group algebra is module-finite over its invariant algebra.
• TauCeti.GaloisDescent.instFiniteTypeGroupAlgebraInvariants: the invariant algebra is finite type over the ground field.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.23 and Appendix A.64.
• M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Proposition 7.8 (Artin--Tate).

This advances Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap. It supplies the finite-type part of the inverse Galois-descent construction from an integral Galois lattice.

theorem TauCeti.GaloisDescent.isIntegral_groupAlgebra_over_groupAlgebraInvariants {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [Finite Gal(L/k)] (rho : Representation ℤ Gal(L/k) M) : Algebra.IsIntegral (↥(groupAlgebraInvariants rho)) (MonoidAlgebra L (Multiplicative M))

The split group algebra is integral over the invariant algebra when its automorphism group is finite.

theorem TauCeti.GaloisDescent.moduleFinite_groupAlgebra_over_groupAlgebraInvariants {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [Algebra.FiniteType k L] [Finite Gal(L/k)] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) : Module.Finite (↥(groupAlgebraInvariants rho)) (MonoidAlgebra L (Multiplicative M))

If L/k is finite type with finite automorphism group and the exponent group is finitely generated, the split group algebra is finite as a module over its invariant algebra.

instance TauCeti.GaloisDescent.instFiniteTypeGroupAlgebraInvariants {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [Algebra.FiniteType k L] [Finite Gal(L/k)] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) : Algebra.FiniteType k ↥(groupAlgebraInvariants rho)

For a finite-type extension with finite automorphism group, the invariant algebra of the automorphism action on the group algebra of a finitely generated abelian group is finite type over the ground field.