The Borel-type subgroup attached to a set of Kostant root subgroups

Let U_ℤ = kostantForm e h act on a rational representation V preserving an additive subgroup M ≤ V with a weight basis b, so that the split torus T(A) = 𝔾ₘ^κ(A) acts diagonally on A ⊗[ℤ] M and each designated root vector eᵢ acts nilpotently. For a set S of root indices,

B_S(A) = U_S(A) ⬝ T(A) ≤ Aut_A(A ⊗[ℤ] M)

is the subgroup generated by the split torus together with the Kostant root subgroups indexed by S. When S is a positive system of a Chevalley system this is the Borel-type solvable subgroup of points out of which the Borel datum of a pinning of the Chevalley--Demazure group is built: the torus, a group of points containing it, and the root vectors.

Three properties are proved. They are what separates B_S from an arbitrary join, though none of them is the maximality that would make B_S a Borel subgroup on the nose. First, the torus normalizes U_S, by the pinning equation t(s) xᵢ(u) t(s)⁻¹ = xᵢ(α(s) u) of TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Torus.Basic; so U_S is normal in B_S for every index set S, with no closure hypothesis on S. Second, the commutator subgroup of B_S lies in U_S: modulo U_S the group is generated by the image of the abelian group κ → Aˣ. Third, B_S is solvable as soon as U_S is, which by isNilpotent_kostantSubsystemSubgroup holds whenever the indices of S carry a bounded height that every nonzero bracket strictly raises — the situation of a positive system in the simply-laced case. Finally the construction is functorial by inclusion: scalar extension along a morphism of value rings A ⟶ B carries B_S(A) into B_S(B), an inclusion that is in general strict, since B_S(B) also contains the points built from parameters outside the image of A.

Nothing here divides by a factorial, so every statement holds over a value ring of any characteristic; and nothing here asserts that B_S is maximal among solvable subgroups, which is a geometric statement about the group scheme rather than about its points.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup: the subgroup B_S(A) generated by the split torus and the Kostant root subgroups indexed by S.

Main results

• TauCeti.UniversalEnvelopingAlgebra.map_kostantSubsystemSubgroup_conj_kostantTorusPoints: a torus point normalizes U_S(A).
• kostantSubsystemSubgroup_normal_subgroupOf_kostantTorusSubsystemSubgroup: U_S(A) is normal in B_S(A).
• TauCeti.UniversalEnvelopingAlgebra.commutator_kostantTorusSubsystemSubgroup_le: the derived subgroup of B_S(A) lies in U_S(A).
• TauCeti.UniversalEnvelopingAlgebra.isSolvable_kostantTorusSubsystemSubgroup: B_S(A) is solvable under the height grading that makes U_S(A) nilpotent.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusSubsystemSubgroup_le: scalar extension along a morphism of value rings carries B_S(A) into B_S(B).

References

• R. W. Carter, Simple Groups of Lie Type, §§8.2 and 8.5.
• J. E. Humphreys, Linear Algebraic Groups, §§26--28.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

The torus normalizes a subsystem subgroup

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantSubsystemSubgroup_conj_kostantTorusPoints {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)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) (s : κ → (↑A)ˣ) : Subgroup.map (↑(MulAut.conj ((kostantTorusPoints M b wt ↑A) s))) (kostantSubsystemSubgroup e h ρ M hM hnil S A) = kostantSubsystemSubgroup e h ρ M hM hnil S A

The torus normalizes every subsystem subgroup. Conjugation by a torus point carries the root-subgroup element xᵢ(t) to xᵢ(α(s) t), an element of the same root subgroup, so it preserves the subgroup generated by any set of them.

No hypothesis on S is needed: unlike conjugation by a root subgroup, conjugation by the torus does not move the index. The case S = Set.univ is map_kostantElementarySubgroup_conj_kostantTorusPoints.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_mem_normalizer_kostantSubsystemSubgroup {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)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) (s : κ → (↑A)ˣ) : (kostantTorusPoints M b wt ↑A) s ∈ Subgroup.normalizer ↑(kostantSubsystemSubgroup e h ρ M hM hnil S A)

A torus point lies in the normalizer of every subsystem subgroup.

The subgroup generated by the torus and a set of root subgroups

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup {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 κ] (S : Set ι) (A : CommAlgCat ℤ) : Subgroup (LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M))

The subgroup of Aut_A(A ⊗[ℤ] M) generated by the split torus and the Kostant root subgroups indexed by a set S of root indices. For suitable positive systems it supplies the group of points underlying the Borel datum of a pinning; maximality among solvable subgroups is not asserted here.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup_eq_sup {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 κ] (S : Set ι) (A : CommAlgCat ℤ) : kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A = kostantSubsystemSubgroup e h ρ M hM hnil S A ⊔ (kostantTorusPoints M b wt ↑A).range

The Borel-type subgroup is the join of the subsystem subgroup and the torus.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_le_kostantTorusSubsystemSubgroup {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 κ] (S : Set ι) (A : CommAlgCat ℤ) : kostantSubsystemSubgroup e h ρ M hM hnil S A ≤ kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A

The subsystem subgroup is contained in the Borel-type subgroup attached to the same index set.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_mem_kostantTorusSubsystemSubgroup {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 κ] {S : Set ι} {i : ι} (hiS : i ∈ S) (A : CommAlgCat ℤ) (t : Multiplicative ↑A) : (kostantRootSubgroupParam e h ρ M hM i ⋯ A) t ∈ kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A

A root-subgroup element with index in S lies in the Borel-type subgroup.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_mem_kostantTorusSubsystemSubgroup {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 κ] (S : Set ι) (A : CommAlgCat ℤ) (s : κ → (↑A)ˣ) : (kostantTorusPoints M b wt ↑A) s ∈ kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A

Every torus point lies in the Borel-type subgroup.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup_le_iff {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 κ] {S : Set ι} {A : CommAlgCat ℤ} {P : Subgroup (LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M))} : kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A ≤ P ↔ (∀ i ∈ S, ∀ (t : Multiplicative ↑A), (kostantRootSubgroupParam e h ρ M hM i ⋯ A) t ∈ P) ∧ ∀ (s : κ → (↑A)ˣ), (kostantTorusPoints M b wt ↑A) s ∈ P

Elimination principle. A subgroup contains B_S(A) exactly when it contains every torus point and every root-subgroup element indexed by S.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup_mono {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 κ] {S T : Set ι} (hST : S ⊆ T) (A : CommAlgCat ℤ) : kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A ≤ kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt T A

The Borel-type subgroup grows with the index set.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup_empty {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 κ] (A : CommAlgCat ℤ) : kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt ∅ A = (kostantTorusPoints M b wt ↑A).range

With no root subgroups adjoined, the Borel-type subgroup is the torus.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup_univ {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 κ] (A : CommAlgCat ℤ) : kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt Set.univ A = kostantElementarySubgroup e h ρ M hM hnil A ⊔ (kostantTorusPoints M b wt ↑A).range

With every root subgroup adjoined, the Borel-type subgroup is generated by the elementary group and the torus.

The subsystem subgroup is normal, with abelian quotient

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup_le_normalizer {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)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) : kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A ≤ Subgroup.normalizer ↑(kostantSubsystemSubgroup e h ρ M hM hnil S A)

The Borel-type subgroup normalizes its subsystem subgroup: the torus does by the pinning equation, and the subsystem subgroup normalizes itself.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_normal_subgroupOf_kostantTorusSubsystemSubgroup {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)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) : ((kostantSubsystemSubgroup e h ρ M hM hnil S A).subgroupOf (kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A)).Normal

The root-generated subsystem subgroup is normal in the Borel-type subgroup.

theorem TauCeti.UniversalEnvelopingAlgebra.commutator_kostantTorusSubsystemSubgroup_le {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)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) : ⁅kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A, kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A⁆ ≤ kostantSubsystemSubgroup e h ρ M hM hnil S A

The derived subgroup of the Borel-type subgroup lies in the subsystem subgroup. Modulo U_S(A) the group B_S(A) is generated by the image of the abelian group κ → Aˣ of torus points, so its commutator subgroup already lies in U_S(A).

Only the normalizing property of the torus is used, so this holds for an arbitrary index set S; the commutator relations among the root subgroups are not needed.

Solvability

theorem TauCeti.UniversalEnvelopingAlgebra.isSolvable_kostantTorusSubsystemSubgroup_of_isSolvable {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)) (α : ι → κ → ℤ) {S : Set ι} (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) (hsolv : Group.IsSolvable ↥(kostantSubsystemSubgroup e h ρ M hM hnil S A)) : Group.IsSolvable ↥(kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A)

The Borel-type subgroup is solvable whenever its subsystem subgroup is. The quotient by the subsystem subgroup is abelian by commutator_kostantTorusSubsystemSubgroup_le.

theorem TauCeti.UniversalEnvelopingAlgebra.isSolvable_kostantTorusSubsystemSubgroup {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)) (α : ι → κ → ℤ) {S : Set ι} (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) {ht : ι → ℕ} {N : ℕ} (hbdd : ∀ i ∈ S, ht i ≤ N) (hgrade : ∀ i ∈ S, ∀ j ∈ S, ⁅e i, e j⁆ = 0 ∨ ∃ k ∈ S, ht i < ht k ∧ ∃ (c : ℤ), ⁅e i, e j⁆ = c • e k ∧ ⁅e i, e k⁆ = 0 ∧ ⁅e j, e k⁆ = 0) : Group.IsSolvable ↥(kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A)

The Borel-type subgroup of a graded closed set of roots is solvable. Under the hypotheses that make U_S(A) nilpotent — every index of S has bounded height, and a nonzero bracket of two root vectors indexed in S is an integer multiple of a third root vector, indexed in S, of strictly larger height and central for both — the subgroup generated by the split torus and the root subgroups indexed by S is solvable over every value ring.

For a simply-laced Chevalley system and S the positive roots this is the solvability of the Borel-type subgroup of points underlying the Borel datum of the pinning.

Change of value ring

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusSubsystemSubgroup_le {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 κ] {A B : CommAlgCat ℤ} (S : Set ι) (φ : A ⟶ B) : Subgroup.map (GrpCat.Hom.hom (GeneralLinear.mapScalarExtensionAutomorphisms φ)) (kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A) ≤ kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S B

Change of value ring. Scalar extension along a morphism of value rings carries the Borel-type subgroup attached to an index set into the Borel-type subgroup attached to the same index set. This is functoriality by inclusion, not by equality: already for the torus part the image lands in the points whose parameters come from A, so the inclusion is in general strict.