Documentation

TauCeti.RepresentationTheory.SU2.Weyl.Character

The Weyl character formula for 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

χ_d (diag (z, z⁻¹)) = z^{-d} + z^{2-d} + ⋯ + z^d.

This file sums that string. Multiplying it by the Weyl denominator z - z⁻¹ telescopes, so

(z - z⁻¹) · χ_d (diag (z, z⁻¹)) = z^{d+1} - z^{-(d+1)}

with no hypothesis on z, and away from the two points z = ±1 where the denominator vanishes this is the Weyl character formula

χ_d (diag (z, z⁻¹)) = (z^{d+1} - z^{-(d+1)}) / (z - z⁻¹).

At the two excluded points the character is (d + 1) · z^d, so the value there is the dimension up to sign, and the description of the character on the torus is complete.

In the angle parametrisation z = e^{iθ} of the torus the numerator and the denominator are 2i·sin ((d+1)θ) and 2i·sin θ, so the telescoping identity reads sin θ · χ_d = sin ((d+1)θ) -- again with no hypothesis, both sides vanishing at the multiples of π -- and the character formula becomes the classical

χ_d (diag (e^{iθ}, e^{-iθ})) = sin ((d+1)θ) / sin θ.

At a multiple of π the character is (d + 1) cosᵈ θ, the two excluded points z = ±1 read in the angle coordinate, so the description in that coordinate is complete as well.

These formulas compute the character of Symᵈ(ℂ²) everywhere, no declaration here being needed for that: a character is conjugation invariant (Representation.char_conj), and TauCeti.SU2.exists_mem_Icc_eq_torusExp_of_conjInvariant (TauCeti/RepresentationTheory/SU2/ConjugacyClasses.lean, not imported here) carries a conjugation-invariant function to the angle in the Weyl chamber [0, π] of the torus element that the given element is conjugate to, where the closed forms below apply.

Main results #

References #

This serves the engine case of TauCetiRoadmap/RepresentationTheory/CompactGroups/README.md, "Engine case: SU(2) and the maximal torus", which asks for the character on the torus in the closed forms sin ((n+1)θ) / sin θ and (e^{i(n+1)θ} - e^{-i(n+1)θ}) / (e^{iθ} - e^{-iθ}).

source
theorem TauCeti.SU2.sub_inv_mul_character_symPower_torusHom (d : ℕ) (z : Circle) :
(↑z - (↑z)⁻¹) * (symPower d).character (torusHom z) = ↑z ^ (d + 1) - (↑z)⁻¹ ^ (d + 1)

The Weyl numerator identity. Multiplying the weight string of Symᵈ(ℂ²) by the Weyl denominator z - z⁻¹ telescopes to z^{d+1} - z^{-(d+1)}.

No hypothesis is needed on z: at the two points z = ±1 where the denominator vanishes both sides are 0.

source
theorem TauCeti.SU2.character_symPower_torusHom_eq_div (d : ℕ) {z : Circle} (hz : ↑z ^ 2 ≠ 1) :
(symPower d).character (torusHom z) = (↑z ^ (d + 1) - (↑z)⁻¹ ^ (d + 1)) / (↑z - (↑z)⁻¹)

The Weyl character formula for SU(2). Away from the two points z = ±1 of the maximal torus, where the Weyl denominator vanishes, the character of Symᵈ(ℂ²) at diag (z, z⁻¹) is the quotient of the Weyl numerator by the Weyl denominator.

source
theorem TauCeti.SU2.character_symPower_torusHom_of_sq_eq_one (d : ℕ) {z : Circle} (hz : ↑z ^ 2 = 1) :
(symPower d).character (torusHom z) = (↑d + 1) * ↑z ^ d

The character at the two points where the Weyl denominator vanishes. At z = ±1 every one of the d + 1 weights contributes z^d, so the character is (d + 1) · z^d; in particular it is d + 1 at the identity and (-1)^d · (d + 1) at the central element -1.

source
theorem TauCeti.SU2.sin_mul_character_symPower_torusExp (d : ℕ) (θ : ℝ) :
↑(Real.sin θ) * (symPower d).character (torusExp θ) = ↑(Real.sin ((↑d + 1) * θ))

The Weyl numerator identity in the angle parametrisation: writing the torus element as diag (e^{iθ}, e^{-iθ}), the identity of TauCeti.SU2.sub_inv_mul_character_symPower_torusHom reads sin θ · χ_d (θ) = sin ((d+1)θ).

As there, no hypothesis is needed on θ: at a multiple of π both sides vanish.

source
theorem TauCeti.SU2.character_symPower_torusExp_eq_sin_div_sin (d : ℕ) {θ : ℝ} (hθ : Real.sin θ ≠ 0) :
(symPower d).character (torusExp θ) = ↑(Real.sin ((↑d + 1) * θ) / Real.sin θ)

The Weyl character formula in the angle parametrisation. Off the multiples of π, where the Weyl denominator 2i·sin θ vanishes, the character of Symᵈ(ℂ²) at diag (e^{iθ}, e^{-iθ}) is sin ((d+1)θ) / sin θ. In particular it is real.

source
theorem TauCeti.SU2.character_symPower_torusExp_of_sin_eq_zero (d : ℕ) {θ : ℝ} (hθ : Real.sin θ = 0) :
(symPower d).character (torusExp θ) = (↑d + 1) * ↑(Real.cos θ) ^ d

The character at the multiples of π, where the Weyl denominator vanishes, in the angle parametrisation: there e^{iθ} = cos θ = ±1, and the character of Symᵈ(ℂ²) is (d + 1) cosᵈ θ. This is TauCeti.SU2.character_symPower_torusHom_of_sq_eq_one read in the angle coordinate, and with TauCeti.SU2.character_symPower_torusExp_eq_sin_div_sin it evaluates the character at every angle.

source
@[simp]
theorem TauCeti.SU2.conj_character_symPower_torusExp (d : ℕ) (θ : ℝ) :
(starRingEnd ℂ) ((symPower d).character (torusExp θ)) = (symPower d).character (torusExp θ)

The character of Symᵈ(ℂ²) is real on the maximal torus: it is a sum of a weight string z^{-d} + ⋯ + z^{d} closed under inversion, and both closed forms above exhibit it as the coercion of a real number, so complex conjugation leaves it fixed.

source
theorem TauCeti.SU2.character_symPower_torusExp_eq_div (d : ℕ) {θ : ℝ} (hθ : Real.sin θ ≠ 0) :
(symPower d).character (torusExp θ) = (Complex.exp (↑((↑d + 1) * θ) * Complex.I) - Complex.exp (-(↑((↑d + 1) * θ) * Complex.I))) / (Complex.exp (↑θ * Complex.I) - Complex.exp (-(↑θ * Complex.I)))

The alternating-sum form of the Weyl character formula. Off the multiples of π the character of Symᵈ(ℂ²) on the torus is the quotient of the alternating sums e^{i(d+1)θ} - e^{-i(d+1)θ} and e^{iθ} - e^{-iθ}.