Smoothness of centralizers of diagonalizable subgroups

Let G = Spec H be an affine group scheme over a commutative ring R and let π : H →ₐc[R] R[X] present a homomorphism D(X) → G from the diagonalizable group of a commutative group X. This file proves that the centralizer Z_G(D(X)) is formally smooth whenever G is, and hence smooth when G is a smooth affine group of finite type, over any base ring.

The proof identifies the centralizer with a fixed-point subscheme. The group D(X) acts on G by conjugation, (g, t) ↦ π(t) g π(t)⁻¹, which makes H a comodule algebra over R[X] (BialgHom.conjugationComoduleAlgebra). Its fixed points are exactly the points of G commuting with D(X), so the centralizer ideal is the fixed-point ideal of this action (BialgHom.centralizerHopfIdeal_toIdeal_eq_fixedPointIdeal). The fixed-point subscheme of a formally smooth affine scheme under a diagonalizable action is formally smooth (TauCeti.ComoduleAlgebra.formallySmooth_quotient_fixedPointIdeal).

No reductivity, connectedness, finite-type or field hypothesis is used, and π need not be injective on points. The statement applies in particular to the centralizer of a maximal torus and to the centralizer of the kernel of a root, and recovers smoothness of the dynamic Levi subgroup Z_G(λ) of a cocharacter, which is the centralizer of its image.

Main declarations

• BialgHom.conjugationCoactAlgHom: the coordinate map of the conjugation action of D(X) on G.
• BialgHom.conjugationComoduleAlgebra: the conjugation action as a comodule algebra structure on H over R[X].
• BialgHom.centralizerHopfIdeal_toIdeal_eq_fixedPointIdeal: the centralizer is the fixed-point subscheme of the conjugation action.
• BialgHom.formallySmooth_quotient_centralizerHopfIdeal: the centralizer of a diagonalizable subgroup of a formally smooth affine group is formally smooth.
• BialgHom.smoothCommHopfAlgProperty_quotient_centralizerHopfIdeal: the centralizer of a diagonalizable subgroup of a smooth affine group of finite type is smooth.

References

• SGA 3, Exposé XI, Corollaire 5.3.
• B. Conrad, O. Gabber, G. Prasad, Pseudo-reductive Groups, Proposition A.8.10(2).
• J. S. Milne, Algebraic Groups (2017), Theorem 13.1.

The conjugation action of D(X) on G

noncomputable def BialgHom.conjugationCoactAlgHom {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) : H →ₐ[R] TensorProduct R H (MonoidAlgebra R X)

The coordinate map H → H ⊗[R] R[X] of the conjugation action (g, t) ↦ π(t) g π(t)⁻¹ of the diagonalizable group D(X) on G. The first tensor factor is the acted-on variable of G, the second the acting variable of D(X).

theorem BialgHom.comp_conjugationCoactAlgHom {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {B : Type x} [CommRing B] [Algebra R B] (ψ : TensorProduct R H (MonoidAlgebra R X) →ₐ[R] B) : ψ.comp π.conjugationCoactAlgHom = (π.mapDomain (WithConv.toConv (ψ.comp Algebra.TensorProduct.includeRight)) * WithConv.toConv (ψ.comp Algebra.TensorProduct.includeLeft) * (π.mapDomain (WithConv.toConv (ψ.comp Algebra.TensorProduct.includeRight)))⁻¹).ofConv

Evaluation of the conjugation action against an arbitrary algebra map out of H ⊗[R] R[X]: it conjugates the restriction to H by the image in G of the restriction to R[X].

@[implicit_reducible]

noncomputable def BialgHom.conjugationComoduleAlgebra {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) : TauCeti.ComoduleAlgebra R (MonoidAlgebra R X) H

The conjugation action of D(X) on G, as a comodule algebra structure on H over R[X]. Its coaction is BialgHom.conjugationCoactAlgHom.

theorem BialgHom.conjugationComoduleAlgebra_coact_apply {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (a : H) : TauCeti.Comodule.coact a = π.conjugationCoactAlgHom a

The coaction of the conjugation comodule algebra is the conjugation action.

The centralizer as a fixed-point subscheme

theorem BialgHom.centralizerHopfIdeal_le_ker_iff_fixedPointIdeal_le_ker {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {B : Type x} [CommRing B] [Algebra R B] (q : H →ₐ[R] B) : π.centralizerHopfIdeal.toIdeal ≤ RingHom.ker q ↔ TauCeti.Comodule.fixedPointIdeal R X H ≤ RingHom.ker q

A point of G lies in the centralizer exactly when it is a fixed point of the conjugation action of D(X).

theorem BialgHom.centralizerHopfIdeal_toIdeal_eq_fixedPointIdeal {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) : π.centralizerHopfIdeal.toIdeal = TauCeti.Comodule.fixedPointIdeal R X H

The centralizer of a diagonalizable subgroup is the fixed-point subscheme of its conjugation action.

Smoothness

instance BialgHom.formallySmooth_quotient_centralizerHopfIdeal {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) [Algebra.FormallySmooth R H] : Algebra.FormallySmooth R (H ⧸ π.centralizerHopfIdeal.toIdeal)

The centralizer of a diagonalizable subgroup of a formally smooth affine group is formally smooth. No finite-type, field, connectedness or reductivity hypothesis is needed.

theorem BialgHom.smoothCommHopfAlgProperty_quotient_centralizerHopfIdeal {R : Type u} {X : Type w} [CommRing R] [CommGroup X] {H : TauCeti.FiniteTypeCommHopfAlgCat R} [Algebra.Smooth R ↑H.obj] (π : ↑H.obj →ₐc[R] MonoidAlgebra R X) : TauCeti.smoothCommHopfAlgProperty R (H.quotient π.centralizerHopfIdeal).obj

The centralizer of a diagonalizable subgroup of a smooth affine group of finite type is smooth, over any base ring.