The tangent vector of a Kostant root subgroup

A pinning of a split reductive group scheme is the data (G, T, B, {X_α}) of a split maximal torus, a Borel containing it, and a root vector X_α in the Lie algebra for each simple root. What ties that data to the root subgroup maps x_α : 𝔾ₐ → G is a pair of equations: the differential of x_α at the identity is X_α, and the torus acts on X_α through the root α. This file proves the first, so that the Kostant root vectors are read off the morphisms already built rather than posited alongside them; the second is kostantTorusPoints_conj_kostantRootOperator, an algebraic statement about points that needs no scheme theory and lives beside the torus it is about.

The integral operator X_α is kostantRootOperator, the restriction to the lattice M of the designated root vector ρ(eᵢ). It is the first restricted divided power, so it is exactly the linear coefficient of the divided-power exponential

xᵢ(t) = ∑ₖ e⁽ᵏ⁾ tᵏ.

The coordinate morphism of x_α therefore sends a generic matrix entry to a polynomial in the coordinate t of 𝔾ₐ whose linear coefficient is the corresponding entry of X_α. A tangent vector at the identity is a counit-valued derivation, and the coordinate t is primitive, so such a derivation annihilates every power of t other than the first (AdditiveGroup.tangent_ι_pow_eq_zero). Differentiating the coordinate morphism therefore reads off precisely that linear coefficient, which is tangentMatrix_derivationComp_kostantRootSubgroupCoordinateMap. Together with the torus equation both directions of the pinning are available in the form a consumer states its conventions in.

Main results

• tangentMatrix_derivationComp_kostantRootSubgroupCoordinateMap, in the namespace TauCeti.UniversalEnvelopingAlgebra: the differential of the root subgroup is the root vector. The matrix of the tangent vector obtained by differentiating x_α : 𝔾ₐ → GLₙ along a tangent vector of 𝔾ₐ is that tangent vector's value times the matrix of X_α. The entrywise form is ..._apply.

References

• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• J. S. Milne, Algebraic Groups (2017), §§10, 21.
• R. W. Carter, Simple Groups of Lie Type, §4.4.

theorem TauCeti.UniversalEnvelopingAlgebra.tangentMatrix_derivationComp_kostantRootSubgroupCoordinateMap_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {B : Type u_2} [CommRing B] [Algebra ℤ B] (d : Derivation ℤ (SymmetricAlgebra ℤ ℤ) (Bialgebra.CounitAlgebra ℤ (SymmetricAlgebra ℤ ℤ) B)) (r s : Fin n) : (GeneralLinear.tangentMatrix n) ((derivationComp (CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b))) d) r s = (b.repr ((kostantRootOperator e h ρ M hM i) (b s))) r • AdditiveGroup.gaTangentLinearEquiv d

The differential of a Kostant root subgroup is the root vector.

Differentiating the coordinate morphism of x_α : 𝔾ₐ → GLₙ at the identity carries a tangent vector of 𝔾ₐ, that is a scalar of the coefficient algebra, to that scalar times the matrix of the integral root operator X_α. This is the equation pinning the root subgroup map against the root vector of the pinning. This is the entrywise form; tangentMatrix_derivationComp_kostantRootSubgroupCoordinateMap is the matrix it computes.

theorem TauCeti.UniversalEnvelopingAlgebra.tangentMatrix_derivationComp_kostantRootSubgroupCoordinateMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {B : Type u_2} [CommRing B] [Algebra ℤ B] (d : Derivation ℤ (SymmetricAlgebra ℤ ℤ) (Bialgebra.CounitAlgebra ℤ (SymmetricAlgebra ℤ ℤ) B)) : (GeneralLinear.tangentMatrix n) ((derivationComp (CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b))) d) = AdditiveGroup.gaTangentLinearEquiv d • ((LinearMap.toMatrix b b) (kostantRootOperator e h ρ M hM i)).map ⇑(algebraMap ℤ B)

The differential of a Kostant root subgroup is the root vector, as a matrix.

Along the tangent vector of 𝔾ₐ with value t, the differential of x_α : 𝔾ₐ → GLₙ at the identity is t X_α, with X_α the integral root operator written in the lattice basis. This is the equation pinning the root subgroup map against the root vector of the pinning; it determines X_α from x_α, since a matrix is determined by its entries.