Laurent functions on a split torus

The characters of the split torus 𝔾ₘ^κ span a subalgebra of the R-valued functions on its points, the Laurent functions TauCeti.laurentFunctions R κ: over a field these are exactly the functions given by a Laurent polynomial in the coordinates. This file builds that subalgebra and proves that the characters spanning it are linearly independent.

Independence is what makes the construction useful. Distinct characters of a monoid with values in a domain are linearly independent (Artin), so TauCeti.linearIndependent_weightCharHom turns an identity between two Laurent expansions into an identity between their coefficients. This is the mechanism by which a weight is read off an expansion, and it is why the weight spaces of a rational representation of GL n k are what they are; the restriction of a rational function to the diagonal torus, which is where that argument starts, is in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.LaurentFunctions.

The value ring is a commutative ring throughout, except where separating characters forces an infinite field: over 𝔽₂ the torus has a single point and all characters coincide.

Main definitions

• TauCeti.weightCharHom: a character of the split torus, with values read in R rather than in Rˣ.
• TauCeti.laurentFunctions: the subalgebra of functions on the torus spanned by the characters.

Main results

• TauCeti.linearIndependent_weightCharHom: over an infinite field the characters of the split torus are linearly independent, so a Laurent expansion determines its coefficients.

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.

def TauCeti.weightCharHom (R : Type u) [CommRing R] {κ : Type v} [Fintype κ] (μ : κ → ℤ) : (κ → Rˣ) →* R

A character of the split torus 𝔾ₘ^κ with its values read in R rather than in Rˣ. This is the form in which a character is a function on the torus, so that families of characters can be asked to be linearly independent and their span can be taken.

Equations

• TauCeti.weightCharHom R μ = (Units.coeHom R).comp (TauCeti.weightChar R μ)

@[simp]

theorem TauCeti.weightCharHom_apply (R : Type u) [CommRing R] {κ : Type v} [Fintype κ] (μ : κ → ℤ) (s : κ → Rˣ) : (weightCharHom R μ) s = ↑((weightChar R μ) s)

@[simp]

theorem TauCeti.coe_weightCharHom_zero (R : Type u) [CommRing R] {κ : Type v} [Fintype κ] : ⇑(weightCharHom R 0) = 1

The trivial character is the constant function 1.

theorem TauCeti.coe_weightCharHom_add (R : Type u) [CommRing R] {κ : Type v} [Fintype κ] (μ ν : κ → ℤ) : ⇑(weightCharHom R (μ + ν)) = ⇑(weightCharHom R μ) * ⇑(weightCharHom R ν)

Characters multiply as their weights add.

theorem TauCeti.weightCharHom_single (R : Type u) [CommRing R] {κ : Type v} [Fintype κ] [DecidableEq κ] (c : κ) (s : κ → Rˣ) : (weightCharHom R (Pi.single c 1)) s = ↑(s c)

The character of Pi.single c 1 is the c-th coordinate function. Not a simp lemma: TauCeti.weightCharHom_apply and TauCeti.weightChar_single already reduce the left-hand side, so tagging it would make it simp-redundant.

theorem TauCeti.weightCharHom_const (R : Type u) [CommRing R] {κ : Type v} [Fintype κ] (z : ℤ) (s : κ → Rˣ) : (weightCharHom R fun (x : κ) => z) s = ↑((∏ j : κ, s j) ^ z)

The character of a constant weight is the corresponding power of the product of the coordinates.

def TauCeti.laurentFunctions (R : Type u) [CommRing R] (κ : Type v) [Fintype κ] : Subalgebra R ((κ → Rˣ) → R)

The Laurent functions on the split torus 𝔾ₘ^κ: the R-subalgebra of functions on its points spanned by the characters. Over a field these are the functions given by a Laurent polynomial in the coordinates; the characters are the Laurent monomials.

Equations

• TauCeti.laurentFunctions R κ = { carrier := ↑(TauCeti.charSpan✝ R κ), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

theorem TauCeti.mem_laurentFunctions_iff (R : Type u) [CommRing R] (κ : Type v) [Fintype κ] {f : (κ → Rˣ) → R} : f ∈ laurentFunctions R κ ↔ f ∈ Submodule.span R (Set.range fun (μ : κ → ℤ) => ⇑(weightCharHom R μ))

Membership in the Laurent functions is membership in the span of the characters: every Laurent function is a finite R-linear combination of characters.

@[simp]

theorem TauCeti.weightCharHom_mem_laurentFunctions (R : Type u) [CommRing R] {κ : Type v} [Fintype κ] (μ : κ → ℤ) : ⇑(weightCharHom R μ) ∈ laurentFunctions R κ

Every character is a Laurent function.

theorem TauCeti.weightCharHom_injective (K : Type u) [Field K] [Infinite K] {κ : Type v} [Fintype κ] : Function.Injective (weightCharHom K)

Distinct weights give distinct K-valued characters of the split torus, over an infinite field.

theorem TauCeti.linearIndependent_weightCharHom (K : Type u) [Field K] [Infinite K] {κ : Type v} [Fintype κ] : LinearIndependent K fun (μ : κ → ℤ) => ⇑(weightCharHom K μ)

Artin's independence of characters for a split torus: over an infinite field the characters of 𝔾ₘ^κ, read as K-valued functions on its points, are linearly independent. This is what makes the coefficients of a Laurent expansion well defined, and hence what makes a weight readable off the action of the torus.