Normalizers transport weight spaces

Suppose a rational point g normalizes a homomorphism D(X) → G, with inverse conjugation inducing the automorphism w of the character group X. In every rational representation of G, the action of g carries the weight space of x onto that of w x.

Normalization is expressed by an equality of coordinate morphisms valid over every value algebra, including nonreduced ones. No smoothness, reducedness, finite type, or field hypothesis is needed. For the adjoint representation and a split maximal torus, this is the transport of root spaces underlying the Weyl action on roots. The same transport statement holds for commutative monoid algebras.

References

• J. S. Milne, Algebraic Groups (2017), §21.1.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

theorem TauCeti.DiagonalizableGroup.basePointsRepresentation_mem_weightSpace {R : Type u_1} {H : Type u_2} {X : Type u_3} {V : Type u_4} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommMonoid X] [AddCommMonoid V] [Module R V] [Comodule R H V] (π : H →ₐc[R] MonoidAlgebra R X) (g : WithConv (H →ₐ[R] R)) (w : X ≃* X) (hg : (↑π).comp (HopfAlgebra.pointConjugationAlgHom g⁻¹) = (↑(MonoidAlgebra.domCongr R R w)).comp ↑π) {x : X} {v : V} (hv : v ∈ weightSpace V π.toCoalgHom x) : ((Comodule.basePointsRepresentation V) g) v ∈ weightSpace V π.toCoalgHom (w x)

A normalizing rational point sends weight vectors to the weights obtained by pullback along inverse conjugation.

theorem TauCeti.DiagonalizableGroup.map_weightSpace_basePointsRepresentation {R : Type u_1} {H : Type u_2} {X : Type u_3} {V : Type u_4} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommMonoid X] [AddCommMonoid V] [Module R V] [Comodule R H V] (π : H →ₐc[R] MonoidAlgebra R X) (g : WithConv (H →ₐ[R] R)) (w : X ≃* X) (hg : (↑π).comp (HopfAlgebra.pointConjugationAlgHom g⁻¹) = (↑(MonoidAlgebra.domCongr R R w)).comp ↑π) (x : X) : Submodule.map ((Comodule.basePointsRepresentation V) g) (weightSpace V π.toCoalgHom x) = weightSpace V π.toCoalgHom (w x)

A normalizing point carries a weight space onto the permuted weight space.

theorem TauCeti.DiagonalizableGroup.weightSpace_apply_ne_bot_iff {R : Type u_1} {H : Type u_2} {X : Type u_3} {V : Type u_4} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommMonoid X] [AddCommMonoid V] [Module R V] [Comodule R H V] (π : H →ₐc[R] MonoidAlgebra R X) (g : WithConv (H →ₐ[R] R)) (w : X ≃* X) (hg : (↑π).comp (HopfAlgebra.pointConjugationAlgHom g⁻¹) = (↑(MonoidAlgebra.domCongr R R w)).comp ↑π) (x : X) : weightSpace V π.toCoalgHom (w x) ≠ ⊥ ↔ weightSpace V π.toCoalgHom x ≠ ⊥

Normalization preserves whether a weight space is nonzero.