The unipotent 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 unipotent closed subgroup is represented contravariantly by a normal Hopf ideal I whose quotient H/I is geometrically connected, smooth, and geometrically unipotent. The maximal-dimension construction and its product theorem show that one such ideal is contained in every other one. This file chooses that unique ideal and packages its quotient as the unipotent radical of H.

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

Over a nonperfect field this construction is the k-unipotent radical: no claim is made that it commutes with extension to an algebraic closure. Applying the construction directly to the geometric fibre gives the geometric unipotent radical.

Main declarations

• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal: the Hopf ideal cutting out the unipotent radical.
• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_le: the radical's defining ideal is below every candidate ideal, so every candidate subgroup lies in the radical.
• TauCeti.FiniteTypeCommHopfAlgCat.eq_unipotentRadicalDefiningIdeal_iff: the choice-free universal property characterizing the radical's defining ideal.
• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_eq_augmentation_iff: the radical is trivial exactly when every candidate subgroup is trivial.
• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadical: the coordinate Hopf algebra of the unipotent radical.
• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalSpec: its affine group scheme.

References

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

This completes the construction target in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap.

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

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

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

Equations

• H.unipotentRadicalDefiningIdeal = Classical.choose ⋯

theorem TauCeti.FiniteTypeCommHopfAlgCat.isUnipotentRadicalCandidate_unipotentRadicalDefiningIdeal {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : HopfIdeal.IsUnipotentRadicalCandidate H H.unipotentRadicalDefiningIdeal

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

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

Every connected normal smooth unipotent closed subgroup is contained in the unipotent 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_unipotentRadicalDefiningIdeal_iff {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : I = H.unipotentRadicalDefiningIdeal ↔ HopfIdeal.IsUnipotentRadicalCandidate H I ∧ ∀ (J : HopfIdeal k ↑H.obj), HopfIdeal.IsUnipotentRadicalCandidate H J → I ≤ J

A Hopf ideal is the defining ideal of the unipotent 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.unipotentRadicalDefiningIdeal_eq_augmentation_iff {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑H.obj ↔ ∀ (I : HopfIdeal k ↑H.obj), HopfIdeal.IsUnipotentRadicalCandidate H I → I = HopfIdeal.augmentation k ↑H.obj

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

@[reducible, inline]

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

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

Equations

• H.unipotentRadical = H.quotient H.unipotentRadicalDefiningIdeal

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

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

Equations

• H.unipotentRadicalCoordinateMap = H.mkQuotient H.unipotentRadicalDefiningIdeal

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalCoordinateMap_def {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.unipotentRadicalCoordinateMap = H.mkQuotient H.unipotentRadicalDefiningIdeal

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

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalCoordinateMap_ker {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : RingHom.ker ↑↑(toBialgHom H.unipotentRadicalCoordinateMap) = H.unipotentRadicalDefiningIdeal.toIdeal

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

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

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

theorem TauCeti.FiniteTypeCommHopfAlgCat.smoothUnipotent_unipotentRadical {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : smoothUnipotentCommHopfAlgProperty k H.unipotentRadical

The coordinate Hopf algebra of the unipotent radical is smooth and geometrically unipotent.

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

The defining ideal of the unipotent radical is normal.

@[reducible, inline]

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

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

Equations

• H.unipotentRadicalSpec = TauCeti.CommHopfAlgCat.quotientSpec H.obj H.unipotentRadicalDefiningIdeal

@[reducible, inline]

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

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

Equations

• H.unipotentRadicalSpecι = TauCeti.CommHopfAlgCat.quotientSpecι H.obj H.unipotentRadicalDefiningIdeal

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

The inclusion of a candidate subgroup into the unipotent radical.

Equations

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

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalSpecMapOfCandidate_comp_unipotentRadicalSpecι {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) (hI : HopfIdeal.IsUnipotentRadicalCandidate H I) : CategoryTheory.CategoryStruct.comp (H.unipotentRadicalSpecMapOfCandidate I hI) H.unipotentRadicalSpecι = 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_unipotentRadicalSpecι {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left H.unipotentRadicalSpecι.hom.hom)

The inclusion of the unipotent radical is a closed immersion.