Documentation

TauCeti.RepresentationTheory.SU2.SymmetricPower

The symmetric powers of the standard representation of SU(2) #

The candidate irreducible representations of SU(2) are the symmetric powers Symᵈ(ℂ²) of the standard representation, of dimension d + 1. This file builds them, as the restriction of the symmetric powers of the standard representation of GL₂(ℂ) along the inclusion of SU(2), and computes their characters on the maximal torus.

The character computation is the weight string: on diag(z, z⁻¹) the character of Symᵈ is

z^d + z^{d-2} + ⋯ + z^{-d},

each of the d + 1 weights d, d-2, …, -d occurring exactly once. This is what the highest-weight classification of the irreducible representations of SU(2) runs on, and the value at the identity is the dimension d + 1, the number of those weights.

The route is Layer 1's TauCeti.char_symPowerRep_diagonal, which gives the character at a diagonal matrix as the complete homogeneous symmetric polynomial h_d in the diagonal entries, together with its rank-two evaluation TauCeti.eval_hsymm_fin_two: the geometric-looking sum ∑ᵢ x^i y^{d-i}.

Main definitions #

Main results #

References #

The symmetric powers of the standard representation #

source
def TauCeti.SU2.toGL :
SU2 →* GL (Fin 2) ℂ

SU(2) as a subgroup of GL₂(ℂ): an element of the group SU(2) is a unit there, and a unit of a submonoid of the matrices is a unit of the matrices.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SU2.coe_toGL (g : SU2) :
    ↑(toGL g) = ↑g
    source
    theorem TauCeti.SU2.toGL_injective :
    Function.Injective ⇑toGL

    The inclusion of SU(2) into GL₂(ℂ) is injective: it does not move the underlying matrix.

    source
    theorem TauCeti.SU2.toGL_torusHom (z : Circle) :
    toGL (torusHom z) = diagGL ![Circle.toUnits z, (Circle.toUnits z)⁻¹]

    The maximal torus of SU(2) inside the diagonal torus of GL₂(ℂ): torusHom z is the diagonal matrix diag(z, z⁻¹).

    source
    noncomputable def TauCeti.SU2.symPower (d : ℕ) :
    Representation ℂ SU2 (SymmetricPower ℂ (Fin d) (Fin 2 → ℂ))

    The d-th symmetric power of the standard representation of SU(2), the candidate irreducible of dimension d + 1: the restriction along TauCeti.SU2.toGL of the symmetric power of the standard representation of GL₂(ℂ).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.SU2.symPower_apply (d : ℕ) (g : SU2) :
      (symPower d) g = (symPowerRep ℂ 2 d) (toGL g)
      source
      theorem TauCeti.SU2.symPower_apply_tprod (d : ℕ) (g : SU2) (v : Fin d → Fin 2 → ℂ) :
      ((symPower d) g) (⨂ₛ[ℂ] (i : Fin d), v i) = ⨂ₛ[ℂ] (i : Fin d), (↑g).mulVec (v i)

      The action on a pure symmetric tensor is factor by factor: g multiplies each factor of v₁ ⊙ ⋯ ⊙ v_d by its own matrix.

      source
      @[simp]
      theorem TauCeti.SU2.finrank_symPower (d : ℕ) :
      Module.finrank ℂ (SymmetricPower ℂ (Fin d) (Fin 2 → ℂ)) = d + 1

      The space Symᵈ(ℂ²) carrying TauCeti.SU2.symPower d has dimension d + 1: a symmetric power of a free module is free on the unordered tuples of basis indices, of which there are Nat.multichoose 2 d = d + 1 in two variables.

      source
      theorem TauCeti.SU2.character_symPower_torusHom (d : ℕ) (z : Circle) :
      (symPower d).character (torusHom z) = ∑ i ∈ Finset.range (d + 1), ↑z ^ i * (↑z)⁻¹ ^ (d - i)

      The weight string. On the maximal torus the character of Symᵈ(ℂ²) is z^{-d} + z^{2-d} + ⋯ + z^d: the d + 1 weights -d, 2-d, …, d each occur once.

      source
      theorem TauCeti.SU2.character_symPower_torusHom_zpow (d : ℕ) (z : Circle) :
      (symPower d).character (torusHom z) = ∑ i ∈ Finset.range (d + 1), ↑z ^ (2 * ↑i - ↑d)

      The weight string with the weights displayed as integer exponents 2i - d.

      source
      theorem TauCeti.SU2.character_symPower_torusExp (d : ℕ) (θ : ℝ) :
      (symPower d).character (torusExp θ) = ∑ i ∈ Finset.range (d + 1), Complex.exp ((2 * ↑i - ↑d) * (↑θ * Complex.I))

      The weight string in exponential coordinates. Writing the torus element as diag(e^{iθ}, e^{-iθ}), the character of Symᵈ(ℂ²) is ∑ᵢ e^{i(2i-d)θ}: the classical e^{idθ} + e^{i(d-2)θ} + ⋯ + e^{-idθ}.

      source
      theorem TauCeti.SU2.character_symPower_one (d : ℕ) :
      (symPower d).character 1 = ↑d + 1

      The dimension is d + 1: the character at the identity is the rank of the underlying space, which is the number d + 1 of weights of the string above, each of multiplicity one.