The simple roots of the special linear group

The roots ε_i - ε_(i+1) form the Bourbaki-numbered base of the diagonal root datum of SL_{r+1}. Its Cartan matrix is CartanMatrix.A r, and its positive roots are precisely ε_a - ε_b with a < b. This fixes the choice of positive roots corresponding to upper triangular matrices, for use in the standard Borel and Weyl-group descriptions.

Under diagonalRootDatumEquiv, this base corresponds to DynkinType.typeASimplyConnectedBase.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate I.
• J. S. Milne, Algebraic Groups (2017), §21, Example 21.2.

def TauCeti.SpecialLinear.diagonalSimpleRootIndex (r : ℕ) (i : Fin r) : SplitTorus.CoordinateRootIndex (Fin (r + 1))

The root index of the i-th simple root ε_i - ε_(i+1) of SL_{r+1}.

Equations

• TauCeti.SpecialLinear.diagonalSimpleRootIndex r i = ⟨(i.castSucc, i.succ), ⋯⟩

@[simp]

theorem TauCeti.SpecialLinear.diagonalSimpleRootIndex_fst (r : ℕ) (i : Fin r) : (↑(diagonalSimpleRootIndex r i)).1 = i.castSucc

@[simp]

theorem TauCeti.SpecialLinear.diagonalSimpleRootIndex_snd (r : ℕ) (i : Fin r) : (↑(diagonalSimpleRootIndex r i)).2 = i.succ

theorem TauCeti.SpecialLinear.diagonalSimpleRootIndex_injective (r : ℕ) : Function.Injective (diagonalSimpleRootIndex r)

The consecutive-root indexing is injective.

noncomputable def TauCeti.SpecialLinear.diagonalRootBase (r : ℕ) : RootPairing.Base (diagonalRootDatum r)

The Bourbaki base of the diagonal root datum of SL_{r+1}.

Equations

• TauCeti.SpecialLinear.diagonalRootBase r = (TauCeti.DynkinType.typeASimplyConnectedBase r).map (TauCeti.SpecialLinear.diagonalRootDatumEquiv r)

@[simp]

theorem TauCeti.SpecialLinear.mem_diagonalRootBase_support (r : ℕ) (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : p ∈ (diagonalRootBase r).support ↔ ∃ (i : Fin r), diagonalSimpleRootIndex r i = p

The base consists exactly of the consecutive coordinate differences.

theorem TauCeti.SpecialLinear.diagonalRootBase_support (r : ℕ) : (diagonalRootBase r).support = simpleSupport ⋯

The support is the image of the Bourbaki simple-root indexing.

theorem TauCeti.SpecialLinear.diagonalRootDatum_pairing_diagonalSimpleRootIndex (r : ℕ) (i j : Fin r) : RootPairing.pairing (diagonalRootDatum r) (diagonalSimpleRootIndex r i) (diagonalSimpleRootIndex r j) = CartanMatrix.A r i j

The simple-root pairings are the entries of the type-A_r Cartan matrix.

theorem TauCeti.SpecialLinear.hasCartanType_diagonalRootDatum (r : ℕ) : HasCartanType (diagonalRootDatum r) (diagonalRootBase r) (DynkinType.A r)

The diagonal root datum of SL_{r+1} with its consecutive-root base has Cartan type A_r.

@[simp]

theorem TauCeti.SpecialLinear.diagonalRootBase_isPos_iff (r : ℕ) (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) : (diagonalRootBase r).IsPos p ↔ (↑p).1 < (↑p).2

A root of the diagonal torus of SL_{r+1} is positive exactly when its row index is smaller than its column index.