Diagonal elements in the standard representation

This file describes the action of the invertible diagonal matrices TauCeti.diagGL t in the standard representation. These elements are the concrete points of the diagonal torus used to compute characters and weight spaces; the matrices themselves, and the torus they form, are in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Diagonal.Basic.

Main statements

• TauCeti.stdRep_diagGL_apply_basisFun: every standard basis vector is an eigenvector of a diagonal matrix.

References

• Classical groups roadmap, Layer 1.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.

@[simp]

theorem TauCeti.stdRep_diagGL_apply {k : Type u} [CommRing k] {n : ℕ} (t : Fin n → kˣ) (v : Fin n → k) (i : Fin n) : ((stdRep k n) (diagGL t)) v i = ↑(t i) * v i

The standard representation acts at diagGL t by coordinatewise multiplication.

@[simp]

theorem TauCeti.stdRep_diagGL_apply_basisFun {k : Type u} [CommRing k] {n : ℕ} (t : Fin n → kˣ) (i : Fin n) : ((stdRep k n) (diagGL t)) ((Pi.basisFun k (Fin n)) i) = ↑(t i) • (Pi.basisFun k (Fin n)) i

Every standard basis vector is an eigenvector for a diagonal matrix.