Characters of SU(2) are even on the maximal torus

The Weyl group of SU(2) computed in TauCeti/RepresentationTheory/SU2/Weyl/Basic.lean inverts the maximal torus: the quarter turn w = !![0, -1; 1, 0] conjugates diag (z, z⁻¹) to diag (z⁻¹, z). Characters are conjugation invariant, so the character of a continuous finite-dimensional representation of SU(2) takes the same value at a torus element and at its inverse. In the angle parametrisation θ ↦ diag (e^{iθ}, e^{-iθ}) this reads χ (torusExp (-θ)) = χ (torusExp θ): the character is an even function of θ.

This is the W-invariance, on the maximal torus, of the characters of SU(2), and it is what makes those characters functions of cos θ. Off the torus this is subsumed by the classification of the conjugacy classes of SU(2) by the trace: a character, being a class function, is a function of the trace on all of SU(2) (ContRepresentation.character_eq_of_trace_eq).

Main results

• ContRepresentation.character_torusHom_inv: the character of a continuous finite-dimensional representation of SU(2) agrees at diag (z, z⁻¹) and diag (z⁻¹, z).
• ContRepresentation.character_torusExp_neg: read in the angle parametrisation of the maximal torus, that character is an even function of the angle.
• ContRepresentation.character_eq_of_trace_eq: that character is a function of the trace.

References

• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapter 18.
• T. Bröcker, T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter IV.

theorem ContRepresentation.character_torusHom_inv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ TauCeti.SU2 V) (hπ : Continuous ⇑π) (z : Circle) : (π.character hπ) (TauCeti.SU2.torusHom z⁻¹) = (π.character hπ) (TauCeti.SU2.torusHom z)

The character of a continuous representation of SU(2) is even on the maximal torus: its values at diag (z, z⁻¹) and at diag (z⁻¹, z) agree, the two being conjugate by the quarter turn.

theorem ContRepresentation.character_torusExp_neg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ TauCeti.SU2 V) (hπ : Continuous ⇑π) (θ : ℝ) : (π.character hπ) (TauCeti.SU2.torusExp (-θ)) = (π.character hπ) (TauCeti.SU2.torusExp θ)

The character of a continuous representation of SU(2), read in the angle parametrisation θ ↦ diag (e^{iθ}, e^{-iθ}) of the maximal torus, is an even function of θ. This is the sense in which the characters of SU(2) are W-invariant functions on the torus.

theorem ContRepresentation.character_eq_of_trace_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (π : ContRepresentation ℂ TauCeti.SU2 V) (hπ : Continuous ⇑π) {g h : TauCeti.SU2} (htr : (↑g).trace = (↑h).trace) : (π.character hπ) g = (π.character hπ) h

The character of a continuous finite-dimensional representation of SU(2) is a function of the trace, the trace being a complete conjugacy invariant (TauCeti.SU2.isConj_iff_trace_eq). Combined with TauCeti.SU2.exists_isConj_torusExp_mem_Icc this is what lets a character of SU(2) be computed from its values θ ↦ χ (diag (e^{iθ}, e^{-iθ})) on the Weyl chamber [0, π] alone.