Rational points and the scheme-theoretic derived series #
When rational points are schematically dense, the nth derived defining ideal is the
vanishing ideal of the nth abstract derived subgroup of rational points. In particular,
this holds for reduced finite-type affine groups over algebraically closed fields.
References #
- A. Borel, Linear Algebraic Groups, §10.5.
- J. S. Milne, Algebraic Groups (2017), §6d.
theorem
CommHopfAlgCat.derivedSeriesDefiningIdeal_eq_vanishingIdeal_derivedSeries_of_dense_points
{k : Type u_1}
[Field k]
(H : CommHopfAlgCat k)
(h : TauCeti.HopfIdeal.vanishingIdeal ⊤ = ⊥)
(n : ℕ)
:
H.derivedSeriesDefiningIdeal n = TauCeti.HopfIdeal.vanishingIdeal (derivedSeries (WithConv (↑H →ₐ[k] k)) n)
For an affine group with schematically dense rational points, each scheme-theoretic derived subgroup is the reduced closure of the corresponding abstract derived subgroup.
theorem
CommHopfAlgCat.derivedSeriesDefiningIdeal_eq_vanishingIdeal_derivedSeries
{k : Type u_1}
[Field k]
(H : CommHopfAlgCat k)
[IsAlgClosed k]
[Algebra.FiniteType k ↑H]
[IsReduced ↑H]
(n : ℕ)
:
H.derivedSeriesDefiningIdeal n = TauCeti.HopfIdeal.vanishingIdeal (derivedSeries (WithConv (↑H →ₐ[k] k)) n)
Each scheme-theoretic derived subgroup of a reduced finite-type affine group over an algebraically closed field is the reduced closure of the corresponding abstract derived subgroup of rational points.