Finiteness of the normalizer action on characters

The rational scheme normalizer of a closed diagonalizable subgroup of a finite-type affine group over a field has finite image in the automorphisms of its character group. Consequently, the quotient of the normalizer's rational points by the kernel of this action is finite. By BialgHom.normalizerCharacterHom_eq_one_iff, this kernel is exactly the points whose conjugation restricts to the identity on the subgroup scheme, its rational centralizer. This is the finiteness step for the Weyl group of a maximal torus; identifying its centralizer with the torus and identifying the resulting finite group with the reflection group require further structure theory.

A finite-dimensional coefficient-generating representation exists by the affine-group embedding theorem. The normalizer permutes its finite set of weights, and agreement on those weights determines the character automorphism. The more general criterion below works over a commutative ring with connected spectrum, given a finite coefficient-generating comodule.

The ambient group and diagonalizable subgroup may be nonreduced. These statements concern rational points of the scheme normalizer, not the normalizer of the rational-point subgroup.

References

• J. S. Milne, Algebraic Groups (2017), §§4.a and 21.1.
• T. A. Springer, Linear Algebraic Groups, §7.1.

theorem BialgHom.finite_range_normalizerCharacterHom_of_matrixCoefficientSubalgebra_eq_top {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] [ConnectedSpace (PrimeSpectrum R)] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) {V : Type u_4} [AddCommMonoid V] [Module R V] [TauCeti.Comodule R H V] [Module.Finite R V] (hV : TauCeti.Comodule.matrixCoefficientSubalgebra = ⊤) : (Set.range ⇑(π.normalizerCharacterHom hπ)).Finite

A finite coefficient-generating representation detects the character action of the normalizer on its finite set of weights, so the character action has finite image.

theorem BialgHom.finite_range_normalizerCharacterHom {k : Type u_1} {H : Type u_2} {X : Type u_3} [Field k] [CommRing H] [HopfAlgebra k H] [CommGroup X] [Algebra.FiniteType k H] (π : H →ₐc[k] MonoidAlgebra k X) (hπ : Function.Surjective ⇑π) : (Set.range ⇑(π.normalizerCharacterHom hπ)).Finite

The rational scheme normalizer of a closed diagonalizable subgroup of a finite-type affine group over a field has finite image on the character group.

instance BialgHom.finite_normalizerPoints_quotient_ker_normalizerCharacterHom {k : Type u_1} {H : Type u_2} {X : Type u_3} [Field k] [CommRing H] [HopfAlgebra k H] [CommGroup X] [Algebra.FiniteType k H] (π : H →ₐc[k] MonoidAlgebra k X) (hπ : Function.Surjective ⇑π) : Finite (↥(π.normalizerPoints hπ) ⧸ (π.normalizerCharacterHom hπ).ker)

The rational normalizer modulo the kernel of its character action is finite. The kernel is the rational centralizer of the diagonalizable subgroup scheme, as characterized by normalizerCharacterHom_eq_one_iff.