The Chevalley commutator relation for the chain β, α + β, 2α + β

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

x * y = y * x + z,   x * z = z * x + 2 • w,

w commuting with x, y commuting with z, and z commuting with w. The integral divided-power exponentials of the four elements act on R ⊗[ℤ] M over every commutative ring R, by TauCeti.baseChangeExp. The main result below is the Chevalley commutator relation for the chain β, α + β, 2α + β

E_x(t) E_y(u) = E_y(u) E_z(t * u) E_w(t ^ 2 * u) 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 exactly α + β and 2 α + β, covering the additional chains in types B, C, and F₄. Type G₂ also needs the longer chain containing 3α + β and 3α + 2β, which is TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq_three_nsmul in TauCeti.RingTheory.Nilpotent.RootString.G2.Basic. This extends the class-two case of TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq. The parameter of the extra factor is t ^ 2 * u, matching the exponents (i, j) = (2, 1) of the root 2 α + β.

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_two_nsmul; the exponential identity is its generating-function form, and the parameters u, t * u, t ^ 2 * u, t are exactly the four monomials u ^ a (t u) ^ b (t ^ 2 u) ^ c t ^ q into which t ^ m u ^ n factors.

Main results

• TauCeti.integralDividedPower_mul_integralDividedPower_of_commutator_eq_two_nsmul: the straightening rule for the integral operators restricted to M.
• TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq_two_nsmul: the Chevalley commutator relation.
• TauCeti.baseChangeExp_conj_of_commutator_eq_two_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

theorem TauCeti.integralDividedPower_mul_integralDividedPower_of_commutator_eq_two_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 : A} (M : S) (hxy : x * y = y * x + z) (hxz : x * z = z * x + 2 • w) (hxw : Commute x w) (hyz : Commute y z) (hzw : Commute z w) (hMx : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hMy : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n y • v ∈ M) (hMz : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n z • v ∈ M) (hMw : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n w • v ∈ M) (m n : ℕ) : integralDividedPower x M m ⋯ * integralDividedPower y M n ⋯ = ∑ p ∈ Associative.chainLeTwoIndex m n, integralDividedPower y M (n - p.1 - p.2) ⋯ * integralDividedPower z M p.1 ⋯ * integralDividedPower w M p.2 ⋯ * integralDividedPower x M (m - p.1 - 2 * p.2) ⋯

Straightening restricted divided powers for the chain β, α + β, 2α + β. If x * y = y * x + z and x * z = z * x + 2 • w, with w commuting with x, y commuting with z, and z commuting with w, the integral operators obtained by restricting divided powers to a stable additive subgroup satisfy the coefficient-one straightening rule.

The generating-function form of the straightening rule

The Chevalley commutator relation

theorem TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq_two_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] {R : Type v} [CommRing R] [Algebra ℤ R] {x y z w : A} (M : S) (hxy : x * y = y * x + z) (hxz : x * z = z * x + 2 • w) (hxw : Commute x w) (hyz : Commute y z) (hzw : Commute z w) (hx : IsNilpotent x) (hy : IsNilpotent y) (hz : IsNilpotent z) (hMx : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hMy : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n y • v ∈ M) (hMz : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n z • v ∈ M) (hMw : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n w • v ∈ M) (t u : R) : baseChangeExp x M hMx t * baseChangeExp y M hMy u = baseChangeExp y M hMy u * baseChangeExp z M hMz (t * u) * baseChangeExp w M hMw (t ^ 2 * u) * baseChangeExp x M hMx t

The Chevalley commutator relation for the chain β, α + β, 2α + β. If x * y = y * x + z and x * z = z * x + 2 • w, with w commuting with x, y commuting with z, and z commuting with w, then over every commutative ring R the integral divided-power exponentials on R ⊗[ℤ] M satisfy

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

No factorial is inverted in R: the relation holds in every characteristic.

theorem TauCeti.baseChangeExp_conj_of_commutator_eq_two_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] {R : Type v} [CommRing R] [Algebra ℤ R] {x y z w : A} (M : S) (hxy : x * y = y * x + z) (hxz : x * z = z * x + 2 • w) (hxw : Commute x w) (hyz : Commute y z) (hzw : Commute z w) (hx : IsNilpotent x) (hy : IsNilpotent y) (hz : IsNilpotent z) (hMx : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hMy : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n y • v ∈ M) (hMz : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n z • v ∈ M) (hMw : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n w • v ∈ M) (t u : R) : baseChangeExp x M hMx t * baseChangeExp y M hMy u * baseChangeExp x M hMx (-t) = baseChangeExp y M hMy u * baseChangeExp z M hMz (t * u) * baseChangeExp w M hMw (t ^ 2 * u)

The conjugation form of the Chevalley commutator relation for the chain β, α + β, 2α + β: conjugating the one-parameter subgroup of y by that of x multiplies it by the one-parameter subgroups of z and of w, at the parameters t * u and t ^ 2 * u.