Connected affine groups preserve normal-subgroup weight spaces

Let a reduced connected affine group of finite type over an algebraically closed field act on a finite-dimensional comodule. Its rational points preserve every nonzero joint weight space for any normal subgroup of the rational point group. The normal subgroup need not be closed.

Normality permutes the finitely many nonzero joint weights. For a weight vector v, choose a functional taking value one on v. Evaluating that functional on g⁻¹ n g v realizes the conjugated character at n as a regular function of g. Its finite image and connectedness make it constant. This supplies the weight-space invariance used in the Lie--Kolchin induction.

References

• A. Borel, Linear Algebraic Groups, §10.5.
• J. E. Humphreys, Linear Algebraic Groups, §17.6.

@[simp]

theorem TauCeti.Comodule.nonzeroJointWeightAction_basePointsRepresentation_eq_one {k : Type u_1} {H : Type u_2} {V : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] (N : Subgroup (WithConv (H →ₐ[k] k))) [N.Normal] : nonzeroJointWeightAction N (basePointsRepresentation V) = 1

A connected affine group acts trivially on the nonzero joint weights of any normal subgroup of its rational point group, in every finite-dimensional rational representation.

theorem TauCeti.Comodule.map_iInf_eigenspace_basePointsRepresentation_eq_self {k : Type u_1} {H : Type u_2} {V : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] (N : Subgroup (WithConv (H →ₐ[k] k))) [N.Normal] (g : WithConv (H →ₐ[k] k)) (χ : NonzeroJointWeight N (basePointsRepresentation V)) : Submodule.map ((basePointsRepresentation V) g) (⨅ (n : ↥N), ((basePointsRepresentation V) ↑n).eigenspace ↑(↑χ n)) = ⨅ (n : ↥N), ((basePointsRepresentation V) ↑n).eigenspace ↑(↑χ n)

Every rational point preserves each nonzero normal-subgroup joint weight space in a finite-dimensional comodule of a reduced connected affine group.

noncomputable def TauCeti.Comodule.normalWeightSubcomodule {k : Type u_1} {H : Type u_2} {V : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] (N : Subgroup (WithConv (H →ₐ[k] k))) [N.Normal] (χ : NonzeroJointWeight N (basePointsRepresentation V)) : Subcomodule k H V

A nonzero normal-subgroup joint weight space as an ambient-group subcomodule.

Equations

• TauCeti.Comodule.normalWeightSubcomodule N χ = TauCeti.Subcomodule.ofEndOfPointStable (⨅ (n : ↥N), ((TauCeti.Comodule.basePointsRepresentation V) ↑n).eigenspace ↑(↑χ n)) ⋯

@[simp]

theorem TauCeti.Comodule.normalWeightSubcomodule_toSubmodule {k : Type u_1} {H : Type u_2} {V : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] (N : Subgroup (WithConv (H →ₐ[k] k))) [N.Normal] (χ : NonzeroJointWeight N (basePointsRepresentation V)) : (normalWeightSubcomodule N χ).toSubmodule = ⨅ (n : ↥N), ((basePointsRepresentation V) ↑n).eigenspace ↑(↑χ n)

The underlying submodule is the joint eigenspace for the specified character.

@[simp]

theorem TauCeti.Comodule.normalWeightSubcomodule_ne_bot {k : Type u_1} {H : Type u_2} {V : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] (N : Subgroup (WithConv (H →ₐ[k] k))) [N.Normal] (χ : NonzeroJointWeight N (basePointsRepresentation V)) : normalWeightSubcomodule N χ ≠ ⊥

The subcomodule associated to a nonzero joint weight is nonzero.

@[simp]

theorem TauCeti.Comodule.mem_normalWeightSubcomodule {k : Type u_1} {H : Type u_2} {V : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] (N : Subgroup (WithConv (H →ₐ[k] k))) [N.Normal] (χ : NonzeroJointWeight N (basePointsRepresentation V)) (v : V) : v ∈ normalWeightSubcomodule N χ ↔ ∀ (n : ↥N), ((basePointsRepresentation V) ↑n) v = ↑(↑χ n) • v

Membership in the normal weight subcomodule is the joint eigenvector equation.