The normalizer action on characters

For a closed diagonalizable subgroup D(X) → G, a rational point normalizing the subgroup induces an automorphism of X by pullback along inverse conjugation. These automorphisms form a group homomorphism, with the variance suited to the action on weight spaces. Points of the diagonalizable subgroup act trivially on characters. The kernel consists exactly of normalizing points whose conjugation restricts to the identity on the subgroup scheme.

Normalization means stabilization of the defining Hopf ideal, not normalization of rational points alone. Thus the construction detects the subgroup scheme, including nonreduced ones. The coordinate map is assumed surjective, expressing that D(X) → G is a closed immersion. The base has connected prime spectrum, as required to recover characters from group-like elements. Neither smoothness nor finite generation is required.

The construction transports the restricted conjugation HopfIdeal.quotientPointConjugation along HopfIdeal.kerLiftBialgEquiv and uses TauCeti.MonoidAlgebra.groupLikeEquiv to recover the character automorphism.

References

• J. S. Milne, Algebraic Groups (2017), §21.1.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2.

noncomputable def BialgHom.normalizerPoints {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) : Subgroup (WithConv (H →ₐ[R] R))

The rational points stabilizing the defining Hopf ideal of a closed diagonalizable subgroup. This is the rational normalizer of the subgroup scheme.

Equations

• π.normalizerPoints hπ = MulAction.stabilizer (WithConv (H →ₐ[R] R)) (TauCeti.HopfIdeal.kerOfSurjective π hπ)

@[simp]

theorem BialgHom.mem_normalizerPoints {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) (g : WithConv (H →ₐ[R] R)) : g ∈ π.normalizerPoints hπ ↔ (TauCeti.HopfIdeal.kerOfSurjective π hπ).conjugate g = TauCeti.HopfIdeal.kerOfSurjective π hπ

Normalizer membership means that conjugation preserves the defining Hopf ideal.

noncomputable def BialgHom.mapDomainToNormalizer {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) : WithConv (MonoidAlgebra R X →ₐ[R] R) →* ↥(π.normalizerPoints hπ)

The points of the diagonalizable subgroup map into its scheme normalizer.

Equations

• π.mapDomainToNormalizer hπ = (TauCeti.AlgHom.mapDomain π).codRestrict (π.normalizerPoints hπ) ⋯

@[simp]

theorem BialgHom.coe_mapDomainToNormalizer {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) (t : WithConv (MonoidAlgebra R X →ₐ[R] R)) : ↑((π.mapDomainToNormalizer hπ) t) = (TauCeti.AlgHom.mapDomain π) t

The normalizer inclusion recovers the original point of the ambient group.

noncomputable def BialgHom.normalizerCharacterHom {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) [ConnectedSpace (PrimeSpectrum R)] : ↥(π.normalizerPoints hπ) →* MulAut X

Inverse conjugation defines the normalizer's action on the character group.

Equations

• π.normalizerCharacterHom hπ = { toFun := BialgHom.normalizerCharacterEquiv✝ π hπ, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem BialgHom.normalizerCharacterHom_comp {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) [ConnectedSpace (PrimeSpectrum R)] (g : ↥(π.normalizerPoints hπ)) : (↑π).comp (TauCeti.HopfAlgebra.pointConjugationAlgHom (↑g)⁻¹) = (↑(MonoidAlgebra.domCongr R R ((π.normalizerCharacterHom hπ) g))).comp ↑π

The induced character automorphism is characterized by the coordinate equation for inverse conjugation on the closed subgroup.

theorem BialgHom.normalizerCharacterHom_unique {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) [ConnectedSpace (PrimeSpectrum R)] (g : ↥(π.normalizerPoints hπ)) (w : X ≃* X) (hw : (↑π).comp (TauCeti.HopfAlgebra.pointConjugationAlgHom (↑g)⁻¹) = (↑(MonoidAlgebra.domCongr R R w)).comp ↑π) : w = (π.normalizerCharacterHom hπ) g

The normalization equation determines the induced character automorphism uniquely.

theorem BialgHom.normalizerCharacterHom_eq_one_iff {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) [ConnectedSpace (PrimeSpectrum R)] (g : ↥(π.normalizerPoints hπ)) : (π.normalizerCharacterHom hπ) g = 1 ↔ (↑π).comp (TauCeti.HopfAlgebra.pointConjugationAlgHom (↑g)⁻¹) = ↑π

A normalizing point acts trivially on characters exactly when its inverse conjugation restricts to the identity on the subgroup scheme.

@[simp]

theorem BialgHom.normalizerCharacterHom_mapDomainToNormalizer {R : Type u_1} {H : Type u_2} {X : Type u_3} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) [ConnectedSpace (PrimeSpectrum R)] (t : WithConv (MonoidAlgebra R X →ₐ[R] R)) : (π.normalizerCharacterHom hπ) ((π.mapDomainToNormalizer hπ) t) = 1

Points of the diagonalizable subgroup act trivially on its character group.