When the solvable radical is the whole group

Let H be the coordinate Hopf algebra of a finite-type affine group over a field. The solvable radical of H is the whole represented group exactly when H itself is geometrically connected, smooth, and has a solvable group of geometric points. In Hopf coordinates, the whole closed subgroup is cut out by the zero Hopf ideal, so this criterion says that solvableRadicalDefiningIdeal H = ⊥.

Applying the criterion to the solvable radical itself shows that the construction is idempotent: the solvable radical of R(H) is all of R(H).

Main declarations

• TauCeti.HopfIdeal.isSolvableRadicalCandidate_bot_iff: the whole group is a solvable-radical candidate exactly under the expected three conditions.
• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal_eq_bot_iff: the solvable radical is the whole group exactly when the ambient group is connected, smooth, and solvable.
• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal_solvableRadical_eq_bot: taking the solvable radical twice does not shrink it further.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and Sections 6.45--6.46.
• A. Borel, Linear Algebraic Groups, Section 11.21.
• Formal template: TauCeti.Algebra.AlgebraicGroup.Unipotent.Radical.Characteristic.

This supplies the characteristic and idempotence API for the solvable-radical construction in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

@[simp]

theorem TauCeti.HopfIdeal.isSolvableRadicalCandidate_bot_iff {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : IsSolvableRadicalCandidate H ⊥ ↔ geometricallyConnectedCommHopfAlgProperty k H.obj ∧ Algebra.Smooth k ↑H.obj ∧ geometricallySolvablePointsCommHopfAlgProperty k H.obj

The zero Hopf ideal is a solvable-radical candidate exactly when the whole represented group is geometrically connected, smooth, and has a solvable group of geometric points.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal_eq_bot_iff {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.solvableRadicalDefiningIdeal = ⊥ ↔ geometricallyConnectedCommHopfAlgProperty k H.obj ∧ Algebra.Smooth k ↑H.obj ∧ geometricallySolvablePointsCommHopfAlgProperty k H.obj

The solvable radical is the whole represented group exactly when the ambient finite-type affine group is geometrically connected, smooth, and has a solvable group of geometric points.

The equality is stated on defining Hopf ideals: the zero ideal cuts out the whole group.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal_solvableRadical_eq_bot {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.solvableRadical.solvableRadicalDefiningIdeal = ⊥

The solvable radical of the solvable radical is the whole solvable radical. Equivalently, the solvable-radical construction is idempotent on defining ideals.