A base of the diagonal root datum of the general linear group

For GL_(n+1), the consecutive coordinate differences

α_i = e_i - e_(i+1),  0 ≤ i < n,

form a base of the diagonal root datum. Every coordinate root e_a - e_b is a sum of these simple roots or the negative of such a sum, by telescoping. The same statement holds for the coroots. The simple roots are linearly independent: summing the first i + 1 coordinates sends α_i to the i-th standard basis vector.

The resulting Cartan matrix is CartanMatrix.A n. Thus the diagonal root datum already attached to the standard maximal torus of GL_(n+1) carries the expected Bourbaki-numbered base of type A_n, providing the positive-root input for standard Borels and Bruhat theory.

Main declarations

• TauCeti.GeneralLinear.diagonalSimpleRootIndex: the root index of e_i - e_(i+1).
• TauCeti.GeneralLinear.diagonalRootBase: the consecutive coordinate roots as a base.
• TauCeti.GeneralLinear.diagonalRootBase_isPos_iff: positive diagonal roots are exactly the coordinate differences e_i - e_j with i < j.
• TauCeti.GeneralLinear.hasCartanType_diagonalRootDatum: this base has Cartan type A_n.

References

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

The support and telescoping organization follows TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.A, adapted here to the character and cocharacter lattices of the diagonal torus in GL_(n+1). This advances Layer 7, "Root datum of (G, T)", of the ReductiveGroups roadmap.

def TauCeti.GeneralLinear.diagonalSimpleRootIndex (n : ℕ) (i : Fin n) : DiagonalRootIndex (n + 1)

The index of the i-th simple root e_i - e_(i+1) in the diagonal root datum of GL_(n+1).

Equations

• TauCeti.GeneralLinear.diagonalSimpleRootIndex n i = ⟨({ down := i.castSucc }, { down := i.succ }), ⋯⟩

@[simp]

theorem TauCeti.GeneralLinear.diagonalSimpleRootIndex_fst (n : ℕ) (i : Fin n) : (↑(diagonalSimpleRootIndex n i)).1 = { down := i.castSucc }

The first coordinate of the i-th diagonal simple-root index is i.

@[simp]

theorem TauCeti.GeneralLinear.diagonalSimpleRootIndex_snd (n : ℕ) (i : Fin n) : (↑(diagonalSimpleRootIndex n i)).2 = { down := i.succ }

The second coordinate of the i-th diagonal simple-root index is i + 1.

theorem TauCeti.GeneralLinear.diagonalSimpleRootIndex_injective (n : ℕ) : Function.Injective (diagonalSimpleRootIndex n)

Distinct nodes give distinct diagonal simple-root indices.

theorem TauCeti.GeneralLinear.diagonalRootDatum_root_diagonalSimpleRootIndex (n : ℕ) (i : Fin n) : (diagonalRootDatum (n + 1)).root (diagonalSimpleRootIndex n i) = SplitTorus.coordinateRoot { down := i.castSucc } { down := i.succ }

The root at the i-th diagonal simple-root index is the consecutive coordinate root e_i - e_(i+1).

theorem TauCeti.GeneralLinear.diagonalRootDatum_coroot_diagonalSimpleRootIndex (n : ℕ) (i : Fin n) : (diagonalRootDatum (n + 1)).coroot (diagonalSimpleRootIndex n i) = SplitTorus.coordinateCoroot { down := i.castSucc } { down := i.succ }

The coroot at the i-th diagonal simple-root index is the consecutive coordinate coroot e_i - e_(i+1).

noncomputable def TauCeti.GeneralLinear.diagonalRootBase (n : ℕ) : RootPairing.Base (diagonalRootDatum (n + 1))

The Bourbaki-numbered base of the diagonal root datum of GL_(n+1), supported on the consecutive coordinate roots e_i - e_(i+1).

Equations

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

theorem TauCeti.GeneralLinear.diagonalRootBase_support (n : ℕ) : (diagonalRootBase n).support = simpleSupport ⋯

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

@[simp]

theorem TauCeti.GeneralLinear.mem_diagonalRootBase_support (n : ℕ) (p : DiagonalRootIndex (n + 1)) : p ∈ (diagonalRootBase n).support ↔ ∃ (i : Fin n), diagonalSimpleRootIndex n i = p

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

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootBase_isPos_iff (n : ℕ) (p : DiagonalRootIndex (n + 1)) : (diagonalRootBase n).IsPos p ↔ (↑p).1.down < (↑p).2.down

A diagonal root is positive for the consecutive-root base exactly when its row index is strictly smaller than its column index.

theorem TauCeti.GeneralLinear.diagonalRootDatum_pairing_diagonalSimpleRootIndex (n : ℕ) (i j : Fin n) : RootPairing.pairing (diagonalRootDatum (n + 1)) (diagonalSimpleRootIndex n i) (diagonalSimpleRootIndex n j) = CartanMatrix.A n i j

The simple-root pairings in the diagonal root datum are the entries of the type-A Cartan matrix.

theorem TauCeti.GeneralLinear.hasCartanType_diagonalRootDatum (n : ℕ) : HasCartanType (diagonalRootDatum (n + 1)) (diagonalRootBase n) (DynkinType.A n)

The diagonal root datum of GL_(n+1), with its consecutive-root base, has Cartan type A_n.