Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Subsystem

Subgroups generated by a set of Kostant root subgroups #

Let U_ℤ = kostantForm e h act on a rational representation V preserving an additive subgroup M ≤ V, with every distinguished root vector eᵢ acting nilpotently. For a set S of indices,

U_S(A) = ⟨xᵢ(t) : i ∈ S, t ∈ A⟩ ≤ Aut_A(A ⊗[ℤ] M)

is the subgroup generated by the corresponding Kostant root subgroups. Taking S to be all indices recovers the elementary group of TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Elementary.Basic. In the simply-laced case, taking S to be the positive roots gives the positive-root subgroup, the class-two model of the group that a pinning of a Chevalley--Demazure group scheme will exhibit as the unipotent radical of a Borel subgroup; that identification is not made here.

The Chevalley commutator relations make U_S behave like the subgroup attached to a closed set of roots. Two statements are proved. First, U_S is normalized by U_T whenever the bracket of a root vector indexed in T with one indexed in S stays in S; this is IsChevalleyStableUnder, which packages the class-two Chevalley hypothesis of TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Commutator.Basic over a pair of index sets. Second, if the indices of S carry a bounded height that every nonzero bracket strictly raises, and each bracket root is central for both inputs, then U_S(A) is nilpotent: the subgroups attached to the level sets {i ∈ S | n ≤ ht i} form a descending central series that reaches the trivial subgroup.

The generic group-theoretic hypotheses of kostantSubsystemSubgroup_le_normalizer and commutator_kostantSubsystemSubgroup_le are stated on the root-subgroup generators rather than on Lie brackets, so that a longer commutator relation — a root string of length greater than one, as occurs outside the simply-laced types — can be fed in the same way once available.

Main declarations #

References #

source
theorem TauCeti.UniversalEnvelopingAlgebra.commute_kostantRootSubgroupParam {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) {i j : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hij : ⁅e i, e j⁆ = 0) (A : CommAlgCat ℤ) (t u : Multiplicative ↑A) :
Commute ((kostantRootSubgroupParam e h ρ M hM i hi A) t) ((kostantRootSubgroupParam e h ρ M hM j hj A) u)

Root subgroups attached to commuting root vectors commute, with the parameter read in the value ring.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_conj_of_lie_eq {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) {i j k : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (A : CommAlgCat ℤ) (t u : Multiplicative ↑A) :
(kostantRootSubgroupParam e h ρ M hM i hi A) t * (kostantRootSubgroupParam e h ρ M hM j hj A) u * ((kostantRootSubgroupParam e h ρ M hM i hi A) t)⁻¹ = (kostantRootSubgroupParam e h ρ M hM j hj A) u * (kostantRootSubgroupParam e h ρ M hM k hk A) (Multiplicative.ofAdd (↑c * (Multiplicative.toAdd t * Multiplicative.toAdd u)))

The Chevalley commutator relation with the parameter in the value ring. If ⁅eᵢ, eⱼ⁆ = c • eₖ with eₖ central for both, then xᵢ(t) xⱼ(u) xᵢ(t)⁻¹ = xⱼ(u) xₖ(c t u).

source
theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupParam_of_lie_eq {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) {i j k : ι} (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (A : CommAlgCat ℤ) (t u : Multiplicative ↑A) :
⁅(kostantRootSubgroupParam e h ρ M hM i hi A) t, (kostantRootSubgroupParam e h ρ M hM j hj A) u⁆ = (kostantRootSubgroupParam e h ρ M hM k hk A) (Multiplicative.ofAdd (↑c * (Multiplicative.toAdd t * Multiplicative.toAdd u)))

The Chevalley commutator relation in element-commutator form, with the parameter in the value ring: ⁅xᵢ(t), xⱼ(u)⁆ = xₖ(c t u).

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

The subgroup of Aut_A(A ⊗[ℤ] M) generated by the Kostant root subgroups indexed by a set S of root indices.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_eq_closure {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)))) (S : Set ι) (A : CommAlgCat ℤ) :
    kostantSubsystemSubgroup e h ρ M hM hnil S A = Subgroup.closure {g : LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M) | ∃ i ∈ S, ∃ (t : Multiplicative ↑A), (kostantRootSubgroupParam e h ρ M hM i ⋯ A) t = g}

    The subgroup attached to S is generated by the root-subgroup elements indexed by S.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_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)))) {S : Set ι} {A : CommAlgCat ℤ} {P : Subgroup (LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M))} :
    kostantSubsystemSubgroup e h ρ M hM hnil S A ≤ P ↔ ∀ i ∈ S, ∀ (t : Multiplicative ↑A), (kostantRootSubgroupParam e h ρ M hM i ⋯ A) t ∈ P

    Elimination principle. A subgroup contains U_S(A) exactly when it contains every root-subgroup element indexed by S.

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

    A root-subgroup element with index in S lies in the subgroup attached to S.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_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)))) {S T : Set ι} (hST : S ⊆ T) (A : CommAlgCat ℤ) :
    kostantSubsystemSubgroup e h ρ M hM hnil S A ≤ kostantSubsystemSubgroup e h ρ M hM hnil T A

    The subgroup attached to a set of indices grows with the set.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_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)))) (A : CommAlgCat ℤ) :
    kostantSubsystemSubgroup e h ρ M hM hnil ∅ A = ⊥

    The empty index set generates the trivial subgroup.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_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)))) (A : CommAlgCat ℤ) :
    kostantSubsystemSubgroup e h ρ M hM hnil Set.univ A = kostantElementarySubgroup e h ρ M hM hnil A

    All indices generate the elementary group.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_le_kostantElementarySubgroup {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)))) (S : Set ι) (A : CommAlgCat ℤ) :
    kostantSubsystemSubgroup e h ρ M hM hnil S A ≤ kostantElementarySubgroup e h ρ M hM hnil A

    Every subsystem subgroup sits inside the elementary group.

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

    Scalar extension along a morphism of value rings carries a subsystem subgroup into the subsystem subgroup attached to the same index set.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_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)))) {S T : Set ι} {A : CommAlgCat ℤ} (hconj : ∀ i ∈ T, ∀ j ∈ S, ∀ (t u : Multiplicative ↑A), (kostantRootSubgroupParam e h ρ M hM i ⋯ A) t * (kostantRootSubgroupParam e h ρ M hM j ⋯ A) u * ((kostantRootSubgroupParam e h ρ M hM i ⋯ A) t)⁻¹ ∈ kostantSubsystemSubgroup e h ρ M hM hnil S A) :
    kostantSubsystemSubgroup e h ρ M hM hnil T A ≤ Subgroup.normalizer ↑(kostantSubsystemSubgroup e h ρ M hM hnil S A)

    Generators normalize. U_T(A) normalizes U_S(A) as soon as every root-subgroup element indexed in T conjugates every root-subgroup element indexed in S back into U_S(A).

    The hypothesis is only needed for one of the two conjugations because the generating set is closed under inverses: xᵢ(t)⁻¹ = xᵢ(t⁻¹).

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.commutator_kostantSubsystemSubgroup_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)))) {S T R : Set ι} {A : CommAlgCat ℤ} (hS : kostantSubsystemSubgroup e h ρ M hM hnil S A ≤ Subgroup.normalizer ↑(kostantSubsystemSubgroup e h ρ M hM hnil R A)) (hT : kostantSubsystemSubgroup e h ρ M hM hnil T A ≤ Subgroup.normalizer ↑(kostantSubsystemSubgroup e h ρ M hM hnil R A)) (hcomm : ∀ i ∈ S, ∀ j ∈ T, ∀ (t u : Multiplicative ↑A), ⁅(kostantRootSubgroupParam e h ρ M hM i ⋯ A) t, (kostantRootSubgroupParam e h ρ M hM j ⋯ A) u⁆ ∈ kostantSubsystemSubgroup e h ρ M hM hnil R A) :
    ⁅kostantSubsystemSubgroup e h ρ M hM hnil S A, kostantSubsystemSubgroup e h ρ M hM hnil T A⁆ ≤ kostantSubsystemSubgroup e h ρ M hM hnil R A

    Generators bound a commutator subgroup. If a subsystem subgroup is normalized by two others, then it contains their commutator as soon as it contains the commutators of the root-subgroup generators.

    source
    def TauCeti.UniversalEnvelopingAlgebra.IsChevalleyStableUnder {L : Type u} [LieRing L] {ι : Type u_1} (e : ι → L) (S T : Set ι) :
    Prop

    The index set S is Chevalley stable under the index set T when, for every i ∈ T and j ∈ S, the root vectors eᵢ and eⱼ either commute or have bracket an integer multiple of a third root vector eₖ with k ∈ S, central for both.

    This is the class-two case of the Chevalley commutator formula: α + β is a root while neither 2α + β nor α + 2β is. In a simply-laced root system every pair of non-proportional roots falls under one of the two alternatives, so a set of roots closed under addition is stable under any set of roots that maps it into itself.

    Equations
    Instances For
      source
      theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_le_normalizer_of_isChevalleyStable {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)))) {S T : Set ι} (hstable : IsChevalleyStableUnder e S T) (A : CommAlgCat ℤ) :
      kostantSubsystemSubgroup e h ρ M hM hnil T A ≤ Subgroup.normalizer ↑(kostantSubsystemSubgroup e h ρ M hM hnil S A)

      A Chevalley-stable index set has its subsystem subgroup normalized by the larger one.

      source
      theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemSubgroup_normal_subgroupOf {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)))) {S T : Set ι} (hST : S ⊆ T) (hstable : IsChevalleyStableUnder e S T) (A : CommAlgCat ℤ) :
      ((kostantSubsystemSubgroup e h ρ M hM hnil S A).subgroupOf (kostantSubsystemSubgroup e h ρ M hM hnil T A)).Normal

      A Chevalley-stable index set contained in T is normal in the subsystem subgroup of T.

      source
      theorem TauCeti.UniversalEnvelopingAlgebra.isNilpotent_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)))) {S : Set ι} {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) (A : CommAlgCat ℤ) :
      Group.IsNilpotent ↥(kostantSubsystemSubgroup e h ρ M hM hnil S A)

      The unipotent group of a class-two graded closed set of roots is nilpotent. Suppose every index of S has height at most N, and that whenever two root vectors indexed in S fail to commute their bracket is an integer multiple of a third root vector, indexed in S, of strictly larger height and central for both. Then U_S(A) is nilpotent over every value ring.

      The height hypothesis is only stated for the first of the two indices; the second one comes for free by reading it at the swapped pair, whose bracket is the negative.

      For a simply-laced Chevalley system and S the positive roots this is the class-two model of the positive-root subgroup, with ht the height of a root and N the height of the highest root. The identification of that subgroup with the unipotent radical of a Borel subgroup needs a pinning and is not part of this statement; longer root strings in non-simply-laced systems are not covered.