Recognising a torus from a splitting field

A torus is defined by becoming a finite-rank split torus over an algebraic closure of the base field. In practice a torus is produced together with a splitting field that is much smaller: a finite Galois extension over which the coordinate Hopf algebra becomes a group algebra. This file converts such data into the definition.

Concretely, if L / k is algebraic and L ⊗[k] H is a split torus, then H is a torus over k.

Main declaration

• TauCeti.torusCommHopfAlgProperty.of_baseChange: a finite-type commutative Hopf algebra that becomes a split torus over an algebraic extension is a torus.
• TauCeti.torusCommHopfAlgProperty.of_baseChange_iso_coordinateRing: the corresponding coordinate-ring criterion.

References

• J. S. Milne, Algebraic Groups (2017), Definition 12.17 and Theorem 12.23.

theorem TauCeti.torusCommHopfAlgProperty.of_baseChange (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsAlgebraic k L] (H : FiniteTypeCommHopfAlgCat k) (hH : splitTorusCommHopfAlgProperty L H.baseChange) : torusCommHopfAlgProperty k H

A finite-type commutative Hopf algebra that becomes a split torus over an algebraic extension is a torus.

theorem TauCeti.torusCommHopfAlgProperty.of_baseChange_iso_coordinateRing (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsAlgebraic k L] (H : FiniteTypeCommHopfAlgCat k) (G : FGCommGrpCat) [IsMulTorsionFree ↑G] (i : H.baseChange ≅ DiagonalizableGroup.coordinateRing L G) : torusCommHopfAlgProperty k H

A finite-type commutative Hopf algebra that becomes a torsion-free diagonalizable coordinate ring over an algebraic extension is a torus.

Torsion freeness of the character group G distinguishes tori among the groups of multiplicative type; finite generation then supplies the split-torus property.