Documentation

TauCeti.RingTheory.Nilpotent.ChevalleyCommutator

The Chevalley commutator relation for integral nilpotent exponentials #

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

x * y = y * x + z,   z commuting with both x and y.

The integral divided-power exponentials of x, y, z act on the scalar extension R ⊗[ℤ] M over every commutative ring R, by TauCeti.baseChangeExp. The main result below is that they satisfy the Chevalley commutator relation

E_x(t) E_y(u) = E_y(u) E_z(t * u) E_x(t).

Equivalently E_x(t) E_y(u) E_x(t)⁻¹ = E_y(u) E_z(t * u): conjugating the one-parameter subgroup of y by the one-parameter subgroup of x multiplies it by the one-parameter subgroup of the commutator, at the product parameter. This is the class-two case of the Chevalley commutator formula, the case in which the only root of the form i α + j β besides α and β is α + β; in a simply-laced root system every pair of non-proportional roots falls under it or under the degenerate case below.

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 normal-ordering rule TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq, which says that the rational divided powers reorder with integral structure constants; the exponential identity is its generating-function form.

Main results #

References #

Normal ordering the restricted operators #

source
theorem TauCeti.integralDividedPower_mul_integralDividedPower_of_commutator_eq {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 : A} (M : S) (hxy : x * y = y * x + z) (hxz : Commute x z) (hyz : Commute y 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) (m n : ℕ) :
integralDividedPower x M m ⋯ * integralDividedPower y M n ⋯ = ∑ k ∈ Finset.range (min m n + 1), integralDividedPower y M (n - k) ⋯ * integralDividedPower z M k ⋯ * integralDividedPower x M (m - k) ⋯

Normal ordering for restricted divided powers. If x * y = y * x + z and z commutes with both x and y, the integral operators obtained by restricting divided powers to a stable additive subgroup satisfy the coefficient-one straightening rule.

Rescaling by an integer #

source
theorem TauCeti.integralDividedPower_zsmul {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] (c : ℤ) {x : A} (M : S) (n : ℕ) (hM : ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hcM : ∀ v ∈ M, Associative.dividedPower n (c • x) • v ∈ M) :
integralDividedPower (c • x) M n hcM = c ^ n • integralDividedPower x M n hM

Restricting the divided power of an integer multiple scales the restricted operator by the same power of that integer.

source
theorem TauCeti.baseChangeExp_zsmul {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] (c : ℤ) {x : A} (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hcM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n (c • x) • v ∈ M) (hx : IsNilpotent x) (t : R) :
baseChangeExp (c • x) M hcM t = baseChangeExp x M hM (↑c * t)

Rescaling an element by an integer c rescales the parameter of its integral exponential by c. This is how an integer Chevalley structure constant is absorbed into the parameter of a root subgroup.

The generating-function form of normal ordering #

The Chevalley commutator relation #

source
theorem TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq {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 : A} (M : S) (hxy : x * y = y * x + z) (hxz : Commute x z) (hyz : Commute y z) (hx : IsNilpotent x) (hy : IsNilpotent y) (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) (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 x M hMx t

The Chevalley commutator relation for integral nilpotent exponentials. If x * y = y * x + z with z commuting with x and with y, 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_x(t).

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

source
theorem TauCeti.commute_baseChangeExp {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 : A} (M : S) (hxy : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) (hMx : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (hMy : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n y • v ∈ M) (t u : R) :
Commute (baseChangeExp x M hMx t) (baseChangeExp y M hMy u)

The degenerate Chevalley commutator relation. Exponentials of commuting elements commute. For root subgroups this is the case of two roots which are not opposite and whose sum is not a root.

source
theorem TauCeti.baseChangeExp_conj_of_commutator_eq {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 : A} (M : S) (hxy : x * y = y * x + z) (hxz : Commute x z) (hyz : Commute y z) (hx : IsNilpotent x) (hy : IsNilpotent y) (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) (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)

The conjugation form of the Chevalley commutator relation: conjugating the one-parameter subgroup of y by that of x multiplies it by the one-parameter subgroup of the commutator z, at the product parameter.