The unipotent radical of a commutative affine group

For a reduced connected commutative affine group of finite type over an algebraically closed field, the closed unipotent Jordan factor is the unipotent radical. Thus the unipotent points form a smooth connected closed subgroup, rather than merely a subgroup of rational points. This identifies the unipotent factor in the commutative splitting with the canonical radical used in the structure theory of connected solvable groups.

The containment theorem also applies without connectedness of the ambient group: every reduced closed subgroup whose rational points are unipotent lies in the unipotent Jordan factor. Reducedness of that subgroup is essential, since rational points do not detect infinitesimal subgroups. Connectedness of the ambient group is used to make its Jordan factor connected.

The construction reuses the regular Jordan projections and closed factors in JordanDecomposition.ClosedFactors, and the universal property of the unipotent radical.

References

• A. Borel, Linear Algebraic Groups, §§4.7 and 11.21.
• T. A. Springer, Linear Algebraic Groups, §§2.4 and 3.1.

theorem TauCeti.HopfAlgebra.Point.ker_unipotentPartBialgHom_le_of_isUnipotentPoint (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (J : HopfIdeal k H) [IsReduced ↑((↧H).quotient J)] (hJ : ∀ g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) J ↧k, IsUnipotentPoint g) : HopfIdeal.ker (unipotentPartBialgHom k H) ≤ J

Every reduced closed subgroup consisting of unipotent rational points is contained in the closed unipotent Jordan factor. The inequality reverses subgroup containment.

theorem TauCeti.HopfAlgebra.Point.isUnipotentRadicalCandidate_ker_unipotentPartBialgHom (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (hH : geometricallyConnectedCommHopfAlgProperty k ↧H) : HopfIdeal.IsUnipotentRadicalCandidate (FiniteTypeCommHopfAlgCat.of k H) (HopfIdeal.ker (unipotentPartBialgHom k H))

The closed unipotent Jordan factor of a connected commutative affine group is a connected normal smooth unipotent subgroup.

theorem TauCeti.HopfAlgebra.Point.unipotentRadicalDefiningIdeal_eq_ker_unipotentPartBialgHom (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (hH : geometricallyConnectedCommHopfAlgProperty k ↧H) : (FiniteTypeCommHopfAlgCat.of k H).unipotentRadicalDefiningIdeal = HopfIdeal.ker (unipotentPartBialgHom k H)

For a connected commutative affine group, the unipotent radical is exactly the closed unipotent Jordan factor, scheme-theoretically and in every characteristic.

@[simp]

theorem TauCeti.HopfAlgebra.Point.mem_quotientPointsSubgroup_unipotentRadical_iff (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (hH : geometricallyConnectedCommHopfAlgProperty k ↧H) (g : WithConv (H →ₐ[k] k)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (FiniteTypeCommHopfAlgCat.of k H).unipotentRadicalDefiningIdeal ↧k ↔ IsUnipotentPoint g

The rational points of the unipotent radical of a connected commutative affine group are exactly the unipotent rational points of the ambient group.