Tori over algebraically closed fields

Every torus over an algebraically closed field is split. This identifies the geometric torus predicate with its split counterpart, so results proved for split tori apply to all tori over such a field. In particular, it removes the splitting assumption from conjugacy of maximal tori in general linear groups.

References

• J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17.

theorem TauCeti.torusCommHopfAlgProperty.split (k : Type u) [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) : splitTorusCommHopfAlgProperty k H

Every torus over an algebraically closed field is split.

theorem TauCeti.torusCommHopfAlgProperty_iff_split (k : Type u) [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : torusCommHopfAlgProperty k H ↔ splitTorusCommHopfAlgProperty k H

Over an algebraically closed field, the torus and split-torus predicates coincide.