The symmetric powers of the standard representation of SU(2) are irreducible

TauCeti/RepresentationTheory/SU2/Weight.lean decomposes Symᵈ(ℂ²) under the maximal torus: the monomial basis TauCeti.SU2.weightBasis consists of weight vectors, the d + 1 weights are pairwise distinct, and consequently a torus-stable subspace is spanned by the weight vectors it contains. That is one half of the highest-weight argument; this file supplies the other half and concludes that Symᵈ(ℂ²) is an irreducible representation of SU(2), for every d.

The torus alone cannot see irreducibility: it is abelian, and every span of weight vectors is torus-stable. What breaks the weight vectors apart is a single element of SU(2) off the torus. Fix the rotation u = !![3/5, -4/5; 4/5, 3/5], an element of SU(2) none of whose entries vanishes, and let W ≠ 0 be an invariant subspace. Then:

• W is torus-stable, so it contains some weight vector, TauCeti.SU2.weightBasis d i.
• The coordinate of u · (weight vector) at the highest weight is a product of entries of u, one for each tensor factor, hence nonzero: the highest weight is indexed by a constant unordered tuple, and only the constant ordered tuple orders it, so the coordinate is the single product ∏ⱼ u₀,ₖⱼ with no cancellation (SymmetricPower.repr_basis_symmetricPower_tprod_ofFn_const). Torus-stability then puts the highest weight vector e₀^d into W.
• u · e₀^d is the pure power (u e₀)^d, and a pure power of a vector with nonzero coordinates has every coordinate nonzero (SymmetricPower.repr_basis_symmetricPower_tprod_const_ne_zero); the terms of the coordinate sum all coincide, so again nothing cancels. Torus-stability now puts every weight vector into W, so W is everything.

The choice of u matters only through the non-vanishing of its four entries, and the rational rotation is taken to keep that check arithmetic. It is a device of the proof and stays private to this file, as TauCeti.SU2.genericTorus does in the weight file.

Main results

• TauCeti.SU2.isIrreducible_symPower: Symᵈ(ℂ²) is an irreducible representation of SU(2).
• TauCeti.SU2.nonempty_equiv_symPower_iff: two of them are equivalent exactly when they have the same degree, so the Symᵈ(ℂ²) are pairwise inequivalent.

Exhaustion -- that every finite-dimensional irreducible representation of SU(2) is one of these -- is not proved here; it is the remaining half of the classification, and is TauCeti/RepresentationTheory/SU2/Exhaustion.lean.

References

This is the "the su2Irrep n are irreducible, pairwise inequivalent" half of the classification asked for by the SU(2) engine case of TauCetiRoadmap/RepresentationTheory/CompactGroups/README.md, which insists that the classification be proved by the weight/highest-weight argument rather than read off Peter-Weyl.

• 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.

A rotation with no zero entry

The weight basis as the monomial basis

The rotated weight vectors have nonzero coordinates

Irreducibility

theorem TauCeti.SU2.isIrreducible_symPower (d : ℕ) : (symPower d).IsIrreducible

The symmetric powers of the standard representation of SU(2) are irreducible. A nonzero invariant subspace is torus-stable, hence spanned by the weight vectors it contains. The image under the rotation TauCeti.SU2.mixMatrix of one of those weight vectors has a nonzero coordinate at the highest weight, which puts the highest weight vector in the subspace; the image of the highest weight vector in turn has a nonzero coordinate at every weight, which puts every weight vector in the subspace. So the subspace is everything.

This is the highest-weight half of the classification of the irreducibles of SU(2); the character orthonormality of TauCeti/RepresentationTheory/SU2/Weyl/Orthogonality.lean validates it but does not prove it.

@[simp]

theorem TauCeti.SU2.nonempty_equiv_symPower_iff (d e : ℕ) : Nonempty ((symPower d).Equiv (symPower e)) ↔ d = e

The symmetric powers are pairwise inequivalent: they are equivalent exactly when they have the same degree, their dimensions d + 1 being distinct. With TauCeti.SU2.isIrreducible_symPower this exhibits Symᵈ(ℂ²) as a family of pairwise non-isomorphic irreducibles of SU(2), one in each dimension.