Documentation

TauCeti.RepresentationTheory.SU2.TorusConjugacy

Every element of SU(2) is conjugate into the maximal torus #

The maximal torus T of SU(2) built in TauCeti/RepresentationTheory/SU2/Basic.lean meets every conjugacy class: for every g : SU(2) there is u : SU(2) with u g u⁻¹ ∈ T. This is the torus-conjugacy input the compact-group roadmap asks for before the classification of the irreducible representations of SU(2), and it is what makes a class function on SU(2) determined by its restriction to the circle.

The proof is unitary diagonalisation, arranged so that it only needs Mathlib's spectral theorem for Hermitian matrices. Mathlib has no spectral theorem for normal or unitary matrices, but in SU(2) one is not needed: writing G for the matrix of g, the determinant condition forces the Hermitian part of G to be a scalar,

G + G* = (tr G) • 1 (TauCeti.SU2.coe_add_star),

because G* = G⁻¹ is the adjugate of G (Matrix.specialUnitaryGroup.star_eq_adjugate) and a 2 × 2 matrix and its adjugate add up to the trace. So G differs from the Hermitian matrix H = i (G - G*) by a scalar matrix, and any unitary that diagonalises H diagonalises G. The eigenvector unitary supplied by the spectral theorem need not have determinant one, but it can be rescaled by a scalar of modulus one until it does (Matrix.exists_circle_smul_mem_specialUnitaryGroup), and rescaling by a scalar does not change the conjugation it induces.

Main results #

Torus conjugacy #

source
theorem TauCeti.SU2.exists_conj_mem_torus (g : SU2) :
∃ (u : SU2), u * g * u⁻¹ ∈ torus

Torus conjugacy for SU(2): every element of SU(2) is conjugate into the maximal torus. Equivalently, every special unitary 2 × 2 matrix is diagonalised by a special unitary matrix.

source
theorem TauCeti.SU2.exists_isConj_torusHom (g : SU2) :
∃ (z : Circle), IsConj g (torusHom z)

Every element of SU(2) is conjugate to the torus element diag (z, z⁻¹) for some point z of the circle: TauCeti.SU2.exists_conj_mem_torus read through the parametrisation TauCeti.SU2.torusHom of the maximal torus.

source
theorem TauCeti.SU2.exists_isConj_torusExp (g : SU2) :
∃ (θ : ℝ), IsConj g (torusExp θ)

Every element of SU(2) is conjugate to the torus element diag (e^{iθ}, e^{-iθ}) for some angle θ. This is TauCeti.SU2.exists_isConj_torusHom in the angle parametrisation.

The Weyl reflection #

source
theorem TauCeti.SU2.isConj_inv_of_mem_torus {g : SU2} (hg : g ∈ torus) :
IsConj g g⁻¹

The Weyl group of SU(2) acts on the maximal torus by inversion: every element of the torus is conjugate in SU(2) to its inverse, by the quarter turn TauCeti.SU2.weylElement that swaps the two coordinate axes. Together with TauCeti.SU2.exists_conj_mem_torus this says that every conjugacy class of SU(2) meets the torus in a nonempty set closed under inversion.

source
theorem TauCeti.SU2.isConj_torusExp_neg (θ : ℝ) :
IsConj (torusExp θ) (torusExp (-θ))

Every element of the maximal torus is conjugate to its inverse in the angle parametrisation: diag (e^{iθ}, e^{-iθ}) and diag (e^{-iθ}, e^{iθ}) are conjugate in SU(2).

Conjugacy on the maximal torus #

source
theorem TauCeti.SU2.isConj_torusHom_iff {z w : Circle} :
IsConj (torusHom z) (torusHom w) ↔ w = z ∨ w = z⁻¹

Each conjugacy class of SU(2) meets the maximal torus in exactly one Weyl orbit: two torus elements are conjugate in SU(2) precisely when they are equal or inverse. The forward direction is TauCeti.SU2.eq_or_eq_inv_of_conj_torusHom and the backward direction is the Weyl reflection TauCeti.SU2.isConj_inv_of_mem_torus.

Class functions #

source
theorem TauCeti.SU2.eq_of_conjInvariant_of_eqOn_torus {α : Type u_1} {f₁ f₂ : SU2 → α} (h₁ : ∀ (u g : SU2), f₁ (u * g * u⁻¹) = f₁ g) (h₂ : ∀ (u g : SU2), f₂ (u * g * u⁻¹) = f₂ g) (h : Set.EqOn f₁ f₂ ↑torus) :
f₁ = f₂

A class function on SU(2) is determined by its restriction to the maximal torus: two conjugation-invariant functions that agree on T agree everywhere.

source
theorem TauCeti.SU2.exists_conjInvariant_torusHom_eq {α : Type u_1} {φ : Circle → α} (hφ : ∀ (z : Circle), φ z⁻¹ = φ z) :
∃ (f : SU2 → α), (∀ (u g : SU2), f (u * g * u⁻¹) = f g) ∧ ∀ (z : Circle), f (torusHom z) = φ z

Every Weyl-invariant function on the maximal torus is the restriction of a class function on SU(2): a function on the circle that takes the same value at z and at z⁻¹ extends to a conjugation-invariant function on SU(2). The extension sends g to the value of the given function at any torus element g is conjugate to (TauCeti.SU2.exists_isConj_torusHom), which is well defined because two such torus elements are equal or inverse (TauCeti.SU2.isConj_torusHom_iff). Together with the uniqueness statement TauCeti.SU2.eq_of_conjInvariant_of_eqOn_torus this identifies the class functions of SU(2) with the W-invariant functions on T.