The defining subspace as a subgroup representation

Let I define a closed subgroup of an affine group with coordinate Hopf algebra H, and let V be a regular H-subcomodule. The subspace of functions in V vanishing on the subgroup is a subcomodule after corestriction to H/I. It is the kernel of restriction V → H/I, viewed as a morphism to the subgroup's regular comodule.

This equips the defining subspace in Chevalley's stabilizer construction with its subgroup representation. It is intended as input to an exterior-power construction of an invariant line under additional hypotheses, such as finite-dimensionality over a field. The subcomodule construction itself requires no reducedness or smoothness.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 4.27 and Lemma 4.28.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2.

noncomputable def TauCeti.HopfIdeal.restrictionHom {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) : Comodule.Hom k (↑H ⧸ I.toIdeal) (↥V) (↑H ⧸ I.toIdeal)

Restrict a regular subcomodule's functions to a closed subgroup, as a morphism to the subgroup's regular comodule.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.HopfIdeal.restrictionHom_toLinearMap {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) : (I.restrictionHom V).toLinearMap = (Ideal.Quotient.mkₐ k I.toIdeal).toLinearMap ∘ₗ SMulMemClass.subtype V

The linear map underlying restriction is the quotient map after inclusion in H.

@[simp]

theorem TauCeti.HopfIdeal.restrictionHom_apply {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) (x : ↥V) : (I.restrictionHom V) x = (Ideal.Quotient.mk I.toIdeal) ↑x

Restriction sends a function to its residue class modulo the defining ideal.

noncomputable def TauCeti.HopfIdeal.definingSubcomodule {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) [Module.Flat k (↑H ⧸ I.toIdeal)] (V : Subcomodule k ↑H ↑H) : Subcomodule k (↑H ⧸ I.toIdeal) ↥V

The functions in a regular subcomodule vanishing on a closed subgroup, as a subcomodule of the representation restricted to that subgroup.

Equations

• I.definingSubcomodule V = (I.restrictionHom V).ker

@[simp]

theorem TauCeti.HopfIdeal.definingSubcomodule_toSubmodule {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) [Module.Flat k (↑H ⧸ I.toIdeal)] (V : Subcomodule k ↑H ↑H) : (I.definingSubcomodule V).toSubmodule = I.definingSubspace V

The defining subcomodule has exactly the previously defined vanishing subspace.

@[simp]

theorem TauCeti.HopfIdeal.mem_definingSubcomodule {k : Type u} [CommRing k] {H : CommHopfAlgCat k} [Module.Flat k ↑H] (I : HopfIdeal k ↑H) [Module.Flat k (↑H ⧸ I.toIdeal)] (V : Subcomodule k ↑H ↑H) (x : ↥V) : x ∈ I.definingSubcomodule V ↔ ↑x ∈ I

A vector is in the defining subcomodule precisely when it vanishes on the subgroup.