Triangularity of positive Kostant root subgroups

Let M be a Kostant-stable integral lattice with a basis of Cartan weight vectors. If the basis is ordered so that adding a positive multiple of a root moves strictly towards the beginning, then every divided power of the corresponding root operator is strictly upper triangular away from degree zero. Consequently its divided-power exponential is upper unitriangular over every commutative base ring.

This realizes a positive Kostant root subgroup inside the upper-unitriangular group. It is the matrix input needed to place the positive-root subgroup in the unipotent radical of a Borel subgroup in the Chevalley--Demazure construction.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.repr_integralDividedPower_eq_zero_of_not_lt: positive divided powers have no coordinate on or below their source basis vector.
• TauCeti.UniversalEnvelopingAlgebra.isUpperUnitriangular_kostantRootSubgroupMatrix: a positive root-subgroup point has an upper-unitriangular matrix over every commutative ring.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupUpperUnitriangular: the root-subgroup homomorphism corestricted to the upper-unitriangular group.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§21, 26--27.
• R. W. Carter, Simple Groups of Lie Type, §4.4.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

Integral divided-power coordinates

theorem TauCeti.UniversalEnvelopingAlgebra.repr_integralDividedPower_eq_zero_of_not_lt {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) {i : ι} {α : κ → ℤ} {η : Type u_2} [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (horder : ∀ {r s : η} {n : ℕ}, 0 < n → wt r = wt s + n • α → r < s) {r s : η} (hrs : ¬r < s) {n : ℕ} (hn : 0 < n) : (b.repr ((integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M n ⋯) (b s))) r = 0

A positive divided power has no coordinate at a basis vector which does not precede its source. The order hypothesis says precisely that a nonzero positive root shift of weights must move from s to an index r < s.

This statement includes both the entries below the diagonal and the diagonal entries of every positive-degree divided power.

theorem TauCeti.UniversalEnvelopingAlgebra.isUpperTriangular_toMatrix_integralDividedPower {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) {i : ι} {α : κ → ℤ} {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (horder : ∀ {r s : η} {n : ℕ}, 0 < n → wt r = wt s + n • α → r < s) {n : ℕ} (hn : 0 < n) : ((LinearMap.toMatrix b b) (integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M n ⋯)).IsUpperTriangular

Every positive divided power of a positive root operator is upper triangular in an ordered weight basis.

Positive root-subgroup matrices

theorem TauCeti.UniversalEnvelopingAlgebra.isUpperUnitriangular_kostantRootSubgroupMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) {α : κ → ℤ} {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_3} [CommRing A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (horder : ∀ {r s : η} {n : ℕ}, 0 < n → wt r = wt s + n • α → r < s) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : (↑((kostantRootSubgroupMatrix e h ρ M hM i hnil b) f)).IsUpperUnitriangular

A positive Kostant root-subgroup point is upper unitriangular in an ordered weight basis over every commutative base ring. The positive-degree divided powers are strictly upper triangular, while the degree-zero divided power supplies the identity diagonal.

theorem TauCeti.UniversalEnvelopingAlgebra.range_kostantRootSubgroupMatrix_le_upperUnitriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) {α : κ → ℤ} {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_3} [CommRing A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (horder : ∀ {r s : η} {n : ℕ}, 0 < n → wt r = wt s + n • α → r < s) : (kostantRootSubgroupMatrix e h ρ M hM i hnil b).range ≤ upperUnitriangularGroup η A

The image of a positive Kostant root subgroup lies in the upper-unitriangular subgroup of the ambient general linear group.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupUpperUnitriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) {α : κ → ℤ} {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_3} [CommRing A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (horder : ∀ {r s : η} {n : ℕ}, 0 < n → wt r = wt s + n • α → r < s) : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A) →* ↥(upperUnitriangularGroup η A)

A positive Kostant root subgroup, with its codomain restricted to the upper-unitriangular group. This is the root-radical form used in triangular Borel constructions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantRootSubgroupUpperUnitriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) {α : κ → ℤ} {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_3} [CommRing A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (horder : ∀ {r s : η} {n : ℕ}, 0 < n → wt r = wt s + n • α → r < s) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : ↑((kostantRootSubgroupUpperUnitriangular e h ρ M hM b wt i hnil hwt hα ⋯) f) = (kostantRootSubgroupMatrix e h ρ M hM i hnil b) f

Forgetting the upper-unitriangular codomain recovers the original root-subgroup matrix.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantRootSubgroupUpperUnitriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) {α : κ → ℤ} {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (horder : ∀ {r s : η} {n : ℕ}, 0 < n → wt r = wt s + n • α → r < s) (φ : A →+* B) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : (UpperUnitriangularGroup.map φ) ((kostantRootSubgroupUpperUnitriangular e h ρ M hM b wt i hnil hwt hα ⋯) f) = (kostantRootSubgroupUpperUnitriangular e h ρ M hM b wt i hnil hwt hα ⋯) ((AlgHom.mapValue φ.toIntAlgHom) f)

The upper-unitriangular realization of a positive Kostant root subgroup is natural in the commutative base ring.