The centralizer and the diagonalizable subgroup are normal in the normalizer

Let G = Spec H be an affine group scheme over a commutative ring R and D(X) → G a closed diagonalizable subgroup with surjective coordinate map π : H →ₐc[R] R[X]. The normalizer N_G(D(X)) is cut out by BialgHom.normalizerHopfIdeal π hπ, and the centralizer Z_G(D(X)) by BialgHom.centralizerHopfIdeal π. This file shows that Z_G(D(X)) is a closed subgroup of N_G(D(X)), that both D(X) and Z_G(D(X)) are normal in N_G(D(X)), and that the normalizer is the whole group exactly when D(X) is normal in G.

A closed subgroup of N_G(D(X)) is cut out by the image, in the quotient Hopf algebra H ⧸ normalizerHopfIdeal π hπ, of the Hopf ideal of H cutting it out in G. It is normal as soon as the points of the normalizer, which are the points normalizing D(X) after every extension of the value algebra, normalize its points in G. For D(X) this is the definition of the normalizer. For Z_G(D(X)), conjugating a point commuting with every point of D(X) by a point normalizing D(X) yields another such point.

Main declarations

• BialgHom.normalizerHopfIdeal_le_centralizerHopfIdeal: the centralizer of the diagonalizable subgroup is contained in its normalizer.
• BialgHom.isNormal_map_kerOfSurjective_mkBialgHom_normalizerHopfIdeal: the diagonalizable subgroup is normal in its normalizer.
• BialgHom.isNormal_map_centralizerHopfIdeal_mkBialgHom_normalizerHopfIdeal: the centralizer of the diagonalizable subgroup is normal in the normalizer.
• BialgHom.normalizerHopfIdeal_eq_bot_iff_isNormal: the normalizer is the whole group exactly when the diagonalizable subgroup is normal.

References

• SGA 3, Exposé XI, Proposition 5.9.
• J. S. Milne, Algebraic Groups (2017), §12 and §13.b.

theorem BialgHom.normalizerHopfIdeal_le_centralizerHopfIdeal {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π ≤ π.centralizerHopfIdeal

The centralizer of a diagonalizable subgroup is contained in its normalizer. The order on defining ideals reverses the inclusion of closed subgroup schemes.

theorem BialgHom.isNormal_map_kerOfSurjective_mkBialgHom_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.kerOfSurjective π hπ).map (Bialgebra.Quotient.mkBialgHom (π.normalizerHopfIdeal hπ).toIdeal)).IsNormal

The diagonalizable subgroup is normal in its normalizer.

theorem BialgHom.isNormal_map_centralizerHopfIdeal_mkBialgHom_normalizerHopfIdeal {R H X : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (hπ : Function.Surjective ⇑π) : (π.centralizerHopfIdeal.map (Bialgebra.Quotient.mkBialgHom (π.normalizerHopfIdeal hπ).toIdeal)).IsNormal

The centralizer of a diagonalizable subgroup is normal in the normalizer.

theorem BialgHom.normalizerHopfIdeal_eq_bot_iff_isNormal {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π).IsNormal

The normalizer is the whole group exactly when the diagonalizable subgroup is normal.