Special and extraspecial pairs of roots

Fix a base b of a reduced crystallographic root pairing together with a linear order on the root indices that is additive: adding a positive root to a positive root moves an index strictly upwards. A special pair is a pair of positive roots α ≺ β whose sum is again a root, and a special pair is extraspecial when its first member is as small as possible among the special pairs with the same sum.

The point of the notion is the enumeration proved here: a positive root is the sum of an extraspecial pair exactly when it is not simple, and that pair is then unique. Carter's construction of a Chevalley basis chooses the sign of one structure constant N(α, β) for each extraspecial pair and determines every remaining structure constant by recursion over the sum α + β, which is why the two members of the pair lying strictly below their sum is recorded here beside the enumeration. Counting the pairs, there are |Φ⁺| - ℓ of them, one for each non-simple positive root.

Additivity of the order is used only for those strict inequalities: existence and uniqueness of the extraspecial pair with a prescribed sum hold for an arbitrary linear order on the indices, and are stated that way.

Main definitions

• TauCeti.IsAdditiveRootOrder: a linear order on root indices that increases strictly when a positive root is added to a positive root.
• TauCeti.IsSpecialPair: an ordered pair of positive roots whose sum is a root.
• TauCeti.IsExtraspecialPair: a special pair whose first member is smallest among the special pairs with the same sum.
• TauCeti.extraspecialPairs: the set of all extraspecial pairs.

Main results

• TauCeti.exists_isAdditiveRootOrder: additive orders exist, so the hypothesis is not vacuous. Ordering by height and breaking ties arbitrarily is one.
• TauCeti.exists_isSpecialPair_root_eq_add: a positive root that is not simple is the sum of a special pair.
• TauCeti.existsUnique_isExtraspecialPair: a positive root that is not simple is the sum of exactly one extraspecial pair.
• TauCeti.exists_isExtraspecialPair_lt: in an additive order both members of that pair lie strictly below the sum, which is the recursion step Carter's construction runs on.
• TauCeti.IsExtraspecialPair.le_of_isPos: the first member of an extraspecial pair is smallest among the first members of all decompositions of its sum into two positive roots, ordered or not.
• TauCeti.ncard_extraspecialPairs: there are |Φ⁺| - ℓ extraspecial pairs.

References

• R. W. Carter, Simple Groups of Lie Type, §4.2.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25.2.

Roadmap

Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md asks for the split reductive group scheme over ℤ to be built "via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra". TauCeti.IsChevalleySystem of TauCeti/Algebra/Lie/Weights/Chevalley/System.lean is that Chevalley basis, carried as a hypothesis, and TauCeti.IsSl2System.isChevalleyNormalized_iff_exists_isChevalleySystem of TauCeti/Algebra/Lie/Weights/Chevalley/Involution.lean reduces producing one to normalising the structure constants to ±(p + 1). Carter's §4.2 performs that normalisation by recursion over the extraspecial pairs enumerated here. Milestone L0 of TauCetiRoadmap/CFSGStatement/README.md is the downstream consumer of the assembled pinned group scheme.

structure TauCeti.IsAdditiveRootOrder {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [l : LinearOrder ι] (b : P.Base) : Prop

A linear order on the root index type is an additive root order for a base b when adding a positive root to a positive root strictly increases the index: if α and β are positive roots whose sum γ is again a root, then the index of α lies strictly below the index of γ.

Carter orders the roots by a linear functional that is positive on the positive roots, which is additive in this sense. Only this consequence of that choice is used below, so it is the hypothesis carried here; TauCeti.exists_isAdditiveRootOrder shows that such orders exist.

• lt_of_root_eq_add {i j k : ι} (hi : b.IsPos i) (hj : b.IsPos j) (hk : P.root k = P.root i + P.root j) : i < k

  Adding a positive root to a positive root strictly increases the index.

theorem TauCeti.exists_isAdditiveRootOrder {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} (b : P.Base) : ∃ (l : LinearOrder ι), IsAdditiveRootOrder P b

Additive root orders exist. Ordering the indices by the height of their root and breaking ties by an arbitrary well-order gives one: heights add, and a positive root has height at least one.

The order is passed to TauCeti.IsAdditiveRootOrder as an explicit argument here, because it is the object asserted to exist rather than an instance available in the context.

structure TauCeti.IsSpecialPair {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [LinearOrder ι] (b : P.Base) (i j : ι) : Prop

A special pair for a base b and a linear order on the root indices is a pair of positive roots, the first strictly below the second, whose sum is again a root.

• isPos_left : b.IsPos i

  The first root of a special pair is positive.

• isPos_right : b.IsPos j

  The second root of a special pair is positive.

• lt : i < j

  The first root of a special pair lies strictly below the second.

• add_mem_range : P.root i + P.root j ∈ Set.range ⇑P.root

  The sum of the two roots of a special pair is again a root.

structure TauCeti.IsExtraspecialPair {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [LinearOrder ι] (b : P.Base) (i j : ι) extends TauCeti.IsSpecialPair P b i j : Prop

A special pair is extraspecial when its first root is smallest, in the chosen order, among the first roots of all the special pairs with the same sum.

• isPos_left : b.IsPos i
• isPos_right : b.IsPos j
• lt : i < j
• add_mem_range : P.root i + P.root j ∈ Set.range ⇑P.root
• le_left (i' j' : ι) : IsSpecialPair P b i' j' → P.root i' + P.root j' = P.root i + P.root j → i ≤ i'

  No special pair with the same sum has a smaller first root.

theorem TauCeti.IsSpecialPair.ne {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} {i j : ι} (h : IsSpecialPair P b i j) : i ≠ j

The two roots of a special pair are distinct, since one lies strictly below the other.

theorem TauCeti.IsSpecialPair.isPos {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} {i j k : ι} (h : IsSpecialPair P b i j) (hk : P.root k = P.root i + P.root j) : b.IsPos k

The sum of a special pair is a positive root.

theorem TauCeti.IsSpecialPair.notMem_support {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} {i j k : ι} (h : IsSpecialPair P b i j) (hk : P.root k = P.root i + P.root j) : k ∉ b.support

The sum of a special pair is never a simple root.

theorem TauCeti.IsSpecialPair.left_lt {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} {i j k : ι} (hb : IsAdditiveRootOrder P b) (h : IsSpecialPair P b i j) (hk : P.root k = P.root i + P.root j) : i < k

In an additive order the first root of a special pair lies strictly below the sum.

theorem TauCeti.IsSpecialPair.right_lt {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} {i j k : ι} (hb : IsAdditiveRootOrder P b) (h : IsSpecialPair P b i j) (hk : P.root k = P.root i + P.root j) : j < k

In an additive order the second root of a special pair lies strictly below the sum.

theorem TauCeti.ne_of_root_eq_add {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [IsDomain R] [P.IsReduced] {i j k : ι} (hk : P.root k = P.root i + P.root j) : i ≠ j

Two roots whose sum is a root are distinct: in a reduced pairing, twice a root is never a root.

theorem TauCeti.isSpecialPair_or_swap {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} [IsDomain R] [P.IsReduced] {i j k : ι} (hi : b.IsPos i) (hj : b.IsPos j) (hk : P.root k = P.root i + P.root j) : IsSpecialPair P b i j ∨ IsSpecialPair P b j i

Two positive roots whose sum is a root are the two members of a special pair, taken in one order or the other.

theorem TauCeti.IsExtraspecialPair.le_of_isPos {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} [IsDomain R] [P.IsReduced] {i j i' j' : ι} (h : IsExtraspecialPair P b i j) (hi' : b.IsPos i') (hj' : b.IsPos j') (hsum : P.root i' + P.root j' = P.root i + P.root j) : i ≤ i'

The first root of an extraspecial pair is smallest among the first roots of all the decompositions of its sum into two positive roots, ordered or not.

theorem TauCeti.IsExtraspecialPair.eq_of_root_add_eq {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} {i j i' j' : ι} (h : IsExtraspecialPair P b i j) (h' : IsExtraspecialPair P b i' j') (hsum : P.root i' + P.root j' = P.root i + P.root j) : i' = i ∧ j' = j

An extraspecial pair is determined by its sum.

theorem TauCeti.exists_isSpecialPair_root_eq_add {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} [IsDomain R] [P.IsReduced] [Finite ι] [P.IsCrystallographic] {k : ι} (hk : b.IsPos k) (hk' : k ∉ b.support) : ∃ (i : ι) (j : ι), IsSpecialPair P b i j ∧ P.root k = P.root i + P.root j

A positive root that is not simple is the sum of a special pair.

theorem TauCeti.exists_isExtraspecialPair {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} [IsDomain R] [P.IsReduced] [Finite ι] [P.IsCrystallographic] {k : ι} (hk : b.IsPos k) (hk' : k ∉ b.support) : ∃ (i : ι) (j : ι), IsExtraspecialPair P b i j ∧ P.root k = P.root i + P.root j

A positive root that is not simple is the sum of an extraspecial pair. The pair is found by minimising the first member over the special pairs with the prescribed sum.

theorem TauCeti.existsUnique_isExtraspecialPair {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} [IsDomain R] [P.IsReduced] [Finite ι] [P.IsCrystallographic] {k : ι} (hk : b.IsPos k) (hk' : k ∉ b.support) : ∃! p : ι × ι, IsExtraspecialPair P b p.1 p.2 ∧ P.root k = P.root p.1 + P.root p.2

A positive root that is not simple is the sum of exactly one extraspecial pair.

theorem TauCeti.exists_isExtraspecialPair_lt {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] {b : P.Base} [IsDomain R] [P.IsReduced] [Finite ι] [P.IsCrystallographic] (hb : IsAdditiveRootOrder P b) {k : ι} (hk : b.IsPos k) (hk' : k ∉ b.support) : ∃ (i : ι) (j : ι), IsExtraspecialPair P b i j ∧ P.root k = P.root i + P.root j ∧ i < k ∧ j < k

The recursion step behind Carter's construction of a Chevalley basis. In an additive order a positive root that is not simple is the sum of a unique extraspecial pair, and both members of that pair lie strictly below it. A structure constant attached to a root can therefore be defined by recursion along the order, with the extraspecial pairs carrying the free sign choices.

def TauCeti.extraspecialPairs {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [LinearOrder ι] (b : P.Base) : Set (ι × ι)

The set of extraspecial pairs of a base, relative to a linear order on the root indices.

Equations

• TauCeti.extraspecialPairs P b = {p : ι × ι | TauCeti.IsExtraspecialPair P b p.1 p.2}

@[simp]

theorem TauCeti.mem_extraspecialPairs {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] (P : RootPairing ι R M N) [LinearOrder ι] (b : P.Base) {p : ι × ι} : p ∈ extraspecialPairs P b ↔ IsExtraspecialPair P b p.1 p.2

theorem TauCeti.bijOn_add_extraspecialPairs {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) : Set.BijOn (fun (p : ι × ι) => P.root p.1 + P.root p.2) (extraspecialPairs P b) (⇑P.root '' (posRoots P b \ ↑b.support))

Extraspecial pairs biject with the non-simple positive roots, by taking the sum.

theorem TauCeti.ncard_extraspecialPairs {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [CharZero R] {P : RootPairing ι R M N} [LinearOrder ι] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) : (extraspecialPairs P b).ncard = (posRoots P b).ncard - b.support.card

There are |Φ⁺| - ℓ extraspecial pairs, one for each positive root that is not simple.