A base of the root datum of the symplectic group

For Sp₂ₘ with its paired diagonal torus, the roots

α_i = e_i - e_(i+1),  0 ≤ i < m - 1,      α_(m-1) = 2 e_(m-1)

form a base of TauCeti.Symplectic.diagonalRootDatum, with simple coroots e_i - e_(i+1) and e_(m-1).

The resulting Cartan matrix is CartanMatrix.C m. The positive roots are exactly the positive long roots 2 e_i, the positive sums e_i + e_j, and the differences e_i - e_j with i < j.

The base equips the diagonal root datum with its simple and positive roots. This is what allows it to be compared with the pinned type-C root datum up to a labelling of the simple roots, and what supplies the positive roots underlying a Borel subgroup and the Bruhat theory of Sp₂ₘ.

Main declarations

• TauCeti.Symplectic.diagonalSimpleRootIndex: the root subgroup of the i-th simple root.
• TauCeti.Symplectic.diagonalRootBase: the Bourbaki-numbered base of the diagonal root datum.
• TauCeti.Symplectic.mem_diagonalRootBase_support: its support consists of the simple indices.
• TauCeti.Symplectic.hasCartanType_diagonalRootDatum: this base has Cartan type Cₘ.
• TauCeti.Symplectic.diagonalRootBase_isPos_positiveLong and its companions: the positive roots of this base.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Section 12.1.

The organization follows TauCeti.GeneralLinear.diagonalRootBase for the diagonal torus of GL_(n+1).

The simple root indices

def TauCeti.Symplectic.diagonalSimpleRootIndex (m : ℕ) (i : Fin m) : GLSymplecticFin.RootSubgroupIndex m

The root subgroup of the i-th simple root of Sp₂ₘ in Bourbaki numbering: the difference root e_i - e_(i+1) before the last node, and the long root 2 e_(m-1) at the last node.

Equations

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

theorem TauCeti.Symplectic.diagonalSimpleRootIndex_of_lt {m : ℕ} (i : Fin m) (h : ↑i + 1 < m) : diagonalSimpleRootIndex m i = GLSymplecticFin.RootSubgroupIndex.difference i ⟨↑i + 1, h⟩ ⋯

Before the last node, the simple root is the difference root e_i - e_(i+1).

theorem TauCeti.Symplectic.diagonalSimpleRootIndex_of_not_lt {m : ℕ} (i : Fin m) (h : ¬↑i + 1 < m) : diagonalSimpleRootIndex m i = GLSymplecticFin.RootSubgroupIndex.positiveLong i

At the last node, the simple root is the long root 2 e_(m-1).

theorem TauCeti.Symplectic.diagonalSimpleRootIndex_injective (m : ℕ) : Function.Injective (diagonalSimpleRootIndex m)

Distinct nodes have distinct simple roots.

Linear independence of the simple roots and coroots

The base

noncomputable def TauCeti.Symplectic.diagonalRootBase (m : ℕ) : RootPairing.Base (diagonalRootDatum m)

The Bourbaki-numbered base of the root datum of Sp₂ₘ relative to its diagonal torus, supported on the roots e_i - e_(i+1) for i < m - 1 and 2 e_(m-1).

Equations

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

theorem TauCeti.Symplectic.diagonalRootBase_support (m : ℕ) : (diagonalRootBase m).support = simpleSupport ⋯

The support of the diagonal base is the image of the simple-root index map.

@[simp]

theorem TauCeti.Symplectic.mem_diagonalRootBase_support {m : ℕ} (p : GLSymplecticFin.RootSubgroupIndex m) : p ∈ (diagonalRootBase m).support ↔ ∃ (i : Fin m), diagonalSimpleRootIndex m i = p

A root index belongs to the diagonal base exactly when it is one of the simple indices.

The Cartan type

theorem TauCeti.Symplectic.diagonalRootDatum_pairing_diagonalSimpleRootIndex {m : ℕ} (i j : Fin m) : RootPairing.pairing (diagonalRootDatum m) (diagonalSimpleRootIndex m i) (diagonalSimpleRootIndex m j) = CartanMatrix.C m i j

The pairings of the simple roots of the diagonal root datum are the entries of the type-C Cartan matrix.

theorem TauCeti.Symplectic.hasCartanType_diagonalRootDatum (m : ℕ) : HasCartanType (diagonalRootDatum m) (diagonalRootBase m) (DynkinType.C m)

The diagonal root datum of Sp₂ₘ, with its Bourbaki-numbered base, has Cartan type Cₘ.

The positive roots

@[simp]

theorem TauCeti.Symplectic.diagonalRootBase_isPos_positiveLong {m : ℕ} (i : Fin m) : (diagonalRootBase m).IsPos (GLSymplecticFin.RootSubgroupIndex.positiveLong i)

The long root 2 eᵢ is positive.

@[simp]

theorem TauCeti.Symplectic.not_diagonalRootBase_isPos_negativeLong {m : ℕ} (i : Fin m) : ¬(diagonalRootBase m).IsPos (GLSymplecticFin.RootSubgroupIndex.negativeLong i)

The long root -2 eᵢ is not positive.

@[simp]

theorem TauCeti.Symplectic.diagonalRootBase_isPos_positiveSum {m : ℕ} {i j : Fin m} (hij : i < j) : (diagonalRootBase m).IsPos (GLSymplecticFin.RootSubgroupIndex.positiveSum i j hij)

The sum root eᵢ + eⱼ is positive.

@[simp]

theorem TauCeti.Symplectic.not_diagonalRootBase_isPos_negativeSum {m : ℕ} {i j : Fin m} (hij : i < j) : ¬(diagonalRootBase m).IsPos (GLSymplecticFin.RootSubgroupIndex.negativeSum i j hij)

The sum root -(eᵢ + eⱼ) is not positive.

@[simp]

theorem TauCeti.Symplectic.diagonalRootBase_isPos_difference_iff {m : ℕ} {i j : Fin m} (hij : i ≠ j) : (diagonalRootBase m).IsPos (GLSymplecticFin.RootSubgroupIndex.difference i j hij) ↔ i < j

The difference root eᵢ - eⱼ is positive exactly when i < j.