Weight spaces read off a basis of weight vectors #
A representation of GL n k that has a basis of weight vectors has no weights other than the ones
that basis exhibits, and no weight multiplicities other than the ones it counts. This file proves
that, once and for all: given a basis b : Module.Basis ι k W together with an assignment
wt : ι → Fin n → ℤ making b i a vector of weight wt i, the weight spaces of ρ span W, the
weight-l space is spanned by the basis vectors labelled l, and every weight space carrying no
label at all vanishes. When the labelling is injective that coordinate subspace is the single
line k ∙ b i on the one basis vector labelled l = wt i; without injectivity it is not, two
basis vectors of the same weight spanning a plane inside one weight space.
This is the pattern every concrete computation of the weight spaces of a GL n k-representation
follows — the coordinate lines of the standard representation, the wedges of standard basis vectors
in an exterior power, the unordered tuples in a symmetric power — and the only thing that varies
between them is the basis and the combinatorial label wt. Isolating it here keeps those
computations to the one step that is genuinely about the representation, namely that each basis
vector is a weight vector.
Two hypotheses recur and are not interchangeable. The separation hypothesis
Function.Injective (weightChar k), standing throughout the weight theory of
TauCeti.RepresentationTheory.ClassicalGroups.Weight.Basic, says that distinct weights give
distinct characters of the torus; TauCeti.weightChar_injective supplies it over an infinite
field, and without it every weight space of every representation is everything over 𝔽₂. The
injectivity of the labelling Function.Injective wt is a separate, combinatorial condition: it
says the basis vectors have pairwise distinct weights, which is what makes each weight space a
single line rather than a larger coordinate subspace. The spanning statement needs neither; the
vanishing statement, and with it the description of which weights occur at all, needs only the
first.
Main results #
Module.Basis.iSup_weightSpace_eq_top: a representation with a basis of weight vectors is spanned by its weight spaces.Module.Basis.repr_eq_zero_of_mem_weightSpace: a weight vector has no coordinate on a basis vector of a different weight.Module.Basis.weightSpace_eq_span_image: the weight spaces are the coordinate subspaces of the basis, the weight-lspace being spanned by the basis vectors labelledl;Module.Basis.weightSpace_eq_spanreads that as a single line when the labelling is injective.Module.Basis.weightSpace_eq_botandModule.Basis.weightSpace_ne_bot_iff: the weights are exactly the labelswt i.Module.Basis.isInternal_weightSpace: a representation with a basis of weight vectors is the internal direct sum of its weight spaces.Module.Basis.finrank_weightSpace_eq_card: the multiplicity of a weight is the number of basis vectors carrying it, whenever that number is finite;Module.Basis.finrank_weightSpace_eq_oneis the case of a distinctly labelled weight, which needs no finiteness.
These are stated in the Module.Basis namespace, so that they read as b.weightSpace_eq_span on a
basis b, like the coordinate lemmas of TauCeti/LinearAlgebra/Eigenspace/DiagonalBasis.lean they
are built on.
References #
- W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.
A representation with a basis of weight vectors is spanned by its weight spaces. Each basis vector lies in one of them, and the basis spans.
Pinning the weight spaces down #
Here the coefficients must separate weights, in the sense that l ↦ weightChar k l is injective;
TauCeti.weightChar_injective supplies that over an infinite field. Only cancellation of nonzero
factors is needed of the ring itself: the argument compares two eigenvalues on a single nonzero
coordinate.
A weight vector has no coordinate on a basis vector of a different weight. The torus acts
on the coordinate of index i through the character of wt i and on the whole vector through the
character of its own weight, so a nonzero coordinate would equate the two characters.
The weight spaces of a representation with a basis of weight vectors are the coordinate
subspaces of that basis: the weight-l space is spanned by the basis vectors labelled l. No
injectivity of the labelling is needed; with it the span collapses to a single line, which is
Module.Basis.weightSpace_eq_span.
The weight spaces of a representation with a basis of weight vectors are the coordinate lines of that basis. The labelling must be injective: two basis vectors of the same weight span a plane inside a single weight space.
Only the labels are weights: a weight carried by no basis vector has no weight vector at all.
The weights of a representation with a basis of weight vectors are exactly the labels of that basis. The labelling need not be injective here: a label occurring at all already makes its weight space nonzero, since it contains a nonzero basis vector.
A representation with a basis of weight vectors is the internal direct sum of its weight spaces.
A basis of weight vectors counts the weight multiplicities: the multiplicity of l is the
number of basis vectors labelled l. The labelling need not be injective, which is the point:
this is the statement that survives when several basis vectors share a weight.
Finiteness of the fibre over l is what makes the count a natural number, and the rest of the
basis may be infinite; the injective case needs no finiteness at all, because there the weight
space is a single exhibited line (Module.Basis.finrank_weightSpace_eq_one).
Distinctly labelled basis weights have multiplicity one.