Exterior-line detection of closed subgroups

A finite-dimensional regular subcomodule containing generators of a closed subgroup's ideal realizes that subgroup as a subspace stabilizer. Over every commutative value algebra A, the top-exterior-line criterion in the exterior algebra over A of A ⊗ V, together with compatibility of the exterior point action with scalar extension, turns this into the stabilizer of a line in the finite-dimensional exterior-power comodule ⋀ᵈ V, where d is the dimension of the defining subspace. This works for nonreduced value algebras and subgroup schemes. The existence of a stabilizing line, together with its unique subgroup character, is proved in TauCeti.Algebra.AlgebraicGroup.Representation.ExteriorStabilizer.Character.

Main statements

• TauCeti.Comodule.map_endOfPoint_baseChange_range_exteriorPowerMap_finrank_eq_iff: a point stabilizes the top exterior line of a subspace exactly when it stabilizes the subspace.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 4.27 and Lemma 4.28.

theorem TauCeti.Comodule.map_endOfPoint_baseChange_range_exteriorPowerMap_finrank_eq_iff {k : Type u} [Field k] {H : Type v} [CommSemiring H] [HopfAlgebra k H] {V : Type u_1} [AddCommGroup V] [Module k V] [Module.Finite k V] [Comodule k H V] (W : Submodule k V) (A : Type u_2) [CommRing A] [Algebra k A] (g : WithConv (H →ₐ[k] A)) : Submodule.map (endOfPoint (↥(⋀[k]^(Module.finrank k ↥W) V)) g.ofConv) (Submodule.baseChange A (exteriorPower.map (Module.finrank k ↥W) W.subtype).range) = Submodule.baseChange A (exteriorPower.map (Module.finrank k ↥W) W.subtype).range ↔ Submodule.map (endOfPoint V g.ofConv) (Submodule.baseChange A W) = Submodule.baseChange A W

Over a field, a point stabilizes the scalar extension of the top exterior line of a subspace W of a finite-dimensional representation V exactly when it stabilizes the scalar extension of W. The line is the image of ⋀ᵈ W in the representation ⋀ᵈ V, where d = dim W. This holds over every commutative value algebra, including nonreduced ones.

theorem TauCeti.HopfIdeal.mem_quotientPointsSubgroup_iff_map_baseChange_range_exteriorPowerMap_eq {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (V : Subcomodule k ↑H ↑H) [Module.Finite k ↥V] (hgen : I.toIdeal ≤ Ideal.span (↑V ∩ ↑I)) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup H I A ↔ Submodule.map (Comodule.endOfPoint (↥(⋀[k]^(Module.finrank k ↥(I.definingSubspace V)) ↥V)) g.ofConv) (Submodule.baseChange (↑A) (exteriorPower.map (Module.finrank k ↥(I.definingSubspace V)) (I.definingSubspace V).subtype).range) = Submodule.baseChange (↑A) (exteriorPower.map (Module.finrank k ↥(I.definingSubspace V)) (I.definingSubspace V).subtype).range

A finite regular subcomodule containing ideal generators realizes the closed subgroup as the stabilizer of a line: the image of the top exterior power of the defining subspace in the corresponding exterior power of the subcomodule. This holds over every value algebra.