The Hopf ideal vanishing on a subgroup of rational points

The functions vanishing on any subgroup of the rational points of an affine group form a radical Hopf ideal. Its quotient is the reduced closed subgroup generated by those points. The construction and its order-theoretic API need no finite-type or algebraic-closedness assumption. The density statement vanishingIdeal_top additionally assumes a reduced finite-type algebra over an algebraically closed field. This construction connects abstract point subgroups, such as commutator subgroups, with closed subgroup schemes.

Passing to the generated closed subgroup is compatible with commutators: the commutator of the closed subgroups generated by two point subgroups lies in the closed subgroup generated by their commutator. The trivial point subgroup generates the trivial closed subgroup.

Main declarations

• TauCeti.HopfIdeal.vanishingIdeal: the Hopf ideal of functions vanishing on a point subgroup.
• TauCeti.HopfIdeal.le_vanishingIdeal_iff: its quotient is the smallest closed subgroup containing the point subgroup.
• TauCeti.HopfIdeal.commutator_quotientPointsSubgroup_vanishingIdeal_le: commutators of closures lie in the closure of the commutator.
• TauCeti.HopfIdeal.quotientPointsSubgroup_vanishingIdeal_bot: the closure of the trivial subgroup is trivial.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §4.

def TauCeti.HopfIdeal.vanishingIdeal {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S : Subgroup (WithConv (H →ₐ[k] k))) : HopfIdeal k H

The radical Hopf ideal of functions vanishing on a subgroup of rational points.

Equations

• TauCeti.HopfIdeal.vanishingIdeal S = TauCeti.HopfIdeal.ofIdeal (TauCeti.HopfIdeal.pointKernelIdeal✝ S) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.HopfIdeal.mem_vanishingIdeal {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S : Subgroup (WithConv (H →ₐ[k] k))) (x : H) : x ∈ vanishingIdeal S ↔ ∀ (g : ↥S), (↑g).ofConv x = 0

Membership means vanishing at every point of the subgroup.

theorem TauCeti.HopfIdeal.eq_zero_of_forall_liftQuotientPoint_apply_eq_zero {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S : Subgroup (WithConv (H →ₐ[k] k))) (x : ↑(CommHopfAlgCat.quotient (↧H) (vanishingIdeal S))) (hx : ∀ (g : ↥S), (CommHopfAlgCat.liftQuotientPoint (↧H) (vanishingIdeal S) ↧k ↑g ⋯).ofConv x = 0) : x = 0

Evaluations at the original subgroup points separate the coordinate algebra of its closure.

theorem TauCeti.HopfIdeal.vanishingIdeal_toIdeal {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S : Subgroup (WithConv (H →ₐ[k] k))) : (vanishingIdeal S).toIdeal = ⨅ (g : ↥S), RingHom.ker (↑g).ofConv

The underlying ideal is the intersection of the kernels of the evaluations.

theorem TauCeti.HopfIdeal.isRadical_vanishingIdeal {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S : Subgroup (WithConv (H →ₐ[k] k))) : (vanishingIdeal S).toIdeal.IsRadical

The vanishing ideal of a point subgroup is radical.

instance TauCeti.HopfIdeal.isReduced_quotient_vanishingIdeal {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S : Subgroup (WithConv (H →ₐ[k] k))) : IsReduced ↑(CommHopfAlgCat.quotient (↧H) (vanishingIdeal S))

The closed subgroup cut out by the vanishing ideal of a point subgroup is reduced.

theorem TauCeti.HopfIdeal.le_vanishingIdeal_iff {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S : Subgroup (WithConv (H →ₐ[k] k))) (I : HopfIdeal k H) : I ≤ vanishingIdeal S ↔ S ≤ CommHopfAlgCat.quotientPointsSubgroup (↧H) I ↧k

A Hopf ideal vanishes on a point subgroup exactly when the associated closed subgroup contains that point subgroup. This is the minimality property of its closed subgroup closure.

theorem TauCeti.HopfIdeal.commutator_quotientPointsSubgroup_vanishingIdeal_le {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S T : Subgroup (WithConv (H →ₐ[k] k))) : ⁅CommHopfAlgCat.quotientPointsSubgroup (↧H) (vanishingIdeal S) ↧k, CommHopfAlgCat.quotientPointsSubgroup (↧H) (vanishingIdeal T) ↧k⁆ ≤ CommHopfAlgCat.quotientPointsSubgroup (↧H) (vanishingIdeal ⁅S, T⁆) ↧k

Commutators of closures lie in the closure of the commutators. For subgroups S and T of rational points, the commutator of the closed subgroups they generate is contained in the closed subgroup generated by ⁅S, T⁆. Here the closed subgroup generated by S is the one cut out by the functions vanishing on S.

@[simp]

theorem TauCeti.HopfIdeal.quotientPointsSubgroup_vanishingIdeal_bot {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] : CommHopfAlgCat.quotientPointsSubgroup (↧H) (vanishingIdeal ⊥) ↧k = ⊥

The closed subgroup generated by the trivial subgroup of rational points is trivial.

@[simp]

theorem TauCeti.HopfIdeal.vanishingIdeal_bot {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] : vanishingIdeal ⊥ = augmentation k H

The closure of the trivial point subgroup is the identity subgroup scheme.

@[simp]

theorem TauCeti.HopfIdeal.vanishingIdeal_eq_augmentation_iff {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] (S : Subgroup (WithConv (H →ₐ[k] k))) : vanishingIdeal S = augmentation k H ↔ S = ⊥

A point subgroup has trivial reduced closure exactly when it is trivial.

@[simp]

theorem TauCeti.HopfIdeal.vanishingIdeal_top {k : Type u_1} {H : Type u_2} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] : vanishingIdeal ⊤ = ⊥

Rational points are schematically dense in a reduced finite-type affine group over an algebraically closed field.