The centralizer of a diagonalizable subgroup

Let G = Spec H be an affine group scheme over a commutative ring R and let D(X) → G be a closed diagonalizable subgroup, given by a surjective morphism π : H →ₐc[R] R[X] of coordinate Hopf algebras for a commutative group X of characters. This file constructs the centralizer Z_G(D(X)) as a closed subgroup scheme of G, that is, as a Hopf ideal of H.

The defining equations are the coefficients, in the basis of R[X] indexed by characters, of the conjugation defect of a coordinate x: the difference between the universal conjugate of the universal point of D(X) by the universal point of G and that point itself, written in the coordinates H ⊗[R] R[X]. A point of G with values in an algebra A kills these coefficients exactly when it commutes with every point of D(X) after every extension of A; since such points form a subgroup, the coefficient ideal is a Hopf ideal. The construction needs no basis of H, only the canonical basis of the monoid algebra R[X], and no hypothesis on R.

The rational points of the centralizer are the rational points of G whose conjugation fixes the coordinate map π. Every such point normalizes D(X), and, when the base has connected prime spectrum, the rational points of the centralizer are exactly the normalizing points acting trivially on the character group X, that is, the kernel of BialgHom.normalizerCharacterHom.

Since D(X) is commutative, it lies in its own centralizer; and the centralizer is the whole group exactly when D(X) is a central closed subgroup of G.

A homomorphism D(Y) → D(X) with coordinate map ψ : R[X] → R[Y] makes ψ ∘ π the coordinate map of the composite D(Y) → D(X) → G. The centralizer of this composite contains that of D(X), and contains D(X) itself. The main instance is the common kernel D(X ⧸ S) → D(X) of a subgroup S of characters, with ψ induced by the quotient map.

Main declarations

• BialgHom.centralizerDefect: the conjugation defect of a coordinate, in H ⊗[R] R[X].
• BialgHom.centralizerCoefficient: its coefficient at a character; centralizerDefect_def and centralizerCoefficient_def are the public formulas for these two definitions.
• BialgHom.centralizerHopfIdeal: the Hopf ideal cutting out the centralizer of the diagonalizable subgroup.
• BialgHom.centralizerHopfIdeal_toIdeal_fg: the centralizer ideal is finitely generated when H is of finite type, over any base ring.
• BialgHom.centralizerHopfIdeal_le_ker_iff: an algebra-valued point kills the centralizer ideal exactly when it commutes with every point of the diagonalizable subgroup over every extension of its value algebra.
• BialgHom.mem_centralizerPointsSubgroup_iff: the same statement for the subgroup of points cut out by the centralizer ideal.
• BialgHom.centralizerHopfIdeal_le_ker_iff_comp_pointConjugationAlgHom_eq: a rational point lies in the centralizer exactly when conjugation by it fixes the coordinate map π.
• BialgHom.normalizerCharacterHom_eq_one_iff_centralizerHopfIdeal_le_ker: the rational points of the centralizer are the kernel of the normalizer action on characters.
• BialgHom.ker_normalizerCharacterHom: the same statement as an equality of subgroups of the rational normalizer.
• BialgHom.centralizerHopfIdeal_le_kerOfSurjective: the diagonalizable subgroup lies in its own centralizer.
• BialgHom.centralizerHopfIdeal_eq_bot_iff_isCentral: the centralizer is the whole group exactly when the diagonalizable subgroup is central.
• BialgHom.centralizerHopfIdeal_comp_le: the centralizer of a composite D(Y) → D(X) → G contains the centralizer of D(X).
• BialgHom.centralizerHopfIdeal_mapDomainBialgHom_comp_eq_of_leftInverse: a split injection of character groups preserves the centralizer.
• BialgHom.centralizerHopfIdeal_comp_le_kerOfSurjective: the centralizer of a composite D(Y) → D(X) → G contains D(X).
• BialgHom.centralizerHopfIdeal_mapDomainBialgHom_mk'_comp_anti: the centralizer of the common kernel D(X ⧸ S) of a subgroup S of characters grows with S.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 1 (normalizers and centralizers), §12 (diagonalizable groups) and §13 (tori acting on schemes).
• SGA 3, Exposé VI_B, Corollaire 6.2.5 (i), and Exposé XI, Corollaire 5.3.

The conjugation defect and its coefficients

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

The conjugation defect of a coordinate x: in the coordinates H ⊗[R] R[X] of G × D(X), the difference between the conjugate of the universal point of D(X) by the universal point of G and the universal point of D(X) itself. The first tensor factor is the conjugating variable of G, the second the conjugated variable of D(X).

theorem BialgHom.centralizerDefect_def {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (x : H) : π.centralizerDefect x = (Algebra.TensorProduct.map (AlgHom.id R H) ↑π) (TauCeti.HopfAlgebra.conjugationAlgHom x) - 1 ⊗ₜ[R] π x

The defining formula of the conjugation defect. This is the public interface to the definition, whose body is not exposed outside this module.

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

The coefficient of the conjugation defect of x at the character χ, in the canonical basis of R[X]. These coefficients generate the centralizer ideal.

theorem BialgHom.centralizerCoefficient_def {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (x : H) (χ : X) : π.centralizerCoefficient x χ = (LinearMap.tensorComponent (TauCeti.Comodule.monoidCoeff R X χ)) (π.centralizerDefect x)

The defining formula of a coefficient of the conjugation defect. This is the public interface to the definition, whose body is not exposed outside this module.

theorem BialgHom.map_centralizerDefect_eq_zero_iff {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 : Type x} [AddCommMonoid A] [Module R A] (f : H →ₗ[R] A) (x : H) : (TensorProduct.map f LinearMap.id) (π.centralizerDefect x) = 0 ↔ ∀ (χ : X), f (π.centralizerCoefficient x χ) = 0

A linear map out of H kills every coefficient of a conjugation defect exactly when it kills the defect itself, after tensoring with the identity of R[X].

theorem BialgHom.apply_map_centralizerDefect {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 : Type x} {B : Type y} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (g : WithConv (H →ₐ[R] A)) (ψ : TensorProduct R A (MonoidAlgebra R X) →ₐ[R] B) (x : H) : ψ ((Algebra.TensorProduct.map g.ofConv (AlgHom.id R (MonoidAlgebra R X))) (π.centralizerDefect x)) = ((ψ.comp Algebra.TensorProduct.includeLeft).mapValue g * π.mapDomain (WithConv.toConv (ψ.comp Algebra.TensorProduct.includeRight)) * ((ψ.comp Algebra.TensorProduct.includeLeft).mapValue g)⁻¹).ofConv x - (π.mapDomain (WithConv.toConv (ψ.comp Algebra.TensorProduct.includeRight))).ofConv x

Evaluating the conjugation defect at a point g of G and then along an algebra map ψ out of the tensor square computes g' t g'⁻¹ - t, where g' is g pushed along ψ and t is the point of D(X) carried by ψ.

The centralizer as a closed subgroup scheme

noncomputable def BialgHom.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) : TauCeti.HopfIdeal R H

The centralizer of a diagonalizable subgroup, as a Hopf ideal. Its quotient represents the points of G commuting with every point of D(X). The ideal is generated by the coefficients of the conjugation defects; it is a Hopf ideal because the points killing it form a subgroup over every value algebra.

theorem BialgHom.centralizerHopfIdeal_toIdeal {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 = Ideal.span (Set.range fun (p : H × X) => π.centralizerCoefficient p.1 p.2)

The centralizer ideal is generated by the coefficients of the conjugation defects.

theorem BialgHom.centralizerHopfIdeal_toIdeal_fg {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.FiniteType R H] : π.centralizerHopfIdeal.toIdeal.FG

The centralizer ideal is finitely generated when H is of finite type, over any base ring: the coefficients of the conjugation defects of finitely many algebra generators of H already generate it.

theorem BialgHom.centralizerHopfIdeal_le_ker_iff_commute_of_injective {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 : Type x} {B : Type y} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (g : WithConv (H →ₐ[R] A)) (ψ : TensorProduct R A (MonoidAlgebra R X) →ₐ[R] B) (hψ : Function.Injective ⇑ψ) : π.centralizerHopfIdeal.toIdeal ≤ RingHom.ker g.ofConv ↔ Commute ((ψ.comp Algebra.TensorProduct.includeLeft).mapValue g) (π.mapDomain (WithConv.toConv (ψ.comp Algebra.TensorProduct.includeRight)))

A point of G kills the centralizer ideal exactly when it commutes with the point of D(X) carried by any injective algebra map ψ out of A ⊗[R] R[X]. The identity of A ⊗[R] R[X] carries the universal point of D(X); the left unitor R ⊗[R] R[X] ≃ R[X] is used for rational points.

theorem BialgHom.commute_mapValue_mapDomain_of_centralizerHopfIdeal_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) {A : Type x} {B : Type y} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {g : WithConv (H →ₐ[R] A)} (hg : π.centralizerHopfIdeal.toIdeal ≤ RingHom.ker g.ofConv) (φ : A →ₐ[R] B) (t : WithConv (MonoidAlgebra R X →ₐ[R] B)) : Commute (φ.mapValue g) (π.mapDomain t)

A point of G killing the centralizer ideal commutes with every point of D(X) over every extension of its value algebra.

theorem BialgHom.centralizerHopfIdeal_le_ker_iff {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 : Type x} [CommRing A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : π.centralizerHopfIdeal.toIdeal ≤ RingHom.ker g.ofConv ↔ ∀ ⦃B : Type (max u w x)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (φ : A →ₐ[R] B) (t : WithConv (MonoidAlgebra R X →ₐ[R] B)), Commute (φ.mapValue g) (π.mapDomain t)

A point of G kills the centralizer ideal exactly when it commutes with every point of D(X) over every extension of its value algebra. Quantifying over extensions is what makes the condition functorial: the universal extension A ⊗[R] R[X] carries the universal point of D(X).

@[reducible, inline]

noncomputable abbrev BialgHom.centralizerPointsSubgroup {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 : CommAlgCat R) : Subgroup (WithConv (H →ₐ[R] ↑A))

The subgroup of A-valued points of G cut out by the centralizer ideal.

theorem BialgHom.mem_centralizerPointsSubgroup_iff {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 : CommAlgCat R) (g : WithConv (H →ₐ[R] ↑A)) : g ∈ π.centralizerPointsSubgroup A ↔ ∀ ⦃B : Type (max u w x)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (φ : ↑A →ₐ[R] B) (t : WithConv (MonoidAlgebra R X →ₐ[R] B)), Commute (φ.mapValue g) (π.mapDomain t)

The points of the centralizer are the points of G commuting with every point of D(X) over every extension of the value algebra.

Rational points

theorem BialgHom.centralizerHopfIdeal_le_ker_iff_comp_pointConjugationAlgHom_eq {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) (g : WithConv (H →ₐ[R] R)) : π.centralizerHopfIdeal.toIdeal ≤ RingHom.ker g.ofConv ↔ (↑π).comp (TauCeti.HopfAlgebra.pointConjugationAlgHom g) = ↑π

A rational point lies in the centralizer exactly when conjugation by it fixes the coordinate map of the diagonalizable subgroup.

theorem BialgHom.mem_normalizerPoints_of_centralizerHopfIdeal_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) (hπ : Function.Surjective ⇑π) {g : WithConv (H →ₐ[R] R)} (hg : π.centralizerHopfIdeal.toIdeal ≤ RingHom.ker g.ofConv) : g ∈ π.normalizerPoints hπ

A rational point of the centralizer normalizes the diagonalizable subgroup.

theorem BialgHom.normalizerCharacterHom_eq_one_iff_centralizerHopfIdeal_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) [ConnectedSpace (PrimeSpectrum R)] (hπ : Function.Surjective ⇑π) (g : ↥(π.normalizerPoints hπ)) : (π.normalizerCharacterHom hπ) g = 1 ↔ π.centralizerHopfIdeal.toIdeal ≤ RingHom.ker (↑g).ofConv

The rational points of the centralizer are the normalizing points acting trivially on the character group: the kernel of BialgHom.normalizerCharacterHom.

theorem BialgHom.ker_normalizerCharacterHom {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) [ConnectedSpace (PrimeSpectrum R)] (hπ : Function.Surjective ⇑π) : (π.normalizerCharacterHom hπ).ker = (π.centralizerPointsSubgroup ↧R).subgroupOf (π.normalizerPoints hπ)

The kernel of the normalizer action on characters is the rational centralizer of the diagonalizable subgroup scheme.

instance BialgHom.normal_centralizerPointsSubgroup_subgroupOf_normalizerPoints {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) [ConnectedSpace (PrimeSpectrum R)] (hπ : Function.Surjective ⇑π) : ((π.centralizerPointsSubgroup ↧R).subgroupOf (π.normalizerPoints hπ)).Normal

The rational centralizer is normal in the rational normalizer, being the kernel of its action on characters.

Comparison with the diagonalizable subgroup

theorem BialgHom.centralizerHopfIdeal_le_kerOfSurjective {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π : Function.Surjective ⇑π) : π.centralizerHopfIdeal ≤ TauCeti.HopfIdeal.kerOfSurjective π hπ

A diagonalizable subgroup lies in its own centralizer, being commutative.

theorem BialgHom.centralizerHopfIdeal_eq_bot_iff_isCentral {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π : Function.Surjective ⇑π) : π.centralizerHopfIdeal = ⊥ ↔ (TauCeti.HopfIdeal.kerOfSurjective π hπ).IsCentral

The centralizer is the whole group exactly when the diagonalizable subgroup is central.

Composites D(Y) → D(X) → G

theorem BialgHom.centralizerHopfIdeal_comp_le {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {Y : Type u_1} [CommGroup Y] (ψ : MonoidAlgebra R X →ₐc[R] MonoidAlgebra R Y) : (ψ.comp π).centralizerHopfIdeal ≤ π.centralizerHopfIdeal

A smaller diagonalizable subgroup has a larger centralizer. If D(Y) → G factors through D(X) → G along the homomorphism D(Y) → D(X) with coordinate map ψ, then every point of G centralizing D(X) centralizes D(Y).

theorem BialgHom.centralizerHopfIdeal_mapDomainBialgHom_comp_eq_of_leftInverse {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {Y : Type u_1} [CommGroup Y] (f : X →* Y) (g : Y →* X) (hgf : g.comp f = MonoidHom.id X) : ((MonoidAlgebra.mapDomainBialgHom R f).comp π).centralizerHopfIdeal = π.centralizerHopfIdeal

A split injective map of character groups does not change the centralizer of a composite diagonalizable subgroup.

theorem BialgHom.centralizerHopfIdeal_comp_le_kerOfSurjective {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {Y : Type u_1} [CommGroup Y] (hπ : Function.Surjective ⇑π) (ψ : MonoidAlgebra R X →ₐc[R] MonoidAlgebra R Y) : (ψ.comp π).centralizerHopfIdeal ≤ TauCeti.HopfIdeal.kerOfSurjective π hπ

The diagonalizable subgroup D(X) lies in the centralizer of any composite D(Y) → D(X) → G, being commutative.

theorem BialgHom.centralizerHopfIdeal_mapDomainBialgHom_mk'_comp_anti {R : Type u} {H : Type v} {X : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [CommGroup X] (π : H →ₐc[R] MonoidAlgebra R X) {S S' : Subgroup X} (h : S ≤ S') : ((MonoidAlgebra.mapDomainBialgHom R (QuotientGroup.mk' S')).comp π).centralizerHopfIdeal ≤ ((MonoidAlgebra.mapDomainBialgHom R (QuotientGroup.mk' S)).comp π).centralizerHopfIdeal

The centralizer of the diagonalizable subgroup D(X ⧸ S) of D(X), the common kernel of the characters in S, grows with S.