The radical is contained in every Borel subgroup

Let H be the coordinate Hopf algebra of a finite-type affine group over a field. A Borel candidate is a smooth, geometrically connected, geometrically solvable closed subgroup. A maximal Borel candidate is a Borel subgroup over an algebraically closed field; over an arbitrary field, a Borel subgroup is one whose base change to an algebraic closure is such a subgroup. This file proves that every normal Borel candidate is contained in every maximal one; in particular the solvable radical R(G), and hence the unipotent radical R_u(G), lies inside every Borel subgroup.

The argument is the standard one and reuses the product machinery that built the two radicals. Let B be a Borel candidate and let N be a geometrically connected normal smooth geometrically solvable closed subgroup. Since N is normal, multiplication is a homomorphism from the conjugation semidirect product of N and B into the ambient group, and its scheme-theoretic image N · B contains both factors. That image is again smooth, geometrically connected and geometrically solvable, so it is a Borel candidate containing B. Maximality of B forces N · B = B, so N is contained in B. Normality of N is what makes N · B a subgroup at all; no hypothesis is needed on B beyond being a Borel candidate, and nothing here needs the ground field to be algebraically closed.

Contravariance is the only thing to keep in mind when reading the statements: Hopf ideals order oppositely to the closed subgroups they cut out, so J ≤ I says that the subgroup defined by I sits inside the subgroup defined by J.

Two consequences are recorded. If the radical is the whole group — that is, if the group is itself smooth, geometrically connected and geometrically solvable — then its unique maximal Borel candidate is the whole group, and the same conclusion holds for every Borel subgroup over the ground field. Conversely, a smooth geometrically connected group with a trivial geometric Borel subgroup is semisimple, since its geometric solvable radical is squeezed between the trivial Borel and the identity subgroup.

Main declarations

• TauCeti.HopfIdeal.IsBorelCandidate.productOfNormal: the multiplication image of a geometrically connected normal smooth geometrically solvable closed subgroup with a Borel candidate is a Borel candidate.
• TauCeti.HopfIdeal.IsBorelCandidate.isSolvableRadicalCandidate_of_isNormal: a normal Borel candidate is a solvable-radical candidate.
• TauCeti.HopfIdeal.IsSolvableRadicalCandidate.le_of_minimal_isBorelCandidate: every geometrically connected normal smooth geometrically solvable closed subgroup is contained in every maximal Borel candidate.
• TauCeti.FiniteTypeCommHopfAlgCat.le_solvableRadicalDefiningIdeal_of_minimal_isBorelCandidate: the solvable radical is contained in every maximal Borel candidate.
• TauCeti.FiniteTypeCommHopfAlgCat.le_unipotentRadicalDefiningIdeal_of_minimal_isBorelCandidate: the unipotent radical is contained in every maximal Borel candidate.
• TauCeti.HopfIdeal.IsBorelOverAlgClosed.le_solvableRadicalDefiningIdeal and TauCeti.HopfIdeal.IsBorelOverAlgClosed.le_unipotentRadicalDefiningIdeal: the same two containments for the Borel-subgroup predicate over an algebraically closed field.
• TauCeti.HopfIdeal.IsBorel.baseChangeHopfIdeal_le_solvableRadicalDefiningIdeal and TauCeti.HopfIdeal.IsBorel.baseChangeHopfIdeal_le_unipotentRadicalDefiningIdeal: over an arbitrary field, the base change of a Borel subgroup contains the two geometric radicals.
• TauCeti.HopfIdeal.IsBorel.le_solvableRadicalDefiningIdeal and TauCeti.HopfIdeal.IsBorel.le_unipotentRadicalDefiningIdeal: over an arbitrary field, the solvable radical, and hence the unipotent radical, is contained in every Borel subgroup.
• TauCeti.HopfIdeal.IsBorel.eq_solvableRadicalDefiningIdeal_of_isNormal: a normal Borel subgroup over an arbitrary field is exactly the solvable radical.
• TauCeti.HopfIdeal.IsBorel.eq_bot_of_solvableRadicalDefiningIdeal_eq_bot: if the solvable radical is the whole group, every Borel subgroup over the ground field is the whole group.
• TauCeti.semisimpleCommHopfAlgProperty_of_isBorelOverAlgClosed_eq_augmentation: a smooth geometrically connected affine group with a trivial geometric Borel subgroup is semisimple.

References

• J. S. Milne, Algebraic Groups (2017), §§17.a and 19.b.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §11.21.
• T. A. Springer, Linear Algebraic Groups, §6.2.

The product-image bookkeeping follows the formal organization of TauCeti.Algebra.AlgebraicGroup.Solvable.Radical.Product, where the same three closure properties are proved for two normal factors.

theorem TauCeti.HopfIdeal.IsBorelCandidate.productOfNormal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I J : HopfIdeal k ↑H.obj} (hJ : IsBorelCandidate k H J) (hI : IsSolvableRadicalCandidate H I) : IsBorelCandidate k H (ker (CommHopfAlgCat.Hom.hom (CommHopfAlgCat.productMapOfNormal H.obj I J ⋯)))

The scheme-theoretic multiplication image of a geometrically connected normal smooth geometrically solvable closed subgroup with a Borel candidate is again a Borel candidate.

Normality of the solvable factor is what makes multiplication a homomorphism out of the conjugation semidirect product; the other factor is an arbitrary Borel candidate.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.le_of_minimal_isBorelCandidate {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I J : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) (hJ : Minimal (IsBorelCandidate k H) J) : J ≤ I

Every geometrically connected normal smooth geometrically solvable closed subgroup is contained in every maximal Borel candidate.

In the contravariant Hopf-ideal order, J ≤ I says that the subgroup cut out by I is contained in the maximal Borel candidate cut out by J.

theorem TauCeti.HopfIdeal.IsBorelCandidate.isSolvableRadicalCandidate_of_isNormal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {J : HopfIdeal k ↑H.obj} (hJ : IsBorelCandidate k H J) (hnormal : J.IsNormal) : IsSolvableRadicalCandidate H J

A normal Borel candidate is a solvable-radical candidate: normality is the only condition separating the two notions.

theorem TauCeti.FiniteTypeCommHopfAlgCat.le_solvableRadicalDefiningIdeal_of_minimal_isBorelCandidate {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) {J : HopfIdeal k ↑H.obj} (hJ : Minimal (HopfIdeal.IsBorelCandidate k H) J) : J ≤ H.solvableRadicalDefiningIdeal

The solvable radical is contained in every maximal Borel candidate.

theorem TauCeti.FiniteTypeCommHopfAlgCat.le_unipotentRadicalDefiningIdeal_of_minimal_isBorelCandidate {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) {J : HopfIdeal k ↑H.obj} (hJ : Minimal (HopfIdeal.IsBorelCandidate k H) J) : J ≤ H.unipotentRadicalDefiningIdeal

The unipotent radical is contained in every maximal Borel candidate, since it is contained in the solvable radical.

theorem TauCeti.FiniteTypeCommHopfAlgCat.eq_solvableRadicalDefiningIdeal_of_isNormal_of_minimal_isBorelCandidate {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) {J : HopfIdeal k ↑H.obj} (hnormal : J.IsNormal) (hJ : Minimal (HopfIdeal.IsBorelCandidate k H) J) : J = H.solvableRadicalDefiningIdeal

A normal maximal Borel candidate is exactly the solvable radical.

One containment is maximality of the Borel candidate, the other is the universal property of the radical applied to the candidate, which is a solvable-radical candidate once it is normal.

theorem TauCeti.FiniteTypeCommHopfAlgCat.eq_bot_of_solvableRadicalDefiningIdeal_eq_bot_of_minimal_isBorelCandidate {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) {J : HopfIdeal k ↑H.obj} (hH : H.solvableRadicalDefiningIdeal = ⊥) (hJ : Minimal (HopfIdeal.IsBorelCandidate k H) J) : J = ⊥

A smooth geometrically connected and geometrically solvable affine group is its own unique maximal Borel candidate.

The hypothesis says that the solvable radical is the whole group, the closed subgroup cut out by the zero Hopf ideal.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.le_solvableRadicalDefiningIdeal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelOverAlgClosed k H I) : I ≤ H.solvableRadicalDefiningIdeal

Over an algebraically closed field, the solvable radical is contained in every Borel subgroup.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.le_unipotentRadicalDefiningIdeal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelOverAlgClosed k H I) : I ≤ H.unipotentRadicalDefiningIdeal

Over an algebraically closed field, the unipotent radical is contained in every Borel subgroup.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.eq_solvableRadicalDefiningIdeal_of_isNormal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelOverAlgClosed k H I) (hnormal : I.IsNormal) : I = H.solvableRadicalDefiningIdeal

Over an algebraically closed field, a normal Borel subgroup is exactly the solvable radical.

theorem TauCeti.HopfIdeal.IsBorelOverAlgClosed.eq_bot_of_solvableRadicalDefiningIdeal_eq_bot {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsBorelOverAlgClosed k H I) (hH : H.solvableRadicalDefiningIdeal = ⊥) : I = ⊥

Over an algebraically closed field, if the solvable radical is the whole group, every Borel subgroup is the whole group.

theorem TauCeti.HopfIdeal.IsBorel.baseChangeHopfIdeal_le_solvableRadicalDefiningIdeal {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorel k H I) : CommHopfAlgCat.baseChangeHopfIdeal I ≤ (FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }).solvableRadicalDefiningIdeal

Over an arbitrary field, the base change of a Borel subgroup contains the geometric solvable radical.

theorem TauCeti.HopfIdeal.IsBorel.baseChangeHopfIdeal_le_unipotentRadicalDefiningIdeal {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorel k H I) : CommHopfAlgCat.baseChangeHopfIdeal I ≤ (FiniteTypeCommHopfAlgCat.baseChange { obj := H, property := ⋯ }).unipotentRadicalDefiningIdeal

Over an arbitrary field, the base change of a Borel subgroup contains the geometric unipotent radical.

theorem TauCeti.HopfIdeal.IsBorel.le_solvableRadicalDefiningIdeal {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorel k H I) : I ≤ FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal { obj := H, property := ⋯ }

Over an arbitrary field, the solvable radical is contained in every Borel subgroup.

The containment is checked after base change to an algebraic closure, where it is the geometric statement, and descends because the base change of a Hopf ideal is faithfully flat.

theorem TauCeti.HopfIdeal.IsBorel.le_unipotentRadicalDefiningIdeal {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorel k H I) : I ≤ FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal { obj := H, property := ⋯ }

Over an arbitrary field, the unipotent radical is contained in every Borel subgroup, since it is contained in the solvable radical.

theorem TauCeti.HopfIdeal.IsBorel.eq_solvableRadicalDefiningIdeal_of_isNormal {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorel k H I) (hnormal : I.IsNormal) : I = FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal { obj := H, property := ⋯ }

Over an arbitrary field, a normal Borel subgroup is exactly the solvable radical.

theorem TauCeti.HopfIdeal.IsBorel.eq_bot_of_solvableRadicalDefiningIdeal_eq_bot {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {I : HopfIdeal k ↑H} (hI : IsBorel k H I) (hH : FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal { obj := H, property := ⋯ } = ⊥) : I = ⊥

Over an arbitrary field, if the solvable radical is the whole group, every Borel subgroup is the whole group.

theorem TauCeti.semisimpleCommHopfAlgProperty_of_isBorelOverAlgClosed_eq_augmentation {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (hsmooth : Algebra.Smooth k ↑H.obj) (hconnected : geometricallyConnectedCommHopfAlgProperty k H.obj) {J : HopfIdeal (AlgebraicClosure k) ↑H.baseChange.obj} (hJ : HopfIdeal.IsBorelOverAlgClosed (AlgebraicClosure k) H.baseChange J) (hJtrivial : J = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj) : semisimpleCommHopfAlgProperty k H

A smooth geometrically connected affine group with a trivial geometric Borel subgroup is semisimple.

The Borel subgroup is taken on the geometric fibre, and triviality means that its defining Hopf ideal is the augmentation ideal. The geometric solvable radical is then contained in the identity subgroup, hence equal to it.