The centralizer of a Lie algebra element

Let G = Spec H be an affine group over a field k whose Lie algebra 𝔤 is finite-dimensional. The centralizer C_G(x) of x ∈ 𝔤 is the stabilizer of x under the adjoint representation: the closed subgroup whose points fix x under Ad. Its points with values in any commutative k-algebra are the points whose adjoint action fixes the constant extension of x, so this is the scheme-theoretic centralizer.

The main result identifies its Lie algebra with the kernel of ad x (TauCeti.lieSubalgebra_centralizerHopfIdeal). The proof differentiates the adjoint representation, whose differential is the adjoint action of 𝔤 on itself. No smoothness, connectedness or characteristic assumption is needed. For a connected group over an algebraically closed field of characteristic zero, the centralizer is the whole group exactly when x is central in 𝔤.

Over a field of characteristic zero the centralizer is smooth, by Cartier's theorem, so its dimension is dim ker (ad x) (TauCeti.ringKrullDim_quotient_centralizerHopfIdeal). By rank and nullity, dim G = dim C_G(x) + dim [𝔤, x] (TauCeti.ringKrullDim_quotient_centralizerHopfIdeal_add_finrank_range_ad). Since [𝔤, x] is the tangent space at x to the adjoint orbit of x, this is the infinitesimal form of the orbit dimension formula dim (G • x) = dim G - dim C_G(x).

The Lie algebra 𝔤 is modelled as the dual of the augmentation cotangent space, which carries the adjoint comodule; Derivation.cotangentDualLieEquiv identifies it with the counit-valued derivations, where closed subgroups have their Lie subalgebras.

Main declarations

• TauCeti.centralizerHopfIdeal: the Hopf ideal of the centralizer of x ∈ 𝔤.
• TauCeti.centralizerHopfIdeal_le_ker_iff: its algebra-valued points are the points whose adjoint action fixes x.
• TauCeti.mem_quotientPointsSubgroup_centralizerHopfIdeal_iff: a base-field point lies in the centralizer exactly when its adjoint Lie automorphism fixes x.
• TauCeti.mem_lieSubalgebra_centralizerHopfIdeal_iff and TauCeti.lieSubalgebra_centralizerHopfIdeal: its Lie algebra is the kernel of ad x.
• TauCeti.centralizerHopfIdeal_eq_bot_iff_mem_center: for a connected group over an algebraically closed field of characteristic zero, the centralizer is the whole group exactly when x is central.
• TauCeti.ringKrullDim_quotient_centralizerHopfIdeal and TauCeti.ringKrullDim_quotient_centralizerHopfIdeal_add_finrank_range_ad: in characteristic zero, dim C_G(x) = dim ker (ad x) and dim G = dim C_G(x) + rank (ad x).

References

• J. S. Milne, Algebraic Groups (2017), Chapter 10, in particular the Lie algebra of a stabilizer.
• J. E. Humphreys, Linear Algebraic Groups, §13.
• D. H. Collingwood and W. M. McGovern, Nilpotent Orbits in Semisimple Lie Algebras, Van Nostrand Reinhold, 1993, §1.3, for centralizers of elements of 𝔤.

noncomputable def TauCeti.centralizerHopfIdeal {k : Type u} [Field k] (H : Type u) [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) : HopfIdeal k H

The Hopf ideal of the centralizer of an element x of the Lie algebra, the stabilizer of x under the adjoint representation. Contravariantly, it cuts out the closed subgroup of Spec H fixing x under Ad.

theorem TauCeti.centralizerHopfIdeal_def {k : Type u} [Field k] (H : Type u) [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) : centralizerHopfIdeal H x = Comodule.stabilizerHopfIdeal k H x

The centralizer of x is the stabilizer of x under the adjoint comodule. Rewriting with this transfers the defining equations and universal property of Comodule.stabilizerHopfIdeal.

theorem TauCeti.centralizerHopfIdeal_le_ker_iff {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) {A : Type u} [CommRing A] [Algebra k A] (g : WithConv (H →ₐ[k] A)) : (centralizerHopfIdeal H x).toIdeal ≤ RingHom.ker g.ofConv ↔ Derivation.adDerivation A ((Derivation.pointInCounitAlgebra A) g) ((Derivation.mapValue (Algebra.ofId k A)) (Derivation.cotangentLinearEquiv x)) = (Derivation.mapValue (Algebra.ofId k A)) (Derivation.cotangentLinearEquiv x)

An algebra-valued point lies in the centralizer of x exactly when its adjoint action fixes the constant extension of x. The value algebra may be nonreduced.

theorem TauCeti.mem_quotientPointsSubgroup_centralizerHopfIdeal_iff {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) (g : ↑(HopfAlgebra.points ↧k)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (centralizerHopfIdeal H x) ↧k ↔ Derivation.cotangentDualLieEquiv.symm ((Derivation.adDerivationLieEquiv k ((Derivation.pointInCounitAlgebra ↑↧k) g)) (Derivation.cotangentDualLieEquiv x)) = x

A base-field point lies in the centralizer exactly when its adjoint Lie automorphism, transported through the cotangent-dual identification, fixes x.

theorem TauCeti.centralizerHopfIdeal_le_ker_iff_adjointAction {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) (A : CommAlgCat k) (g : WithConv (H →ₐ[k] ↑A)) : (centralizerHopfIdeal H x).toIdeal ≤ RingHom.ker g.ofConv ↔ ↑((CategoryTheory.ConcreteCategory.hom (Derivation.adjointAction A)) g) (1 ⊗ₜ[k] x) = 1 ⊗ₜ[k] x

An algebra-valued point centralizes x precisely when its adjoint action fixes 1 ⊗ x. This criterion retains the equations over nonreduced coefficient algebras.

theorem TauCeti.centralizerHopfIdeal_eq_bot_iff {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) : centralizerHopfIdeal H x = ⊥ ↔ Comodule.coact x = x ⊗ₜ[k] 1

The centralizer of x is the whole group exactly when x is fixed by the adjoint coaction.

@[simp]

theorem TauCeti.centralizerHopfIdeal_zero {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] : centralizerHopfIdeal H 0 = ⊥

The centralizer of 0 is the whole group.

theorem TauCeti.mem_lieSubalgebra_centralizerHopfIdeal_iff {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) (d : Derivation k H (Bialgebra.CounitAlgebra k H k)) : d ∈ (centralizerHopfIdeal H x).lieSubalgebra ↔ ⁅Derivation.cotangentDualLieEquiv x, d⁆ = 0

A tangent vector lies in the Lie algebra of the centralizer of x exactly when it commutes with x.

theorem TauCeti.lieSubalgebra_centralizerHopfIdeal {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) : (centralizerHopfIdeal H x).lieSubalgebra.toSubmodule = LinearMap.ker ((LieAlgebra.ad k (Derivation k H (Bialgebra.CounitAlgebra k H k))) (Derivation.cotangentDualLieEquiv x))

The Lie algebra of a centralizer. The Lie algebra of the centralizer of x is the kernel of ad x.

theorem TauCeti.cotangentDualLieEquiv_mem_lieSubalgebra_centralizerHopfIdeal {k : Type u} [Field k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Module.Finite k (Bialgebra.CotangentSpace k H)] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) : Derivation.cotangentDualLieEquiv x ∈ (centralizerHopfIdeal H x).lieSubalgebra

An element of the Lie algebra lies in the Lie algebra of its own centralizer.

theorem TauCeti.centralizerHopfIdeal_eq_bot_iff_mem_center {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] (x : Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj)) : centralizerHopfIdeal (↑H.obj) x = ⊥ ↔ x ∈ LieAlgebra.center k (Module.Dual k (Bialgebra.CotangentSpace k ↑H.obj))

For a connected affine group over an algebraically closed field of characteristic zero, the centralizer of x is the whole group exactly when x is central in the Lie algebra.

theorem TauCeti.ringKrullDim_quotient_centralizerHopfIdeal {k : Type u} [Field k] [CharZero k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) : ringKrullDim (H ⧸ (centralizerHopfIdeal H x).toIdeal) = ↑(Module.finrank k ↥(LinearMap.ker ((LieAlgebra.ad k (Module.Dual k (Bialgebra.CotangentSpace k H))) x)))

The dimension of a centralizer. Over a field of characteristic zero, the centralizer C_G(x) of an element x of the Lie algebra of a finite-type affine group G has dimension dim ker (ad x).

theorem TauCeti.ringKrullDim_quotient_centralizerHopfIdeal_add_finrank_range_ad {k : Type u} [Field k] [CharZero k] {H : Type u} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (x : Module.Dual k (Bialgebra.CotangentSpace k H)) : ringKrullDim (H ⧸ (centralizerHopfIdeal H x).toIdeal) + ↑(Module.finrank k ↥(LinearMap.range ((LieAlgebra.ad k (Module.Dual k (Bialgebra.CotangentSpace k H))) x))) = ringKrullDim H

The dimension of a centralizer and of [𝔤, x]. Over a field of characteristic zero, the dimension of a finite-type affine group G is the dimension of the centralizer C_G(x) of an element x of its Lie algebra 𝔤 plus the rank of ad x, the dimension of [𝔤, x].