Weights of a coefficient-generating representation separate points

For a homomorphism D(X) → G, two points of D(X) act identically on a representation of G when they agree on its occurring weights. If the representation's matrix coefficients generate the coordinate algebra of G and D(X) → G is a closed immersion, these weights separate all algebra-valued points of D(X). In particular, automorphisms of the character group are determined by their values on the weights of such a representation. This gives a finite set on which to detect the normalizer action when the representation is finite.

The point-separation statements work over commutative semirings and allow nonreduced value algebras. No finite-generation hypothesis on the representation is needed here.

References

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

theorem BialgHom.endOfPoint_comp_eq_of_eqOn_weights {R : Type u_1} {H : Type u_2} {X : Type u_3} {V : Type u_4} {A : Type u_5} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommMonoid X] [AddCommMonoid V] [Module R V] [TauCeti.Comodule R H V] [CommSemiring A] [Algebra R A] (π : H →ₐc[R] MonoidAlgebra R X) (f g : MonoidAlgebra R X →ₐ[R] A) (hfg : ∀ (x : X), TauCeti.DiagonalizableGroup.weightSpace V π.toCoalgHom x ≠ ⊥ → f (MonoidAlgebra.single x 1) = g (MonoidAlgebra.single x 1)) : TauCeti.Comodule.endOfPoint V (f.comp ↑π) = TauCeti.Comodule.endOfPoint V (g.comp ↑π)

Points agreeing on all weights with nonzero weight spaces induce the same action on the representation.

theorem BialgHom.eq_of_eqOn_weights_of_matrixCoefficientSubalgebra_eq_top {R : Type u_1} {H : Type u_2} {X : Type u_3} {V : Type u_4} {A : Type u_5} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommMonoid X] [AddCommMonoid V] [Module R V] [TauCeti.Comodule R H V] [CommSemiring A] [Algebra R A] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) (hV : TauCeti.Comodule.matrixCoefficientSubalgebra = ⊤) (f g : MonoidAlgebra R X →ₐ[R] A) (hfg : ∀ (x : X), TauCeti.DiagonalizableGroup.weightSpace V π.toCoalgHom x ≠ ⊥ → f (MonoidAlgebra.single x 1) = g (MonoidAlgebra.single x 1)) : f = g

For a closed diagonalizable subgroup, the weights of a coefficient-generating ambient representation separate its points over every commutative value algebra.

theorem BialgHom.mulEquiv_eq_of_eqOn_weights {R : Type u_1} {H : Type u_2} {X : Type u_3} {V : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [CommMonoid X] [AddCommMonoid V] [Module R V] [TauCeti.Comodule R H V] [Nontrivial R] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) (hV : TauCeti.Comodule.matrixCoefficientSubalgebra = ⊤) (w w' : X ≃* X) (hww' : Set.EqOn ⇑w ⇑w' {x : X | TauCeti.DiagonalizableGroup.weightSpace V π.toCoalgHom x ≠ ⊥}) : w = w'

Automorphisms of the character group are determined on the occurring weights of a coefficient-generating representation of the ambient group.