Recovering reduced closed subgroups from geometric points

Let H be a commutative Hopf algebra over a field and fix an algebraically closed extension. A Hopf ideal I cuts out the subgroup of extension-valued points of H that vanish on I. If the quotient H/I is reduced and of finite type, its points separate functions, so this subgroup determines I.

The order statement is contravariant: if every point cut out by J is also cut out by I, then I ≤ J, provided H/J is reduced and of finite type. Applying it in both directions shows that two reduced finite-type closed subgroups with the same points have the same defining Hopf ideal.

Main declarations

• TauCeti.HopfIdeal.le_of_quotientPointsSubgroup_le: recover an inclusion of Hopf ideals from the reverse inclusion of their algebraically closed point subgroups.
• TauCeti.HopfIdeal.eq_of_quotientPointsSubgroup_eq: reduced finite-type closed subgroups are determined by their algebraically closed points.

References

• J. S. Milne, Algebraic Groups (2017), Sections 1.d and 2.a.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 3.2.

This is the point-separation input for the maximal-torus step in Layer 7 of the ReductiveGroups roadmap. It allows pointwise centralizer calculations to determine reduced closed subgroup schemes.

theorem TauCeti.HopfIdeal.le_of_quotientPointsSubgroup_le {k : Type u} [Field k] {K : Type w} [Field K] [Algebra k K] [IsAlgClosed K] {H : CommHopfAlgCat k} {I J : HopfIdeal k ↑H} [Algebra.FiniteType k ↑(CommHopfAlgCat.quotient H J)] [IsReduced ↑(CommHopfAlgCat.quotient H J)] (hpoints : CommHopfAlgCat.quotientPointsSubgroup H J ↧K ≤ CommHopfAlgCat.quotientPointsSubgroup H I ↧K) : I ≤ J

Recover an inclusion of Hopf ideals from the reverse inclusion of their point subgroups.

Only the quotient by the ideal on the right of the conclusion must be reduced and of finite type. Those hypotheses make its K-valued points separate functions.

theorem TauCeti.HopfIdeal.eq_of_quotientPointsSubgroup_eq {k : Type u} [Field k] {K : Type w} [Field K] [Algebra k K] [IsAlgClosed K] {H : CommHopfAlgCat k} {I J : HopfIdeal k ↑H} [Algebra.FiniteType k ↑(CommHopfAlgCat.quotient H I)] [IsReduced ↑(CommHopfAlgCat.quotient H I)] [Algebra.FiniteType k ↑(CommHopfAlgCat.quotient H J)] [IsReduced ↑(CommHopfAlgCat.quotient H J)] (hpoints : CommHopfAlgCat.quotientPointsSubgroup H I ↧K = CommHopfAlgCat.quotientPointsSubgroup H J ↧K) : I = J

Two reduced finite-type closed subgroups of an affine group have the same defining Hopf ideal when they have the same points over an algebraically closed extension.