Restricting a rational function on GL n R to the diagonal torus

A rational function on GL n R restricts along the diagonal embedding TauCeti.diagGL to a Laurent function on the torus (TauCeti.comp_diagGL_mem_laurentFunctions). The determinant becomes the product of the coordinates, hence a character, so inverting a power of it stays inside the algebra; a polynomial in the matrix entries becomes a polynomial in the coordinates, because an off-diagonal entry of a diagonal matrix vanishes and a diagonal one is a coordinate.

This is the step that lets the weight theory of GL n k be run inside the algebra of Laurent functions built in TauCeti.LinearAlgebra.Basis.DiagonalTorus.LaurentFunctions, where distinct characters are linearly independent and a weight can therefore be read off an expansion.

Main results

• TauCeti.eval_diagGL_mem_laurentFunctions: a polynomial in the matrix entries restricts to a Laurent function on the diagonal torus.
• TauCeti.comp_diagGL_mem_laurentFunctions: so does a rational function on GL n R.

References

• Classical groups roadmap, Layer 3, "The maximal torus and weight spaces".
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.

theorem TauCeti.entry_diagGL_mem_laurentFunctions {R : Type u} [CommRing R] {n : ℕ} (p : Fin n × Fin n) : (fun (t : Fin n → Rˣ) => ↑(diagGL t) p.1 p.2) ∈ laurentFunctions R (Fin n)

A matrix entry of a diagonal matrix, as a function of the point of the torus, is a Laurent function: off the diagonal it vanishes, and on the diagonal it is a coordinate.

theorem TauCeti.eval_diagGL_mem_laurentFunctions {R : Type u} [CommRing R] {n : ℕ} (P : MvPolynomial (Fin n × Fin n) R) : (fun (t : Fin n → Rˣ) => (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑(diagGL t) p.1 p.2) P) ∈ laurentFunctions R (Fin n)

A polynomial in the matrix entries restricts along the diagonal embedding to a Laurent function on the torus.

theorem TauCeti.comp_diagGL_mem_laurentFunctions {R : Type u} [CommRing R] {n : ℕ} {f : GL (Fin n) R → R} (hf : f ∈ Matrix.GeneralLinearGroup.rationalFunctions R n) : (fun (t : Fin n → Rˣ) => f (diagGL t)) ∈ laurentFunctions R (Fin n)

A rational function on GL n R restricts to a Laurent function on the diagonal torus. The determinant of a diagonal matrix is the product of its coordinates, so the denominator is an inverted character and stays inside the algebra, while the numerator is handled by TauCeti.eval_diagGL_mem_laurentFunctions.