Base change of the solvable radical

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

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

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

The four candidate conditions use their corresponding base-change theorems. The quotient by a base-changed ideal is identified with the base change of the original quotient by CommHopfAlgCat.quotientBaseChangeIso; finite-type Nullstellensatz makes the universal derived-word defect nilpotent, so that condition also survives arbitrary field extension.

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

Main declarations

• TauCeti.HopfIdeal.IsSolvableRadicalCandidate.baseChange: scalar extension preserves solvable-radical candidates.
• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal_baseChange_le: the base-changed solvable radical is contained in the radical after base change.
• TauCeti.FiniteTypeCommHopfAlgCat. solvableRadicalDefiningIdeal_eq_augmentation_of_baseChange_eq_augmentation: triviality of the solvable 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.
• TauCeti.Algebra.AlgebraicGroup.Unipotent.Radical.BaseChange: proves the analogous descent of radical triviality for the unipotent radical.

This advances the scalar-extension compatibility of the radical in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

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

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

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

The solvable radical after base change contains the base change of the original solvable 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.solvableRadicalDefiningIdeal_eq_augmentation_of_baseChange_eq_augmentation {k K : Type u} [Field k] [Field K] [Algebra k K] {H : FiniteTypeCommHopfAlgCat k} (hgeometric : H.baseChange.solvableRadicalDefiningIdeal = HopfIdeal.augmentation K ↑H.baseChange.obj) : H.solvableRadicalDefiningIdeal = HopfIdeal.augmentation k ↑H.obj

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