Documentation

TauCeti.RepresentationTheory.SU2.Completeness

The characters of the symmetric powers span the class functions of SU(2) #

TauCeti/RepresentationTheory/SU2/Weyl/Orthogonality.lean proves that the characters χ_d of the symmetric powers Symᵈ(ℂ²) are orthonormal against the Weyl density. This file proves the complementary statement, that nothing else is needed: the ℂ-linear span of the χ_d is uniformly dense in the continuous class functions of SU(2), and its closure is exactly the space of continuous class functions.

The route #

The engine is a closed form for the character. TauCeti.SU2.character_symPower_torusHom_zpow computes χ_d on the maximal torus as the weight string ∑_{i ≤ d} z^{2i-d}, and multiplying that string by z + z⁻¹ = tr (diag (z, z⁻¹)) telescopes to χ_{d+1} + χ_{d-1}. Since both sides are class functions and every element of SU(2) is conjugate into the torus, this recursion holds on all of SU(2) (TauCeti.SU2.trace_mul_character_symPower). It is the Chebyshev recursion, so with the two base cases χ_0 = 1 and χ_1 = tr it gives

χ_d = U_d (tr / 2) (TauCeti.SU2.character_symPower_eq_chebyshevU_eval)

for the Chebyshev polynomial Polynomial.Chebyshev.U of the second kind. Two things follow at once: each χ_d is continuous, being a polynomial in the trace; and, running the recursion the other way, every power of the trace lies in the span of the χ_d (TauCeti.SU2.pow_symPowerCharacter_one_mem_characterSpan), so by linearity that span is exactly the polynomial functions of the trace.

Density is then Weierstrass approximation on the interval [-2, 2] of traces. Every element of SU(2) is conjugate to diag (e^{iθ}, e^{-iθ}) for an angle θ of the Weyl chamber [0, π] (TauCeti.SU2.exists_isConj_torusExp_mem_Icc), where the trace is 2 cos θ; since arccos inverts cos on that chamber, the continuous function t ↦ f (diag (e^{i arccos (t/2)}, …)) on [-2, 2] takes at the trace of g the value f g. Approximating its real and imaginary parts by real polynomials and substituting the trace therefore approximates f uniformly by elements of the span.

Main definitions #

Main results #

References #

This is the completeness half of the "the {χ_n} are an orthonormal basis of the class functions of SU(2)" item of the SU(2) engine case of TauCetiRoadmap/RepresentationTheory/CompactGroups/README.md; orthonormality is TauCeti.SU2.character_symPower_orthonormal_torusExp. It is the analytic input to the remaining item of that engine case, that the Symᵈ(ℂ²) exhaust the finite-dimensional irreducibles, which is not proved here: that deduction additionally needs the symmetric powers as continuous unitary representations, so that the character orthogonality of TauCeti/RepresentationTheory/Compact/Character/Basic.lean applies to them.

The Chebyshev recursion for the characters #

source
theorem TauCeti.SU2.trace_mul_character_symPower (d : ℕ) (g : SU2) :
(↑g).trace * (symPower (d + 1)).character g = (symPower (d + 2)).character g + (symPower d).character g

The Chebyshev recursion for the characters of SU(2): tr · χ_{d+1} = χ_{d+2} + χ_d.

On the level of representations this is the Clebsch-Gordan decomposition Sym¹(ℂ²) ⊗ Sym^{d+1}(ℂ²) ≅ Sym^{d+2}(ℂ²) ⊕ Symᵈ(ℂ²), read on characters; only the character identity is proved here, by telescoping the weight strings on the maximal torus and extending to SU(2) by conjugation invariance.

source
@[simp]
theorem TauCeti.SU2.character_symPower_zero (g : SU2) :
(symPower 0).character g = 1

Sym⁰(ℂ²) is the trivial representation: its character is constantly 1.

source
@[simp]
theorem TauCeti.SU2.character_symPower_one_eq_trace (g : SU2) :
(symPower 1).character g = (↑g).trace

Sym¹(ℂ²) is the standard representation: its character is the trace.

source
theorem TauCeti.SU2.character_symPower_eq_chebyshevU_eval (d : ℕ) (g : SU2) :
(symPower d).character g = Polynomial.eval ((↑g).trace / 2) (Polynomial.Chebyshev.U ℂ ↑d)

The character of Symᵈ(ℂ²) is the Chebyshev polynomial of half the trace: χ_d (g) = U_d (tr g / 2), for Polynomial.Chebyshev.U the Chebyshev polynomial of the second kind. On the maximal torus this is the classical U_d (cos θ) = sin ((d+1) θ) / sin θ, and off it the statement is meaningful because the trace is a complete conjugacy invariant of SU(2).

The characters as continuous functions #

source
theorem TauCeti.SU2.continuous_character_symPower (d : ℕ) :
Continuous fun (g : SU2) => (symPower d).character g

The character of Symᵈ(ℂ²) is continuous, being a polynomial in the trace.

source
noncomputable def TauCeti.SU2.symPowerCharacter (d : ℕ) :
C(SU2, ℂ)

The character of Symᵈ(ℂ²), bundled as a continuous function on SU(2). This is the form in which the characters generate a subspace of C(SU(2), ℂ); the unbundled statements are about (TauCeti.SU2.symPower d).character.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SU2.symPowerCharacter_apply (d : ℕ) (g : SU2) :
    (symPowerCharacter d) g = (symPower d).character g
    source
    @[simp]
    theorem TauCeti.SU2.symPowerCharacter_zero :
    symPowerCharacter 0 = 1

    The span of the characters #

    source
    noncomputable def TauCeti.SU2.characterSpan :
    Submodule ℂ C(SU2, ℂ)

    The ℂ-linear span of the characters of the symmetric powers Symᵈ(ℂ²) inside the continuous complex-valued functions on SU(2).

    Equations
    Instances For
      source
      theorem TauCeti.SU2.symPowerCharacter_mem_characterSpan (d : ℕ) :
      symPowerCharacter d ∈ characterSpan
      source
      theorem TauCeti.SU2.characterSpan_le_iff {p : Submodule ℂ C(SU2, ℂ)} :
      characterSpan ≤ p ↔ ∀ (d : ℕ), symPowerCharacter d ∈ p

      The span of the characters is contained in a subspace exactly when every character is: the characteristic property of TauCeti.SU2.characterSpan as a span.

      source
      theorem TauCeti.SU2.pow_symPowerCharacter_one_mem_characterSpan (n : ℕ) :
      symPowerCharacter 1 ^ n ∈ characterSpan

      Every power of the trace lies in the span of the characters. The first character is the trace (TauCeti.SU2.character_symPower_one_eq_trace), so with linearity this says that every polynomial function of the trace is a linear combination of the characters; the reverse inclusion is TauCeti.SU2.character_symPower_eq_chebyshevU_eval, which writes each character as a polynomial in the trace.

      Uniform density in the class functions #

      source
      theorem TauCeti.SU2.exists_mem_characterSpan_norm_sub_lt {f : C(SU2, ℂ)} (hf : ∀ (u g : SU2), f (u * g * u⁻¹) = f g) {ε : ℝ} (hε : 0 < ε) :
      ∃ h ∈ characterSpan, ‖f - h‖ < ε

      The characters of the symmetric powers span a uniformly dense subspace of the continuous class functions of SU(2): a continuous conjugation-invariant function is within any ε > 0, in the supremum norm, of a linear combination of the χ_d.

      The class function is read on the Weyl chamber [0, π], where θ ↦ 2 cos θ parametrises the traces [-2, 2]; Weierstrass approximation on that interval, applied to the real and imaginary parts, produces the linear combination through TauCeti.SU2.pow_symPowerCharacter_one_mem_characterSpan.

      source
      theorem TauCeti.SU2.mem_topologicalClosure_characterSpan_iff {f : C(SU2, ℂ)} :
      f ∈ characterSpan.topologicalClosure ↔ ∀ (u g : SU2), f (u * g * u⁻¹) = f g

      The closure of the span of the characters is exactly the continuous class functions of SU(2). Membership of the closure is uniform approximability by linear combinations of the χ_d, so this says that the characters of the symmetric powers are a complete orthonormal system for the class functions, the companion of the orthonormality TauCeti.SU2.character_symPower_orthonormal_torusExp.