Derived subgroups of closures of point subgroups

The derived closed subgroup of the reduced closure of a rational-point subgroup S is the reduced closure of ⁅S, S⁆. This holds over any field: the points of S separate functions on their own closure, and their pairs therefore separate its tensor square. In particular, this comparison can be iterated along the abstract derived series.

For a reduced finite-type affine group over an algebraically closed field, specializing to all rational points identifies the derived defining ideal with the vanishing ideal of the abstract commutator subgroup. Thus the all-points comparison is a specialization of the subgroup-closure comparison.

If the rational points of the ambient group have finite derived length, then commutators of closures lie in the closure of the commutator (TauCeti.HopfIdeal.commutator_quotientPointsSubgroup_vanishingIdeal_le), so the rational points of the derived subgroup have strictly smaller derived length. This is the measure the Lie--Kolchin induction decreases.

Main declarations

• TauCeti.CommHopfAlgCat.derivedDefiningIdeal_eq_vanishingIdeal_commutator: the derived subgroup is the closure of the abstract commutator subgroup of rational points.
• TauCeti.CommHopfAlgCat.derivedSeries_points_derived_eq_bot: if the rational points have derived length at most n + 1, those of the derived subgroup have derived length at most n.

References

• A. Borel, Linear Algebraic Groups, §2.3 and §10.5.
• J. S. Milne, Algebraic Groups (2017), §6d.

theorem TauCeti.CommHopfAlgCat.comapOfSurjective_derivedDefiningIdeal_quotient_vanishingIdeal_eq_vanishingIdeal_commutator {k : Type u_1} [Field k] {H : CommHopfAlgCat k} (S : Subgroup (WithConv (↑H →ₐ[k] k))) : (derivedDefiningIdeal ↑(quotient H (HopfIdeal.vanishingIdeal S))).comapOfSurjective (CommHopfAlgCat.Hom.hom (mkQuotient H (HopfIdeal.vanishingIdeal S))) ⋯ = HopfIdeal.vanishingIdeal ⁅S, S⁆

Taking the derived closed subgroup commutes with taking the reduced closure of a rational-point subgroup. The equality is stated as equality of defining ideals in the ambient coordinate algebra.

theorem TauCeti.CommHopfAlgCat.derivedDefiningIdeal_eq_vanishingIdeal_commutator_of_dense_points {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (hdense : HopfIdeal.vanishingIdeal ⊤ = ⊥) : derivedDefiningIdeal H = HopfIdeal.vanishingIdeal (commutator (WithConv (H →ₐ[k] k)))

If rational points are schematically dense, the derived subgroup is the reduced closed subgroup generated by their abstract commutator subgroup.

theorem TauCeti.CommHopfAlgCat.derivedDefiningIdeal_eq_vanishingIdeal_commutator {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] : derivedDefiningIdeal H = HopfIdeal.vanishingIdeal (commutator (WithConv (H →ₐ[k] k)))

The derived subgroup is the reduced closed subgroup generated by the abstract commutator subgroup of rational points.

@[simp]

theorem TauCeti.CommHopfAlgCat.mem_derivedDefiningIdeal_iff_forall_commutator_apply_eq_zero {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (x : H) : x ∈ derivedDefiningIdeal H ↔ ∀ (g : ↥(commutator (WithConv (H →ₐ[k] k)))), (↑g).ofConv x = 0

A function vanishes on the derived subgroup exactly when it vanishes on every element of the abstract commutator subgroup of rational points.

theorem TauCeti.CommHopfAlgCat.derivedSeries_points_derived_eq_bot {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] {n : ℕ} (hn : derivedSeries (WithConv (H →ₐ[k] k)) (n + 1) = ⊥) : derivedSeries (WithConv (↑(quotient (↧H) (derivedDefiningIdeal H)) →ₐ[k] k)) n = ⊥

The derived subgroup has strictly shorter derived length. If the rational points of a reduced finite-type affine group over an algebraically closed field have derived length at most n + 1, then the rational points of its scheme-theoretic derived subgroup have derived length at most n.