Base change of the unipotent radical

Let H be a finite-type commutative Hopf algebra over a field k. Extension to a field K sends every connected normal smooth unipotent closed subgroup of the affine group represented by H to another such subgroup. In particular, the base change of the unipotent radical is contained in the unipotent radical formed after base change.

In coordinate rings, closed-subgroup containment reverses the order on defining ideals, so the conclusion is

  unipotentRadicalDefiningIdeal (K ⊗[k] H) ≤
    baseChangeHopfIdeal (unipotentRadicalDefiningIdeal H).

Normality and geometric connectedness survive base change directly. The quotient by a base-changed ideal is identified with the base change of the original quotient, where smooth geometric unipotence follows from the universal coefficient-matrix argument.

Triviality of the radical after a field extension descends to the ground field by faithful-flat reflection of equality of Hopf ideals.

Equality requires descent of an arbitrary radical candidate over K and is not asserted here.

Main declarations

• TauCeti.HopfIdeal.IsUnipotentRadicalCandidate.baseChange: scalar extension preserves unipotent-radical candidates.
• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_baseChange_le: the base-changed unipotent radical is contained in the radical after base change.
• TauCeti.FiniteTypeCommHopfAlgCat. unipotentRadicalDefiningIdeal_eq_augmentation_of_baseChange_eq_augmentation: triviality of the unipotent radical after a field extension descends to the ground field.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and Sections 6.45--6.46.
• A. Borel, Linear Algebraic Groups, Section 11.21.

This advances scalar-extension compatibility for the unipotent radical in Layer 5 of the ReductiveGroups roadmap.

theorem TauCeti.HopfIdeal.IsUnipotentRadicalCandidate.baseChange {k K : Type u} [Field k] [Field K] [Algebra k K] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsUnipotentRadicalCandidate H I) : IsUnipotentRadicalCandidate H.baseChange (CommHopfAlgCat.baseChangeHopfIdeal I)

Base change of a unipotent-radical candidate is again a unipotent-radical candidate.

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_baseChange_le {k K : Type u} [Field k] [Field K] [Algebra k K] (H : FiniteTypeCommHopfAlgCat k) : H.baseChange.unipotentRadicalDefiningIdeal ≤ CommHopfAlgCat.baseChangeHopfIdeal H.unipotentRadicalDefiningIdeal

The unipotent radical after base change contains the base change of the original unipotent radical.

The displayed inequality is between defining Hopf ideals, hence has the opposite direction from the corresponding inclusion of represented closed subgroups.

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_eq_augmentation_of_baseChange_eq_augmentation {k K : Type u} [Field k] [Field K] [Algebra k K] {H : FiniteTypeCommHopfAlgCat k} (hgeometric : H.baseChange.unipotentRadicalDefiningIdeal = HopfIdeal.augmentation K ↑H.baseChange.obj) : H.unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑H.obj

Triviality of the unipotent radical after base change to a field extension descends to the ground field.