sl₂ pairs whose raising and lowering elements square to zero

Let H, E, F satisfy the sl₂ relations for the ring commutator of an associative ring, as in TauCeti/Algebra/Lie/Sl2/Associative.lean, and assume in addition that E and F square to zero. For a representation that means the α-string through every weight has length at most two, so the module is a sum of copies of the trivial and the standard two-dimensional representation. This file records what that hypothesis buys.

First it halves the relation H E - E H = 2 E to E F E = E: once E ^ 2 = 0 both H E and -E H are already equal to E F E. The two products E F and F E then become orthogonal idempotents whose difference is H, cutting out the two ends of each α-string.

Second, a square-zero element makes the exponential 1 + t E affine in its parameter, and the Chevalley rank-one identity

x_α(u) x_{-α}(-u⁻¹) x_α(u) = h_α(u) n_α,      n_α = x_α(1) x_{-α}(-1) x_α(1),

holds over every commutative coefficient ring, at every unit u, because both sides equal 1 + u E - u⁻¹ F - E F - F E. The left-hand side is the triple product computed in triple_product_of_mul_self_eq_zero, and the right-hand side is the diagonal element 1 + (u - 1) E F + (u⁻¹ - 1) F E rescaling the two root terms of that normal form at parameters (1, -1), which is torus_mul_triple_product_of_mul_self_eq_zero. Neither step divides by anything: the square-zero hypothesis truncates every divided-power exponential after its first term, so no denominator is ever introduced.

Together these are the rank-one inputs to the scheme-theoretic root generation of an explicit Chevalley--Demazure carrier whose representation has short α-strings, the standard symplectic carrier of type Cₙ among them.

Main results

• e_mul_f_mul_e_of_mul_self_eq_zero and f_mul_e_mul_f_of_mul_self_eq_zero: the halved sl₂ relations E F E = E and F E F = F.
• triple_product_of_mul_self_eq_zero: the normal form of (1 + α E) (1 + β F) (1 + α E) when α β = -1, over an arbitrary commutative coefficient ring.
• torus_mul_triple_product_of_mul_self_eq_zero: multiplying that normal form at (1, -1) by a diagonal element rescales its two root terms.
• mul_apply_of_eq_intCast_smul: an integer eigenvector of H has eigenvalue 1, 0 or -1, and in the outer two cases it is fixed by one of the two idempotents and killed by the other.

References

• R. Steinberg, Lectures on Chevalley Groups, §3, Lemma 20.
• R. W. Carter, Simple Groups of Lie Type, §6.4.

Halving the sl₂ relation

theorem TauCeti.Sl2.e_mul_f_mul_e_of_mul_self_eq_zero {A : Type u_1} [Ring A] [Algebra ℚ A] {H E F : A} (hEE : E * E = 0) (hef : E * F - F * E = H) (hhe : H * E - E * H = 2 • E) : E * F * E = E

A square-zero raising element satisfies E F E = E. Both H E and -E H equal E F E once E * E = 0, so the sl₂ relation H E - E H = 2 E halves to the displayed identity.

theorem TauCeti.Sl2.f_mul_e_mul_f_of_mul_self_eq_zero {A : Type u_1} [Ring A] [Algebra ℚ A] {H E F : A} (hFF : F * F = 0) (hef : E * F - F * E = H) (hhf : H * F - F * H = -(2 • F)) : F * E * F = F

A square-zero lowering element satisfies F E F = F, the mirror image of e_mul_f_mul_e_of_mul_self_eq_zero across the sl₂ triple (-H, F, E).

The rank-one identity over an arbitrary coefficient ring

theorem TauCeti.Sl2.triple_product_of_mul_self_eq_zero {B : Type u_1} [CommRing B] {N : Type u_2} [AddCommGroup N] [Module B N] {E F : Module.End B N} (hEE : E * E = 0) (hEFE : E * F * E = E) {α β : B} (hαβ : α * β = -1) : (1 + α • E) * (1 + β • F) * (1 + α • E) = 1 + α • E + β • F - E * F - F * E

The rank-one product of three square-zero exponentials. When the two parameters multiply to -1, the product (1 + α E) (1 + β F) (1 + α E) is 1 + α E + β F - E F - F E.

theorem TauCeti.Sl2.torus_mul_triple_product_of_mul_self_eq_zero {B : Type u_1} [CommRing B] {N : Type u_2} [AddCommGroup N] [Module B N] {E F : Module.End B N} (hEE : E * E = 0) (hFF : F * F = 0) (hEFE : E * F * E = E) (hFEF : F * E * F = F) (α β : B) : (1 + (α - 1) • (E * F) + (β - 1) • (F * E)) * (1 + 1 • E + -1 • F - E * F - F * E) = 1 + α • E + -β • F - E * F - F * E

The coroot value times the Weyl representative. Multiplying the normal form at parameters (1, -1) by the diagonal element 1 + (α - 1) E F + (β - 1) F E rescales its two root terms.

The two idempotents on an integer eigenvector

theorem TauCeti.Sl2.mul_apply_of_eq_intCast_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] {E F H : Module.End ℚ V} (hEE : E * E = 0) (hFF : F * F = 0) (hEFE : E * F * E = E) (hFEF : F * E * F = F) (hef : E * F - F * E = H) {m : ℤ} {v : V} (hv : H v = ↑m • v) (hv0 : v ≠ 0) : m = 1 ∧ (E * F) v = v ∧ (F * E) v = 0 ∨ m = 0 ∧ (E * F) v = 0 ∧ (F * E) v = 0 ∨ m = -1 ∧ (E * F) v = 0 ∧ (F * E) v = v

The two square-zero products split an integer eigenvector of H. The products E F and F E are orthogonal idempotents whose difference is H, so a nonzero eigenvector with integer eigenvalue has eigenvalue 1, 0 or -1, and in the outer two cases it is fixed by E F respectively by F E while the other product kills it.