The diagonal root datum and the adjoint roots of the general linear group

For GL_n with its diagonal split torus, the coordinate root datum has roots e_i - e_j, indexed by ordered pairs i ≠ j. Independently, the nontrivial weights of the restricted adjoint representation have been classified as the same characters. This file identifies the two constructions exactly.

Thus the roots packaged by GeneralLinear.diagonalRootDatum are neither merely an abstract coordinate model nor just a subset of the adjoint weights: their range is the complete set Derivation.nontrivialAdjointWeights for the diagonal-torus morphism. The induced equivalence records the canonical root indexing. The existing adjoint classification then identifies each root space with the line spanned by the corresponding matrix unit E_ij.

This is a worked-example bridge between two concrete constructions. It does not assert that the diagonal torus is maximal or construct the general root datum of a reductive pair.

Main declarations

• TauCeti.GeneralLinear.mem_nontrivialAdjointWeights_iff_exists_diagonalRoot: a character is a nontrivial adjoint weight exactly when it is a root of the diagonal root datum.
• TauCeti.GeneralLinear.range_ofAdd_diagonalRootDatum_root_eq_nontrivialAdjointWeights: the packaged root set equals the adjoint root set.
• TauCeti.GeneralLinear.diagonalRootIndexEquivNontrivialAdjointWeights: the canonical equivalence from root indices to nontrivial adjoint weights.

References

• J. S. Milne, Algebraic Groups (2017), Example 19.7 and Section 21.1.
• J. E. Humphreys, Linear Algebraic Groups (1975), Sections 16.1 and 26.3.

This supplies the root-set computation for the standard split GL_n worked example in Layer 7, "Root datum of (G, T)", of the ReductiveGroups roadmap. Proving maximality of the diagonal torus, constructing root data for arbitrary split reductive pairs, and identifying their Weyl groups remain separate milestones.

theorem TauCeti.GeneralLinear.mem_nontrivialAdjointWeights_iff_exists_diagonalRoot {k : Type u} [Field k] {n : ℕ} (alpha : Multiplicative (ULift.{u, 0} (Fin n) →₀ ℤ)) : alpha ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) ↔ ∃ (p : DiagonalRootIndex n), alpha = Multiplicative.ofAdd ((diagonalRootDatum n).root p)

A character of the diagonal torus is a nontrivial adjoint weight exactly when it is the multiplicative form of a root in diagonalRootDatum.

theorem TauCeti.GeneralLinear.range_ofAdd_diagonalRootDatum_root_eq_nontrivialAdjointWeights {k : Type u} [Field k] {n : ℕ} : (Set.range fun (p : DiagonalRootIndex n) => Multiplicative.ofAdd ((diagonalRootDatum n).root p)) = Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap)

The multiplicative roots of the diagonal coordinate root datum are exactly the nontrivial adjoint weights of GL_n relative to its diagonal torus.

noncomputable def TauCeti.GeneralLinear.diagonalRootIndexEquivNontrivialAdjointWeights {k : Type u} [Field k] {n : ℕ} : DiagonalRootIndex n ≃ { alpha : Multiplicative (ULift.{u, 0} (Fin n) →₀ ℤ) // alpha ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) }

The root indices of the diagonal coordinate root datum are canonically equivalent to the nontrivial adjoint weights of GL_n relative to its diagonal torus.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootIndexEquivNontrivialAdjointWeights_apply {k : Type u} [Field k] {n : ℕ} (p : DiagonalRootIndex n) : ↑(diagonalRootIndexEquivNontrivialAdjointWeights p) = Multiplicative.ofAdd ((diagonalRootDatum n).root p)

The root-index equivalence sends an index to the multiplicative form of its packaged root.