Square-zero root vectors make the weight torus redundant

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Torus.Coroot puts a coroot value h_α(u) of a Kostant carrier in the elementary group generated by the root subgroups whenever u is a value α(s) of the root on the weight torus, which reaches every unit exactly when the coordinates of α are setwise coprime. That criterion fails at a long simple root of B₂ and of Cₙ, whose row of the Cartan matrix is (2, -2) up to padding, and at the rank-one row (2).

This file supplies the criterion that covers those cases. It needs nothing about the coordinates of the root and instead asks that the raising and lowering operators act with square zero, which for a weight module says that the α-string through every weight has length at most two. Writing E and F for the two operators and u for a unit of the value ring, the Chevalley rank-one identity

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

holds because both sides are 1 + u E - u⁻¹ F - E F - F E: the square-zero hypothesis truncates each exponential to 1 + t E, and E F and F E are then orthogonal idempotents projecting onto the two ends of every α-string, with h_α(u) acting by u on one and u⁻¹ on the other.

The rank-one algebra behind that identity is carried out for an arbitrary square-zero sl₂ pair in TauCeti/Algebra/Lie/Sl2/SquareZero.lean; this file only feeds it the base-changed Kostant root operators and reads the coordinate cocharacter off the weight basis.

Since n_α is itself a product of root subgroup elements, the identity puts h_α(u) in the elementary group for every unit u, so the weight torus of a carrier all of whose numbered root operators square to zero is redundant. The standard symplectic carrier of type Cₙ, whose representation is the standard one, is of that kind.

Main results

• kostantRootSubgroupParam_val_of_sq_eq_zero: a square-zero root operator exponentiates to 1 + t E.
• kostantCoordinateCocharacter_mem_kostantElementarySubgroup_of_sq_eq_zero: the coroot value at every unit lies in the elementary group.
• kostantTorusSubgroup_le_kostantElementarySubgroup_of_forall_coordinateCocharacter and kostantTorusSubsystemSubgroup_univ_eq_kostantElementarySubgroup_of_sq_eq_zero: the weight torus, and then the Borel-type join, collapse into the elementary group.

All names below live in the TauCeti.UniversalEnvelopingAlgebra namespace.

References

• R. Steinberg, Lectures on Chevalley Groups, §3, Lemma 20 and Corollary 5.
• R. W. Carter, Simple Groups of Lie Type, §6.4.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

Square-zero root operators

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_val_of_sq_eq_zero {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (i : ι) (hsq : ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) ^ 2 = 0) (A : CommAlgCat ℤ) (t : Multiplicative ↑A) : ↑((kostantRootSubgroupParam e h ρ M hM i ⋯ A) t) = 1 + Multiplicative.toAdd t • LinearMap.baseChange (↑A) (kostantRootOperator e h ρ M hM i)

A square-zero root operator exponentiates to 1 + t X_α. All divided powers beyond the first vanish, so the root subgroup element is affine in its parameter.

The weight torus of a carrier with square-zero root operators

theorem TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter_mem_kostantElementarySubgroup_of_sq_eq_zero {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] [DecidableEq κ] {c : κ} {i j : ι} (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hsqi : ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) ^ 2 = 0) (hsqj : ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)) ^ 2 = 0) (A : CommAlgCat ℤ) (u : (↑A)ˣ) : (kostantCoordinateCocharacter M b wt (↑A) c) u ∈ kostantElementarySubgroup e h ρ M hM hnil A

A square-zero sl₂ pair puts every coroot value in the elementary group. The rank-one identity x_α(u) x_{-α}(-u⁻¹) x_α(u) = h_α(u) n_α exhibits the coroot value at an arbitrary unit as a product of root subgroup elements, with no coprimality condition on the coordinates of α.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubgroup_le_kostantElementarySubgroup_of_forall_coordinateCocharacter {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] [DecidableEq κ] (A : CommAlgCat ℤ) (hcoord : ∀ (d : κ) (v : (↑A)ˣ), (kostantCoordinateCocharacter M b wt (↑A) d) v ∈ kostantElementarySubgroup e h ρ M hM hnil A) : kostantTorusSubgroup M b wt ↑A ≤ kostantElementarySubgroup e h ρ M hM hnil A

The weight torus lies in the elementary group as soon as every coordinate cocharacter does.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup_univ_eq_kostantElementarySubgroup_of_sq_eq_zero {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (raise lower : κ → ι) (hT : ∀ (d : κ), IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h d))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (raise d)))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (lower d))))) (hsq : ∀ (k : ι), ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)) ^ 2 = 0) (A : CommAlgCat ℤ) : kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt Set.univ A = kostantElementarySubgroup e h ρ M hM hnil A

The Borel-type join of the weight torus with every root subgroup is the elementary group when every numbered root operator squares to zero.