Documentation

TauCeti.RepresentationTheory.SU2.Exhaustion

The symmetric powers exhaust the irreducibles of SU(2) #

TauCeti/RepresentationTheory/SU2/Irreducible.lean shows the symmetric powers Symᵈ(ℂ²) of the standard representation of SU(2) are irreducible and pairwise inequivalent, and TauCeti/RepresentationTheory/SU2/Completeness.lean shows their characters span a uniformly dense subspace of the continuous class functions. This file closes the classification: every finite-dimensional irreducible continuous representation of SU(2) is one of them (TauCeti.SU2.exists_nonempty_equiv_symPower), and the degree is unique (TauCeti.SU2.existsUnique_nonempty_equiv_symPower), so d ↦ Symᵈ(ℂ²) is a bijection from ℕ onto the isomorphism classes.

The deduction is the classical one: an irreducible not in the list has a character orthogonal to every χ_d, hence -- by continuity of the L² pairing along the uniform approximation -- to every class function, hence to itself, contradicting ‖χ_π‖ = 1. What is new here is the plumbing that lets the general orthogonality relations of TauCeti/RepresentationTheory/Compact/Character/Basic.lean reach Symᵈ(ℂ²) at all: those relations are about a ContRepresentation on a normed space, whereas Symᵈ(ℂ²) is a symmetric tensor power, carrying no topology. So the weight basis is used to carry the symmetric power onto the standard model ℂ^{d+1} (TauCeti.SU2.symPowerModel), and its action is shown to be continuous.

That continuity is the one genuinely analytic step. A group element acts on a pure symmetric tensor factor by factor, so the action is the composition of the continuous map g ↦ (g·v₁, …, g·v_d) with the multilinear map ⨂ₛ, read in coordinates; multilinear maps on finite-dimensional spaces are continuous (MultilinearMap.continuous_of_finiteDimensional), and expanding an arbitrary vector in the weight basis extends the conclusion from pure tensors to all of Symᵈ(ℂ²).

Unitarity of Symᵈ(ℂ²) is not established, and is not needed: the second orthogonality relation asks for unitarity only of the representation being tested, and even that hypothesis is discharged by Weyl's unitarian trick, so the statements below assume none. The transported model carries the inner product making the weight basis orthonormal, which for d ≥ 2 is not the SU(2)-invariant one.

Main definitions #

Main results #

References #

The character-theoretic argument uses the irreducibility and weight results of TauCeti/RepresentationTheory/SU2/Irreducible.lean together with the density of the character span. It is not circular. Peter-Weyl is nowhere used; the density is Stone-Weierstrass applied to the Chebyshev recursion for χ_d; and the orthogonality relations invoked are the general compact-group ones of TauCeti/RepresentationTheory/Compact/Character/Basic.lean, which know nothing of SU(2), rather than the concrete SU(2) orthonormality that is computed from the Weyl integration formula.

source
noncomputable def TauCeti.SU2.weightEquiv (d : ℕ) :
SymmetricPower ℂ (Fin d) (Fin 2 → ℂ) ≃ₗ[ℂ] EuclideanSpace ℂ (Fin (d + 1))

The weight basis read as an identification of Symᵈ(ℂ²) with the standard model space ℂ^{d+1}.

Equations
Instances For
    source
    noncomputable def TauCeti.SU2.symPowerModel (d : ℕ) :
    ContRepresentation ℂ SU2 (EuclideanSpace ℂ (Fin (d + 1)))

    The d-th symmetric power of the standard representation of SU(2), carried onto the standard model space ℂ^{d+1} by the weight basis.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.SU2.weightEquiv_weightBasis (d : ℕ) (i : Fin (d + 1)) :
      (weightEquiv d) ((weightBasis d) i) = EuclideanSpace.single i 1

      The identification sends the i-th weight vector to the i-th standard basis vector.

      source
      @[simp]
      theorem TauCeti.SU2.weightEquiv_symm_single (d : ℕ) (i : Fin (d + 1)) :
      (weightEquiv d).symm (EuclideanSpace.single i 1) = (weightBasis d) i

      The identification sends the i-th standard basis vector back to the i-th weight vector.

      source
      @[simp]
      theorem TauCeti.SU2.symPowerModel_apply (d : ℕ) (g : SU2) (x : EuclideanSpace ℂ (Fin (d + 1))) :
      ((symPowerModel d) g) x = (weightEquiv d) (((symPower d) g) ((weightEquiv d).symm x))

      Continuity #

      source
      theorem TauCeti.SU2.continuous_symPowerModel (d : ℕ) :
      Continuous ⇑(symPowerModel d)

      The model action is continuous. A pure symmetric tensor moves multilinearly in its factors, and a multilinear map on finite-dimensional spaces is continuous, so the coordinates of the action are continuous in the group element.

      What the model inherits #

      source
      noncomputable def TauCeti.SU2.symPowerModelEquiv (d : ℕ) :
      (symPower d).Equiv (ContRepresentation.toRepresentation ℂ SU2 (EuclideanSpace ℂ (Fin (d + 1))) (symPowerModel d))

      The model is equivalent to the symmetric power it is transported from.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.SU2.symPowerModelEquiv_toLinearEquiv (d : ℕ) :
        (symPowerModelEquiv d).toLinearEquiv = weightEquiv d

        The equivalence to the model is the weight-basis identification.

        source
        @[simp]
        theorem TauCeti.SU2.symPowerModelEquiv_apply (d : ℕ) (x : SymmetricPower ℂ (Fin d) (Fin 2 → ℂ)) :
        (symPowerModelEquiv d) x = (weightEquiv d) x
        source
        @[simp]
        theorem TauCeti.SU2.character_symPowerModel (d : ℕ) :
        (symPowerModel d).character ⋯ = symPowerCharacter d

        The character of the model is the character of the symmetric power: the trace does not see the transport.

        source
        theorem TauCeti.SU2.isIrreducible_symPowerModel (d : ℕ) :
        (ContRepresentation.toRepresentation ℂ SU2 (EuclideanSpace ℂ (Fin (d + 1))) (symPowerModel d)).IsIrreducible

        The model is irreducible, being equivalent to Symᵈ(ℂ²).

        Exhaustion #

        source
        theorem TauCeti.SU2.exists_nonempty_equiv_symPower {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ SU2 V) (hπ : Continuous ⇑π) (hirr : (ContRepresentation.toRepresentation ℂ SU2 V π).IsIrreducible) :
        ∃ (d : ℕ), Nonempty ((symPower d).Equiv (ContRepresentation.toRepresentation ℂ SU2 V π))

        The symmetric powers exhaust the irreducibles of SU(2). Every finite-dimensional irreducible continuous representation of SU(2) is equivalent to Symᵈ(ℂ²) for some d.

        Neither an inner product nor unitarity is assumed of the carrier. A finite-dimensional normed space over ℂ is continuously linearly equivalent to ℂ^{dim V} by dimension count, and transporting π along that equivalence changes neither the hypotheses nor the conclusion, so the argument may be run on a Euclidean carrier, where the characters live; there Weyl's unitarian trick disposes of unitarity in the same way.

        source
        theorem TauCeti.SU2.existsUnique_nonempty_equiv_symPower {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ SU2 V) (hπ : Continuous ⇑π) (hirr : (ContRepresentation.toRepresentation ℂ SU2 V π).IsIrreducible) :
        ∃! d : ℕ, Nonempty ((symPower d).Equiv (ContRepresentation.toRepresentation ℂ SU2 V π))

        The classification of the irreducible representations of SU(2). A finite-dimensional irreducible continuous representation of SU(2) is Symᵈ(ℂ²) for exactly one d, so d ↦ Symᵈ(ℂ²) is a bijection from ℕ onto the isomorphism classes. Exhaustion is TauCeti.SU2.exists_nonempty_equiv_symPower and uniqueness is TauCeti.SU2.nonempty_equiv_symPower_iff.