The closed normalizer of a diagonalizable subgroup

For a closed diagonalizable subgroup D(X) → G, the normalizer is a closed subgroup scheme. Its equations are the coefficients of universal conjugation applied to the defining ideal of D(X), together with their antipodes. These two sets of equations require conjugation by a point and its inverse to preserve the subgroup.

The point criterion tests normalization after every extension of the value algebra. Thus it captures the subgroup scheme, including its infinitesimal structure, rather than merely its rational points. The construction works over any commutative ring; smoothness and finite type are not required. It supplies a represented normalizer for the character action and for normalizer quotients of split tori.

The coefficient argument follows TauCeti.Algebra.AlgebraicGroup.Center.Basic, using the canonical basis of the group algebra in place of a chosen vector-space basis. The Hopf-ideal structure comes from HopfIdeal.ofIdealOfPointsSubgroup.

References

• J. S. Milne, Algebraic Groups (2017), §1.j, Proposition 1.83.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

noncomputable def BialgHom.universalNormalizerPoints {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (A : CommAlgCat R) : Subgroup (WithConv (H →ₐ[R] ↑A))

Points normalizing the diagonalizable subgroup after every extension of their value algebra. The subgroup at each extension is the image of the points of D(X).

@[simp]

theorem BialgHom.mem_universalNormalizerPoints {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (A : CommAlgCat R) (g : WithConv (H →ₐ[R] ↑A)) : g ∈ π.universalNormalizerPoints A ↔ ∀ (B : CommAlgCat R) (φ : ↑A →ₐ[R] ↑B), φ.mapValue g ∈ Subgroup.normalizer ↑π.mapDomain.range

Universal normalization means normalization of the point subgroup over every extension.

theorem BialgHom.mapValue_mem_universalNormalizerPoints {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {A B : CommAlgCat R} (φ : ↑A →ₐ[R] ↑B) {g : WithConv (H →ₐ[R] ↑A)} (hg : g ∈ π.universalNormalizerPoints A) : φ.mapValue g ∈ π.universalNormalizerPoints B

Changing the value algebra preserves universal normalization.

theorem BialgHom.mapDomain_mem_universalNormalizerPoints {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (A : CommAlgCat R) (t : WithConv (MonoidAlgebra R X →ₐ[R] ↑A)) : π.mapDomain t ∈ π.universalNormalizerPoints A

The diagonalizable subgroup lies in its universal normalizer.

@[simp]

theorem BialgHom.universalNormalizerPoints_base_eq_normalizerPoints {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) : π.universalNormalizerPoints ↧R = π.normalizerPoints hπ

On base-valued points, universal normalization agrees with stabilization of the defining Hopf ideal, the existing rational normalizer interface.

noncomputable def BialgHom.normalizerCoefficient {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (x : H) (i : X) : H

A coefficient of the universal conjugation restricted to D(X), in its character basis. Only coefficients at elements in ker π enter the normalizer equations.

theorem BialgHom.normalizerCoefficient_def {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (x : H) (i : X) : π.normalizerCoefficient x i = ((TensorProduct.equivFinsuppOfBasisLeft (MonoidAlgebra.basis X R)) ((TensorProduct.comm R H (MonoidAlgebra R X)) ((Algebra.TensorProduct.map (AlgHom.id R H) ↑π) (TauCeti.HopfAlgebra.conjugationAlgHom x)))) i

The normalizer coefficient is the indicated coordinate in the character basis.

noncomputable def BialgHom.normalizerHopfIdeal {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) : TauCeti.HopfIdeal R H

The Hopf ideal cutting out the closed normalizer of D(X) → G. Its quotient represents normalization of the subgroup after every value-algebra extension.

@[simp]

theorem BialgHom.normalizerHopfIdeal_toIdeal {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) : (π.normalizerHopfIdeal hπ).toIdeal = Ideal.span {y : H | ∃ (x : H), π x = 0 ∧ ∃ (i : X), π.normalizerCoefficient x i = y} ⊔ Ideal.map (HopfAlgebra.antipodeAlgHom R H) (Ideal.span {y : H | ∃ (x : H), π x = 0 ∧ ∃ (i : X), π.normalizerCoefficient x i = y})

The normalizer ideal is generated by the conjugation coefficients and their antipodes.

theorem BialgHom.normalizerHopfIdeal_le_ker_iff {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) (A : CommAlgCat R) (g : WithConv (H →ₐ[R] ↑A)) : (π.normalizerHopfIdeal hπ).toIdeal ≤ RingHom.ker g.ofConv ↔ g ∈ π.universalNormalizerPoints A

A point annihilates the normalizer ideal exactly when it normalizes the subgroup universally.

@[simp]

theorem BialgHom.quotientPointsSubgroup_normalizerHopfIdeal {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) (A : CommAlgCat R) : TauCeti.CommHopfAlgCat.quotientPointsSubgroup (↧H) (π.normalizerHopfIdeal hπ) A = π.universalNormalizerPoints A

The closed subgroup represented by the normalizer ideal has exactly the universal normalizer points over every commutative value algebra.

theorem BialgHom.normalizerHopfIdeal_le_kerOfSurjective {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) : π.normalizerHopfIdeal hπ ≤ TauCeti.HopfIdeal.kerOfSurjective π hπ

The normalizer contains the original closed diagonalizable subgroup. The order on defining ideals reverses the inclusion of closed subgroup schemes.