The solvable radical of an affine group

Let H be the coordinate Hopf algebra of a finite-type affine group over a field. A connected normal smooth solvable closed subgroup is represented contravariantly by a normal Hopf ideal I whose quotient H/I is geometrically connected, smooth, and has a solvable group of geometric points. The maximal-dimension construction and product closure show that one such ideal is contained in every other one. This file chooses that unique ideal and packages its quotient as the solvable radical of H.

The order on Hopf ideals reverses inclusion of represented closed subgroups. Thus solvableRadicalDefiningIdeal_le says precisely that every connected normal smooth solvable closed subgroup lies in the solvable radical. The chosen ideal is canonical because this universal property determines it uniquely.

Main declarations

• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal: the Hopf ideal cutting out the solvable radical.
• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal_le: the radical's defining ideal is below every candidate ideal.
• TauCeti.FiniteTypeCommHopfAlgCat.eq_solvableRadicalDefiningIdeal_iff: the choice-free universal property characterizing the radical's defining ideal.
• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadical: the coordinate Hopf algebra of the solvable radical.
• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalSpec: its affine group scheme.

References

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

The packaging and characteristic API follow the existing formal construction in TauCeti.Algebra.AlgebraicGroup.Unipotent.Radical.Construction, with solvability replacing unipotence.

This completes the solvable-radical construction in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : HopfIdeal k ↑H.obj

The Hopf ideal cutting out the solvable radical of a finite-type affine group.

It is the unique solvable-radical candidate contained in every other candidate. Since Hopf-ideal order reverses closed-subgroup inclusion, its represented subgroup is the greatest connected normal smooth solvable closed subgroup.

Equations

• H.solvableRadicalDefiningIdeal = Classical.choose ⋯

theorem TauCeti.FiniteTypeCommHopfAlgCat.isSolvableRadicalCandidate_solvableRadicalDefiningIdeal {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : HopfIdeal.IsSolvableRadicalCandidate H H.solvableRadicalDefiningIdeal

The defining ideal of the solvable radical cuts out a connected normal smooth solvable closed subgroup.

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

Every connected normal smooth solvable closed subgroup is contained in the solvable radical.

Contravariantly, this says that the radical's defining Hopf ideal is contained in the ideal cutting out the given subgroup.

theorem TauCeti.FiniteTypeCommHopfAlgCat.eq_solvableRadicalDefiningIdeal_iff {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : I = H.solvableRadicalDefiningIdeal ↔ HopfIdeal.IsSolvableRadicalCandidate H I ∧ ∀ (J : HopfIdeal k ↑H.obj), HopfIdeal.IsSolvableRadicalCandidate H J → I ≤ J

A Hopf ideal is the defining ideal of the solvable radical exactly when it is a candidate contained in every other candidate. This is the choice-free universal property of the radical.

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal_eq_augmentation_iff {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.solvableRadicalDefiningIdeal = HopfIdeal.augmentation k ↑H.obj ↔ ∀ (I : HopfIdeal k ↑H.obj), HopfIdeal.IsSolvableRadicalCandidate H I → I = HopfIdeal.augmentation k ↑H.obj

The solvable radical is trivial exactly when every solvable-radical candidate is the identity subgroup.

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalDefiningIdeal_le_unipotentRadicalDefiningIdeal {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.solvableRadicalDefiningIdeal ≤ H.unipotentRadicalDefiningIdeal

The solvable radical contains the unipotent radical. In coordinate rings, this inclusion is the reverse inequality between their defining Hopf ideals.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.solvableRadical {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : FiniteTypeCommHopfAlgCat k

The finite-type coordinate Hopf algebra of the solvable radical.

Equations

• H.solvableRadical = H.quotient H.solvableRadicalDefiningIdeal

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalCoordinateMap {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H ⟶ H.solvableRadical

The coordinate morphism from an affine group to its solvable radical. Contravariantly, this is the inclusion of the solvable radical into the ambient group.

Equations

• H.solvableRadicalCoordinateMap = H.mkQuotient H.solvableRadicalDefiningIdeal

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalCoordinateMap_def {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.solvableRadicalCoordinateMap = H.mkQuotient H.solvableRadicalDefiningIdeal

The solvable-radical coordinate morphism is the canonical quotient morphism.

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadical_hom_ext {k : Type u} [Field k] {H X : FiniteTypeCommHopfAlgCat k} {f g : H.solvableRadical ⟶ X} (h : CategoryTheory.CategoryStruct.comp H.solvableRadicalCoordinateMap f = CategoryTheory.CategoryStruct.comp H.solvableRadicalCoordinateMap g) : f = g

A morphism out of a solvable radical is determined by its composite with the coordinate quotient map.

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadical_hom_ext_iff {k : Type u} [Field k] {H X : FiniteTypeCommHopfAlgCat k} {f g : H.solvableRadical ⟶ X} : f = g ↔ CategoryTheory.CategoryStruct.comp H.solvableRadicalCoordinateMap f = CategoryTheory.CategoryStruct.comp H.solvableRadicalCoordinateMap g

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalCoordinateMap_ker {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : RingHom.ker ↑↑(toBialgHom H.solvableRadicalCoordinateMap) = H.solvableRadicalDefiningIdeal.toIdeal

The kernel of the solvable-radical coordinate morphism is its defining ideal.

theorem TauCeti.FiniteTypeCommHopfAlgCat.geometricallyConnected_solvableRadical {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : geometricallyConnectedCommHopfAlgProperty k H.solvableRadical.obj

The coordinate Hopf algebra of the solvable radical is geometrically connected.

theorem TauCeti.FiniteTypeCommHopfAlgCat.smooth_solvableRadical {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : Algebra.Smooth k ↑H.solvableRadical.obj

The coordinate Hopf algebra of the solvable radical is smooth.

theorem TauCeti.FiniteTypeCommHopfAlgCat.geometricallySolvable_solvableRadical {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : geometricallySolvablePointsCommHopfAlgProperty k H.solvableRadical.obj

The geometric points of the solvable radical form a solvable group.

theorem TauCeti.FiniteTypeCommHopfAlgCat.isNormal_solvableRadicalDefiningIdeal {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.solvableRadicalDefiningIdeal.IsNormal

The defining ideal of the solvable radical is normal.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalSpec {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))

The affine group scheme represented by the solvable radical's coordinate algebra.

Equations

• H.solvableRadicalSpec = TauCeti.CommHopfAlgCat.quotientSpec H.obj H.solvableRadicalDefiningIdeal

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalSpecι {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.solvableRadicalSpec ⟶ (AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op H.obj)

The canonical inclusion of the solvable radical into the ambient affine group scheme.

Equations

• H.solvableRadicalSpecι = TauCeti.CommHopfAlgCat.quotientSpecι H.obj H.solvableRadicalDefiningIdeal

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalSpecMapOfCandidate {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) (hI : HopfIdeal.IsSolvableRadicalCandidate H I) : CommHopfAlgCat.quotientSpec H.obj I ⟶ H.solvableRadicalSpec

The inclusion of a candidate subgroup into the solvable radical.

Equations

• H.solvableRadicalSpecMapOfCandidate I hI = TauCeti.CommHopfAlgCat.quotientSpecMapOfLe H.obj ⋯

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalSpecMapOfCandidate_comp_solvableRadicalSpecι {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) (hI : HopfIdeal.IsSolvableRadicalCandidate H I) : CategoryTheory.CategoryStruct.comp (H.solvableRadicalSpecMapOfCandidate I hI) H.solvableRadicalSpecι = CommHopfAlgCat.quotientSpecι H.obj I

A candidate's inclusion into the radical followed by the radical's ambient inclusion is the candidate's ambient inclusion.

instance TauCeti.FiniteTypeCommHopfAlgCat.isClosedImmersion_solvableRadicalSpecι {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left H.solvableRadicalSpecι.hom.hom)

The inclusion of the solvable radical is a closed immersion.