Closed subgroups as stabilizers of subspaces

A closed subgroup of an affine group of finite type over a field is the stabilizer of a subspace of a finite-dimensional representation. The representation can be taken inside the regular representation: choose a finite-dimensional subcomodule containing generators of the defining ideal, and intersect it with that ideal. The stabilizer identity holds over every commutative value algebra, so it detects nonreduced subgroup schemes as well as reduced ones.

This is the subspace form of Chevalley's stabilizer construction. Passing to a suitable exterior power gives a line stabilizer, the input for constructing homogeneous spaces as orbits in projective space.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 4.27, the subspace-stabilizer step in the proof of Chevalley's theorem. See also the updated text: https://www.jmilne.org/math/Books/iAG2022.pdf.

noncomputable def TauCeti.HopfIdeal.definingSubspace {k : Type u} [CommRing k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) : Submodule k ↥V

The intersection of a regular subcomodule with the ideal defining a closed subgroup, viewed as a subspace of the subcomodule.

Equations

• I.definingSubspace V = ((Ideal.Quotient.mkₐ k I.toIdeal).toLinearMap ∘ₗ SMulMemClass.subtype V).ker

@[simp]

theorem TauCeti.HopfIdeal.mem_definingSubspace {k : Type u} [CommRing k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) (x : ↥V) : x ∈ I.definingSubspace V ↔ ↑x ∈ I

A vector belongs to the defining subspace exactly when its underlying function vanishes on the closed subgroup.

theorem TauCeti.HopfIdeal.baseChange_definingSubspace {k : Type u} [CommRing k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) (A : Type w) [CommRing A] [Algebra k A] [Module.Flat k A] : Submodule.baseChange A (I.definingSubspace V) = (LinearMap.baseChange A ((Ideal.Quotient.mkₐ k I.toIdeal).toLinearMap ∘ₗ SMulMemClass.subtype V)).ker

Scalar extension of the defining subspace is the kernel of restriction to the subgroup.

theorem TauCeti.HopfIdeal.exists_finite_subcomodule_generating {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Free k ↑H] (I : HopfIdeal k ↑H) (hI : I.toIdeal.FG) : ∃ (V : Subcomodule k ↑H ↑H), Module.Finite k ↥V.toSubmodule ∧ I.toIdeal ≤ Ideal.span (↑V ∩ ↑I)

Over a free coordinate Hopf algebra, a finitely generated Hopf ideal has generators in one finite regular subcomodule. The generator property lets the same subcomodule be used in the stabilizer characterizations at any value-algebra universe.

theorem TauCeti.HopfIdeal.endOfPoint_mapsTo_definingSubspace {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) (A : CommAlgCat k) [Module.Flat k ↑A] (g : ↑(HopfAlgebra.points A)) (hg : g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A) : Set.MapsTo ⇑(Comodule.endOfPoint (↥V) g.ofConv) ↑(Submodule.baseChange (↑A) (I.definingSubspace V)) ↑(Submodule.baseChange (↑A) (I.definingSubspace V))

Every point of the closed subgroup preserves the defining subspace over any value algebra flat over the base.

theorem TauCeti.HopfIdeal.mem_quotientPointsSubgroup_of_mapsTo_definingSubspace {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) (hgen : I.toIdeal ≤ Ideal.span (↑V ∩ ↑I)) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) (hg : Set.MapsTo ⇑(Comodule.endOfPoint (↥V) g.ofConv) ↑(Submodule.baseChange (↑A) (I.definingSubspace V)) ↑(Submodule.baseChange (↑A) (I.definingSubspace V))) : g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A

If the functions in the defining subspace generate the defining ideal, preserving that subspace forces a point to lie in the subgroup.

theorem TauCeti.HopfIdeal.mem_quotientPointsSubgroup_iff_mapsTo_definingSubspace {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) (hgen : I.toIdeal ≤ Ideal.span (↑V ∩ ↑I)) (A : CommAlgCat k) [Module.Flat k ↑A] (g : ↑(HopfAlgebra.points A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A ↔ Set.MapsTo ⇑(Comodule.endOfPoint (↥V) g.ofConv) ↑(Submodule.baseChange (↑A) (I.definingSubspace V)) ↑(Submodule.baseChange (↑A) (I.definingSubspace V))

A regular subcomodule containing ideal generators realizes the closed subgroup as the stabilizer of its defining subspace, over every flat value algebra.

theorem TauCeti.HopfIdeal.mem_quotientPointsSubgroup_iff_map_definingSubspace_eq {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) (hgen : I.toIdeal ≤ Ideal.span (↑V ∩ ↑I)) (A : CommAlgCat k) [Module.Flat k ↑A] (g : ↑(HopfAlgebra.points A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A ↔ Submodule.map (Comodule.endOfPoint (↥V) g.ofConv) (Submodule.baseChange (↑A) (I.definingSubspace V)) = Submodule.baseChange (↑A) (I.definingSubspace V)

The subgroup is the full stabilizer, with equality rather than just preservation of the scalar-extended subspace.

theorem TauCeti.HopfIdeal.exists_finite_subcomodule_stabilizer {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (hI : I.toIdeal.FG) : ∃ (V : Subcomodule k ↑H ↑H), Module.Finite k ↥V.toSubmodule ∧ ∀ (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)), g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A ↔ Submodule.map (Comodule.endOfPoint (↥V) g.ofConv) (Submodule.baseChange (↑A) (I.definingSubspace V)) = Submodule.baseChange (↑A) (I.definingSubspace V)

A closed subgroup with finitely generated defining ideal is the stabilizer of a subspace in a finite-dimensional regular subcomodule. In particular this applies to every closed subgroup of a finite-type affine group. The same subspace works for all value algebras.