The weight decomposition of Symᵈ(ℂ²) under the maximal torus of SU(2)

TauCeti/RepresentationTheory/SU2/SymmetricPower.lean computes the character of the symmetric power Symᵈ(ℂ²) of the standard representation of SU(2) on the maximal torus as the weight string z^{-d} + z^{2-d} + ⋯ + z^d. A character is a trace, so it records the weights only with multiplicity; this file builds the decomposition behind it.

The monomial basis of Symᵈ(ℂ²), reindexed by Fin (d + 1) through TauCeti.symFinTwoEquiv, is a basis of weight vectors: diag(z, z⁻¹) acts on the i-th one by the scalar z^{2i - d}. The d + 1 weights 2i - d are pairwise distinct, so each weight occurs with multiplicity exactly one, and the character above, TauCeti.SU2.character_symPower_torusHom_zpow, is their sum.

Two consequences make this the form the highest-weight classification uses.

• A torus-stable subspace is spanned by weight vectors. Nothing forces this for a single operator with repeated eigenvalues; here the eigenvalues are distinct, which is exactly the hypothesis of the general coordinate argument TauCeti/LinearAlgebra/Eigenspace/DiagonalBasis.lean. Feeding it a torus element whose integer powers are pairwise distinct — exp(i), by the irrationality of π — separates the d + 1 weights at once. That element is a device of the proof and stays private to this file.
• The weight spaces are lines. A nonzero vector on which the whole torus acts through a single character z ↦ z^m is a multiple of one basis vector, and m is one of the d + 1 weights.

Main definitions

• TauCeti.SU2.weightBasis: the weight basis of Symᵈ(ℂ²), indexed by Fin (d + 1).
• TauCeti.SU2.weight: the weight 2i - d of the i-th weight vector.

Main results

• TauCeti.SU2.symPower_torusHom_weightBasis: diag(z, z⁻¹) acts on the i-th weight vector by z^{2i - d}, and TauCeti.SU2.weight_injective: the weights are pairwise distinct.
• TauCeti.SU2.weightBasis_mem_of_repr_ne_zero and TauCeti.SU2.eq_span_weightBasis_mem: a torus-stable subspace contains every weight vector occurring in one of its elements, and is spanned by the weight vectors it contains.
• TauCeti.SU2.exists_weight_eq_of_forall_torusHom_smul: a nonzero vector on which the torus acts through a single character z ↦ z^m is a multiple of a single weight vector, and m is that vector's weight.

References

This is the "weight/string decomposition" milestone of the SU(2) engine case of TauCetiRoadmap/RepresentationTheory/CompactGroups/README.md, which asks for the weights {d, d-2, …, -d} of Symᵈ(ℂ²) "each with multiplicity one, computed from the diagonal action", as the input to the highest-weight argument.

• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapter 3.
• T. Bröcker, T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter II, §5.

The weight basis and the weights

noncomputable def TauCeti.SU2.weightBasis (d : ℕ) : Module.Basis (Fin (d + 1)) ℂ (SymmetricPower ℂ (Fin d) (Fin 2 → ℂ))

The weight basis of Symᵈ(ℂ²): the monomial basis of the symmetric power, whose index i : Fin (d + 1) counts the factors equal to the first standard basis vector of ℂ². Its elements are eigenvectors of the maximal torus, by TauCeti.SU2.symPower_torusHom_weightBasis.

Equations

• TauCeti.SU2.weightBasis d = (Module.Basis.symmetricPower d (Pi.basisFun ℂ (Fin 2))).reindex (TauCeti.symFinTwoEquiv d)

theorem TauCeti.SU2.weightBasis_apply (d : ℕ) (i : Fin (d + 1)) : (weightBasis d) i = (Module.Basis.symmetricPower d (Pi.basisFun ℂ (Fin 2))) ((symFinTwoEquiv d).symm i)

The i-th weight vector is the monomial basis vector of Symᵈ(ℂ²) with i factors equal to the first standard basis vector of ℂ² and d - i equal to the second.

theorem TauCeti.SU2.exists_weightBasis_eq_tprod (d : ℕ) (i : Fin (d + 1)) : ∃ (f : Fin d → Fin 2), (weightBasis d) i = ⨂ₛ[ℂ] (j : Fin d), (Pi.basisFun ℂ (Fin 2)) (f j)

Every weight vector is a pure symmetric tensor of standard basis vectors: some ordering of the unordered tuple indexing it lists its factors.

def TauCeti.SU2.weight (d : ℕ) (i : Fin (d + 1)) : ℤ

The weight of the i-th weight vector: the torus element diag(z, z⁻¹) acts on it by z^{2i - d}. As i runs over Fin (d + 1) these are the d + 1 integers -d, 2 - d, …, d - 2, d.

Equations

• TauCeti.SU2.weight d i = 2 * ↑↑i - ↑d

theorem TauCeti.SU2.weight_def (d : ℕ) (i : Fin (d + 1)) : weight d i = 2 * ↑↑i - ↑d

The weight of the i-th weight vector, unfolded.

@[simp]

theorem TauCeti.SU2.weight_zero (d : ℕ) : weight d 0 = -↑d

The lowest weight of Symᵈ(ℂ²) is -d, on the monomial with no factor of the first basis vector.

@[simp]

theorem TauCeti.SU2.weight_last (d : ℕ) : weight d (Fin.last d) = ↑d

The highest weight of Symᵈ(ℂ²) is d, on the d-th power of the first basis vector.

theorem TauCeti.SU2.weight_injective (d : ℕ) : Function.Injective (weight d)

The d + 1 weights 2i - d are pairwise distinct. Together with TauCeti.SU2.symPower_torusHom_weightBasis this is what makes each weight of Symᵈ(ℂ²) occur with multiplicity one, in the form TauCeti.SU2.exists_weight_eq_of_forall_torusHom_smul.

The torus acts diagonally in the weight basis

theorem TauCeti.SU2.symPower_torusHom_weightBasis (d : ℕ) (z : Circle) (i : Fin (d + 1)) : ((symPower d) (torusHom z)) ((weightBasis d) i) = ↑z ^ weight d i • (weightBasis d) i

The maximal torus is diagonal in the weight basis: diag(z, z⁻¹) multiplies the i-th weight vector by z^{2i - d}. This is the weight decomposition of Symᵈ(ℂ²), of which the character TauCeti.SU2.character_symPower_torusHom is the trace.

theorem TauCeti.SU2.weightBasis_repr_symPower_torusHom (d : ℕ) (z : Circle) (w : SymmetricPower ℂ (Fin d) (Fin 2 → ℂ)) (i : Fin (d + 1)) : ((weightBasis d).repr (((symPower d) (torusHom z)) w)) i = ↑z ^ weight d i * ((weightBasis d).repr w) i

The coordinates of a vector in the weight basis are scaled by the weights: the torus is diagonal, so it multiplies the i-th coordinate by z^{2i - d}.

A torus element with pairwise distinct powers

Torus-stable subspaces are spanned by weight vectors

theorem TauCeti.SU2.weightBasis_mem_of_repr_ne_zero {d : ℕ} {W : Submodule ℂ (SymmetricPower ℂ (Fin d) (Fin 2 → ℂ))} (hW : ∀ (z : Circle), ∀ v ∈ W, ((symPower d) (torusHom z)) v ∈ W) {w : SymmetricPower ℂ (Fin d) (Fin 2 → ℂ)} (hw : w ∈ W) {i : Fin (d + 1)} (hi : ((weightBasis d).repr w) i ≠ 0) : (weightBasis d) i ∈ W

A torus-stable subspace contains every weight vector that occurs in one of its elements. The torus is diagonal in the weight basis and the weights weight d i are pairwise distinct, so a single torus element already separates the coordinates of a vector.

theorem TauCeti.SU2.eq_span_weightBasis_mem {d : ℕ} {W : Submodule ℂ (SymmetricPower ℂ (Fin d) (Fin 2 → ℂ))} (hW : ∀ (z : Circle), ∀ v ∈ W, ((symPower d) (torusHom z)) v ∈ W) : W = Submodule.span ℂ {v : SymmetricPower ℂ (Fin d) (Fin 2 → ℂ) | ∃ (i : Fin (d + 1)), (weightBasis d) i = v ∧ v ∈ W}

A torus-stable subspace of Symᵈ(ℂ²) is spanned by the weight vectors it contains.

The weight spaces are lines

theorem TauCeti.SU2.exists_weight_eq_of_forall_torusHom_smul {d : ℕ} {w : SymmetricPower ℂ (Fin d) (Fin 2 → ℂ)} (hw : w ≠ 0) {m : ℤ} (hsmul : ∀ (z : Circle), ((symPower d) (torusHom z)) w = ↑z ^ m • w) : ∃ (i : Fin (d + 1)), weight d i = m ∧ w ∈ ℂ ∙ (weightBasis d) i

A vector transforming under a single character of the torus is a weight vector. A nonzero w on which the whole maximal torus acts through z ↦ z^m is a multiple of a single weight vector, and m is that vector's weight, one of the d + 1 integers 2i - d.