Weight spaces of the adjoint representation

Let G = Spec H be an affine group scheme over R whose augmentation cotangent space is finite projective, so that its Lie algebra is the single R-module Module.Dual R (Bialgebra.CotangentSpace R H) carrying the adjoint comodule of TauCeti.Algebra.AlgebraicGroup.Tangent.Representation. Let π : H →ₐc[R] R[M] be a morphism of coordinate bialgebras, that is, a homomorphism D(M) → G of affine group schemes out of the diagonalizable group on a commutative group M written multiplicatively.

Restricting the adjoint representation along π decomposes the Lie algebra into weight submodules, indexed by M. This file names them: adjointWeightSpace π α is the α-weight submodule 𝔤_α, nontrivialAdjointWeights π is the set of nontrivial characters whose weight submodule is nonzero, and the Lie algebra is spanned by 𝔤_1 together with the 𝔤_α for α ∈ nontrivialAdjointWeights π. A point of D(M) acts on 𝔤_α by the value of α at that point, and the Lie bracket sends 𝔤_α × 𝔤_β into 𝔤_{αβ}.

Nothing here asserts that π is a closed immersion, that D(M) is a torus, let alone a maximal one, or that G is reductive. When π does exhibit a split maximal torus T in a reductive G, nontrivialAdjointWeights π is the set of roots of the split pair (G, T).

Main definitions

• Derivation.adjointWeightSpace: the α-weight submodule 𝔤_α of the Lie algebra of G under a homomorphism from a diagonalizable group.
• Derivation.nontrivialAdjointWeights: the nontrivial characters whose adjoint weight submodule is nonzero.

Main results

• Derivation.isInternal_adjointWeightSpace: the Lie algebra of G is the internal direct sum of its weight submodules.
• Derivation.sup_iSup_adjointWeightSpace_eq_top: the trivial weight submodule together with the submodules indexed by nontrivialAdjointWeights π exhaust the Lie algebra.
• Derivation.finite_nontrivialAdjointWeights: the set of nontrivial adjoint weights is finite.
• Derivation.endOfPoint_tmul_of_mem_adjointWeightSpace: a point of D(M) acts on the α-weight submodule by the value of α at that point.
• Derivation.mem_adjointWeightSpace_iff_universalPointAction: weight-space membership can be tested using the universal point of D(M).
• Derivation.lie_mem_adjointWeightSpace_mul: the adjoint weight decomposition is a Lie grading: [𝔤_α, 𝔤_β] ⊆ 𝔤_{αβ}.

Roadmap

Layer 7 of TauCetiRoadmap/ReductiveGroups/README.md asks for the root datum (X*(T), Φ, X_*(T), Φ^∨) of a split pair (G, T), taking the split case first. The character and cocharacter lattices with their pairing are already in TauCeti.Algebra.AlgebraicGroup.Cocharacter; this file supplies the weight decomposition that Φ is read off, the remaining piece of the root datum that comes from the group rather than the torus. Layer 9's split reductive group schemes over ℤ take the split maximal torus as part of their data and are defined by conditions on exactly this decomposition, and milestone L0 of TauCetiRoadmap/CFSGStatement/README.md consumes those pinned Chevalley--Demazure groups.

References

• J. S. Milne, Algebraic Groups (2017), §21.1 (the roots of a split reductive group).
• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2.
• B. Conrad, Reductive Group Schemes (SGA3 exposition), §3.2.

noncomputable def Derivation.adjointWeightSpace {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] (π : H →ₐc[R] MonoidAlgebra R M) (α : M) : Submodule R (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))

The α-weight submodule 𝔤_α of the Lie algebra of G = Spec H under a homomorphism D(M) → G with coordinate morphism π: the part of the Lie algebra on which D(M) acts through the character α.

Equations

• Derivation.adjointWeightSpace π α = TauCeti.DiagonalizableGroup.weightSpace (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) (↑π) α

@[simp]

theorem Derivation.mem_adjointWeightSpace {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] {π : H →ₐc[R] MonoidAlgebra R M} {α : M} {x : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)} : x ∈ adjointWeightSpace π α ↔ (TensorProduct.map LinearMap.id (↑π).toLinearMap) (TauCeti.Comodule.coact x) = x ⊗ₜ[R] MonoidAlgebra.single α 1

Membership in the α-weight submodule, in terms of the adjoint coaction: pushing the adjoint coaction of x through π must give x ⊗ α.

theorem Derivation.mem_adjointWeightSpace_iff_universalPointAction {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type u} [CommGroup M] (pi : H →ₐc[R] MonoidAlgebra R M) (alpha : M) (x : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) : x ∈ adjointWeightSpace pi alpha ↔ ↑((CategoryTheory.ConcreteCategory.hom (adjointAction (CommAlgCat.of R (MonoidAlgebra R M)))) (WithConv.toConv ↑pi)) (1 ⊗ₜ[R] x) = MonoidAlgebra.single alpha 1 ⊗ₜ[R] x

Membership in an adjoint weight space can be tested on the universal point of the diagonalizable group. The universal point acts on a weight vector of weight alpha by the group-algebra basis element [alpha].

This is the converse to endOfPoint_tmul_of_mem_adjointWeightSpace at the universal point.

theorem Derivation.isInternal_adjointWeightSpace {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] (π : H →ₐc[R] MonoidAlgebra R M) : DirectSum.IsInternal (adjointWeightSpace π)

The Lie algebra of G is the internal direct sum of its weight submodules under a homomorphism from a diagonalizable group.

def Derivation.nontrivialAdjointWeights {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] (π : H →ₐc[R] MonoidAlgebra R M) : Set M

The nontrivial characters of D(M) whose adjoint weight submodule in the Lie algebra of G is nonzero. When π exhibits a split maximal torus T in a reductive G, these are the roots of the split pair (G, T).

Equations

• Derivation.nontrivialAdjointWeights π = {α : M | α ≠ 1 ∧ Derivation.adjointWeightSpace π α ≠ ⊥}

@[simp]

theorem Derivation.mem_nontrivialAdjointWeights {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] {π : H →ₐc[R] MonoidAlgebra R M} {α : M} : α ∈ nontrivialAdjointWeights π ↔ α ≠ 1 ∧ adjointWeightSpace π α ≠ ⊥

theorem Derivation.adjointWeightSpace_eq_bot_of_notMem_nontrivialAdjointWeights {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] {π : H →ₐc[R] MonoidAlgebra R M} {α : M} (hα : α ≠ 1) (h : α ∉ nontrivialAdjointWeights π) : adjointWeightSpace π α = ⊥

Off the nontrivial adjoint weights and the trivial character the weight submodule vanishes.

theorem Derivation.finite_nontrivialAdjointWeights {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] (π : H →ₐc[R] MonoidAlgebra R M) : (nontrivialAdjointWeights π).Finite

The set of nontrivial adjoint weights is finite. The Lie algebra is finitely generated, so only finitely many weight submodules are nonzero.

theorem Derivation.sup_iSup_adjointWeightSpace_eq_top {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] (π : H →ₐc[R] MonoidAlgebra R M) : adjointWeightSpace π 1 ⊔ ⨆ α ∈ nontrivialAdjointWeights π, adjointWeightSpace π α = ⊤

The Lie algebra is spanned by the trivial weight submodule together with the submodules indexed by the nontrivial adjoint weights.

theorem Derivation.endOfPoint_tmul_of_mem_adjointWeightSpace {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] {A : Type u_1} [CommSemiring A] [Algebra R A] (π : H →ₐc[R] MonoidAlgebra R M) (f : MonoidAlgebra R M →ₐ[R] A) (a : A) {α : M} {x : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)} (hx : x ∈ adjointWeightSpace π α) : (TauCeti.Comodule.endOfPoint (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) (f.comp ↑π)) (a ⊗ₜ[R] x) = (a * f (MonoidAlgebra.single α 1)) ⊗ₜ[R] x

A point of D(M) acts on the α-weight submodule 𝔤_α by the value of the character α at that point.

theorem Derivation.lie_mem_adjointWeightSpace_mul {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {M : Type w} [CommGroup M] {π : H →ₐc[R] MonoidAlgebra R M} {α β : M} {x y : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)} (hx : x ∈ adjointWeightSpace π α) (hy : y ∈ adjointWeightSpace π β) : ⁅x, y⁆ ∈ adjointWeightSpace π (α * β)

The bracket of an α-weight vector and a β-weight vector has weight α * β.

For a split pair this is the root-space grading relation [𝔤_α, 𝔤_β] ⊆ 𝔤_{αβ} (with characters written multiplicatively).