The Chevalley commutator relation in type `G₂` #

Let V be a module over a ℚ-algebra A, let M ≤ V be an additive subgroup, and let x, y, z, w, v, s be elements of A with

x * y = y * x + z,   x * z = z * x + 2 • w,   x * w = w * x + 3 • v,   w * z = z * w + 3 • s,

v and s commuting with x, y commuting with z, w commuting with v, and s commuting with z, w, and v. The integral divided-power exponentials of the six elements act on R ⊗[ℤ] M over every commutative ring R, by TauCeti.baseChangeExp. The main result below is the Chevalley commutator relation in type G₂

E_x(t) E_y(u) = E_y(u) E_z(t * u) E_w(t ^ 2 * u) E_v(t ^ 3 * u) E_s(t ^ 3 * u ^ 2) E_x(t).

This is the case of the Chevalley commutator formula in which the roots of the form i α + j β with i, j > 0 are α + β, 2α + β, 3α + β, and 3α + 2β. It occurs for the two simple roots of a root system of type G₂, α short and β long, and in no other type; it extends the chain β, α + β, 2α + β of TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq_two_nsmul. The parameter of each factor is t ^ i * u ^ j for the root i α + j β it belongs to; in particular the last factor has the parameter t ^ 3 * u ^ 2, which is what makes this case not a chain in ad x alone. The one remaining type-G₂ configuration, the pair α, α + β, is not treated here; see TauCeti.RingTheory.Nilpotent.RootString.G2.ShortPair for its exponential relation.

Nothing here divides by a factorial in R, so the relation holds over a ring of arbitrary characteristic. The whole point is the coefficient-one straightening rule TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq_three_nsmul; the exponential identity is its generating-function form, and the parameters u, t * u, t ^ 2 * u, t ^ 3 * u, t ^ 3 * u ^ 2, t are exactly the six monomials into which t ^ m u ^ n factors.

Main results #

TauCeti.integralDividedPower_mul_integralDividedPower_of_commutator_eq_three_nsmul: the straightening rule for the integral operators restricted to M.
TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq_three_nsmul: the Chevalley commutator relation in type G₂.
TauCeti.baseChangeExp_conj_of_commutator_eq_three_nsmul: its conjugation form.

References #

R. W. Carter, Simple Groups of Lie Type, §4.2 and Theorem 5.2.2.
J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§25--26.
J. C. Jantzen, Representations of Algebraic Groups, II.1.

Straightening the restricted operators #

source

theorem TauCeti.integralDividedPower_mul_integralDividedPower_of_commutator_eq_three_nsmul {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {x y z w v s : A} (M : S) (hxy : x * y = y * x + z) (hxz : x * z = z * x + 2 • w) (hxw : x * w = w * x + 3 • v) (hwz : w * z = z * w + 3 • s) (hxv : Commute x v) (hxs : Commute x s) (hyz : Commute y z) (hwv : Commute w v) (hzs : Commute z s) (hws : Commute w s) (hvs : Commute v s) (hMx : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n x • a ∈ M) (hMy : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n y • a ∈ M) (hMz : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n z • a ∈ M) (hMw : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n w • a ∈ M) (hMv : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n v • a ∈ M) (hMs : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n s • a ∈ M) (m n : ℕ) :

integralDividedPower x M m ⋯ * integralDividedPower y M n ⋯ = ∑ p ∈ Associative.chainG2Index m n, integralDividedPower y M (n - p.1 - p.2.1 - p.2.2.1 - 2 * p.2.2.2) ⋯ * integralDividedPower z M p.1 ⋯ * integralDividedPower w M p.2.1 ⋯ * integralDividedPower v M p.2.2.1 ⋯ * integralDividedPower s M p.2.2.2 ⋯ * integralDividedPower x M (m - p.1 - 2 * p.2.1 - 3 * p.2.2.1 - 3 * p.2.2.2) ⋯

Straightening restricted divided powers in type G₂. The type-G₂ straightening rule transported to the integral operators obtained by restricting divided powers to a stable additive subgroup.

The generating-function form of the straightening rule #