Documentation

TauCeti.RepresentationTheory.ClassicalGroups.Torus

The diagonal torus in the standard representation #

The diagonal torus TauCeti.diagonalTorus k n of GL n k, the subgroup of invertible diagonal matrices, is built in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Diagonal.Basic, where its three descriptions — as the range of TauCeti.diagGL, by diagonality of the matrix, and as its own centralizer — are proved. What is recorded here is its action on the coordinate lines k ∙ eᵢ of the standard representation: every torus element scales eᵢ by its i-th diagonal entry (TauCeti.stdRep_apply_basisFun_of_mem_diagonalTorus), so each line is stable (TauCeti.map_stdRep_span_basisFun).

Over a general k these lines are not yet the weight spaces of the torus: that identification needs the coordinate characters to be pairwise distinct, and it fails outright when the torus is trivial, as it is over 𝔽₂ (TauCeti.diagonalTorus_eq_bot).

Main statements #

References #

source
theorem TauCeti.stdRep_apply_basisFun_of_mem_diagonalTorus {k : Type u} [CommRing k] {n : ℕ} {g : GL (Fin n) k} (hg : g ∈ diagonalTorus k n) (i : Fin n) :
((stdRep k n) g) ((Pi.basisFun k (Fin n)) i) = ↑g i i • (Pi.basisFun k (Fin n)) i

An element of the diagonal torus scales the standard basis vector eᵢ by its (i, i) matrix entry, the i-th coordinate character of the torus read off diagGL through TauCeti.diagonalTorusEquiv. This is an eigen-relation rather than an eigenvector statement: over the zero ring eᵢ itself vanishes.

source
theorem TauCeti.map_stdRep_span_basisFun {k : Type u} [CommRing k] {n : ℕ} {g : GL (Fin n) k} (hg : g ∈ diagonalTorus k n) (i : Fin n) :
Submodule.map ((stdRep k n) g) (k ∙ (Pi.basisFun k (Fin n)) i) = k ∙ (Pi.basisFun k (Fin n)) i

Each coordinate line of the standard representation is stable under the diagonal torus, a torus element acting on it by the invertible scalar given by its i-th diagonal entry.