SU(2) and its maximal torus

SU(2) is Matrix.specialUnitaryGroup (Fin 2) ℂ, the compact group that grounds the compact-group representation theory of the compact-groups roadmap. Its compactness and topological group structure come from TauCeti/Topology/Algebra/UnitaryGroup.lean, where they are proved for every special unitary matrix group; Hausdorffness is inherited from the ambient matrix topology, SU(2) carrying the subtype topology.

This file builds the maximal torus T ⊂ SU(2), the diagonal circle subgroup

T = { diag (z, z⁻¹) : |z| = 1 },

and identifies it with Mathlib's Circle as a topological group. Three facts pin it down:

• TauCeti.SU2.mem_torus_iff: an element of SU(2) lies in T exactly when it is diagonal, so T really is the diagonal subgroup and not merely some circle inside SU(2);
• TauCeti.SU2.centralizer_torus: T is its own centralizer, whence TauCeti.SU2.eq_torus_of_isMulCommutative: T is a maximal abelian subgroup, which is what earns it the name "maximal torus";
• TauCeti.SU2.mem_torus_iff_exists_torusExp: every element of T is diag (e^{iθ}, e^{-iθ}), the parametrisation the Weyl integration and character formulas for SU(2) are stated in.

The centralizer computation is run at a single well-chosen torus element: already TauCeti.SU2.centralizer_torusHom says that diag (z, z⁻¹) with z² ≠ 1 has centralizer exactly T. Together with TauCeti.SU2.eq_or_eq_inv_of_conj_torusHom, which says that conjugating a torus element back into T can only return it or its inverse, this is the rigidity that the Weyl group of SU(2) is computed from in TauCeti/RepresentationTheory/SU2/Weyl/Basic.lean.

It also records the structural identity TauCeti.SU2.coe_add_star: an element of SU(2) and its conjugate transpose add up to (tr g) • 1, so the Hermitian part of an element of SU(2) is a scalar matrix; tracing it shows the trace is real (TauCeti.SU2.isSelfAdjoint_trace). Conjugate elements have the same trace (TauCeti.SU2.trace_eq_of_isConj). On the torus the trace is TauCeti.SU2.trace_torusMatrix: tr (diag (z, z⁻¹)) = z + z⁻¹, in the angle parametrisation TauCeti.SU2.trace_torusExp: tr (diag (e^{iθ}, e^{-iθ})) = 2 cos θ, and TauCeti.SU2.eq_or_eq_inv_of_trace_torusMatrix_eq says that this value determines z up to inversion. That the trace is a complete conjugacy invariant is proved in TauCeti/RepresentationTheory/SU2/ConjugacyClasses.lean.

Main definitions

• TauCeti.SU2: the group SU(2).
• TauCeti.SU2.torusHom: the circle parametrisation z ↦ diag (z, z⁻¹) of the maximal torus.
• TauCeti.SU2.torus: the maximal torus of SU(2), the range of torusHom.
• TauCeti.SU2.torusContinuousMulEquiv: the isomorphism of topological groups Circle ≃ₜ* T.
• TauCeti.SU2.torusExp: the torus element diag (e^{iθ}, e^{-iθ}).

@[reducible, inline]

abbrev TauCeti.SU2 : Type

SU(2), the special unitary group of 2 × 2 complex matrices. It is a compact Hausdorff topological group: the compactness and topological group instances come from TauCeti/Topology/Algebra/UnitaryGroup.lean, and Hausdorffness from the ambient matrix topology.

Equations

• TauCeti.SU2 = ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)

theorem TauCeti.SU2.coe_add_star (g : SU2) : ↑g + star ↑g = (↑g).trace • 1

An element of SU(2) and its conjugate transpose add up to (tr g) • 1: the conjugate transpose of g is its adjugate, and a 2 × 2 matrix plus its adjugate is the trace times the identity. Equivalently, the Hermitian part of g is a scalar matrix.

theorem TauCeti.SU2.isSelfAdjoint_trace (g : SU2) : IsSelfAdjoint (↑g).trace

The trace of an element of SU(2) is real. Taking traces in TauCeti.SU2.coe_add_star, g + g* = (tr g) • 1, gives tr g + conj (tr g) on the left and 2 tr g on the right.

theorem TauCeti.SU2.trace_eq_of_isConj {g h : SU2} (hgh : IsConj g h) : (↑g).trace = (↑h).trace

Conjugate elements of SU(2) have the same trace.

The diagonal matrices diag (z, z⁻¹)

noncomputable def TauCeti.SU2.torusMatrix (z : Circle) : Matrix (Fin 2) (Fin 2) ℂ

The diagonal matrix diag (z, z⁻¹) attached to a point z of the unit circle.

Equations

• TauCeti.SU2.torusMatrix z = Matrix.diagonal ![↑z, (↑z)⁻¹]

@[simp]

theorem TauCeti.SU2.torusMatrix_apply_zero_zero (z : Circle) : torusMatrix z 0 0 = ↑z

@[simp]

theorem TauCeti.SU2.torusMatrix_apply_one_one (z : Circle) : torusMatrix z 1 1 = (↑z)⁻¹

@[simp]

theorem TauCeti.SU2.torusMatrix_apply_zero_one (z : Circle) : torusMatrix z 0 1 = 0

@[simp]

theorem TauCeti.SU2.torusMatrix_apply_one_zero (z : Circle) : torusMatrix z 1 0 = 0

@[simp]

theorem TauCeti.SU2.torusMatrix_one : torusMatrix 1 = 1

@[simp]

theorem TauCeti.SU2.torusMatrix_mul (z w : Circle) : torusMatrix (z * w) = torusMatrix z * torusMatrix w

@[simp]

theorem TauCeti.SU2.star_torusMatrix (z : Circle) : star (torusMatrix z) = torusMatrix z⁻¹

@[simp]

theorem TauCeti.SU2.trace_torusMatrix (z : Circle) : (torusMatrix z).trace = ↑z + (↑z)⁻¹

The trace of the torus matrix diag (z, z⁻¹) is z + z⁻¹.

@[simp]

theorem TauCeti.SU2.det_torusMatrix (z : Circle) : (torusMatrix z).det = 1

theorem TauCeti.SU2.torusMatrix_mem (z : Circle) : torusMatrix z ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ

theorem TauCeti.SU2.continuous_torusMatrix : Continuous torusMatrix

The maximal torus

noncomputable def TauCeti.SU2.torusHom : Circle →* SU2

The circle parametrisation z ↦ diag (z, z⁻¹) of the maximal torus of SU(2).

Equations

• TauCeti.SU2.torusHom = { toFun := fun (z : Circle) => ⟨TauCeti.SU2.torusMatrix z, ⋯⟩, map_one' := TauCeti.SU2.torusHom._proof_2✝, map_mul' := TauCeti.SU2.torusHom._proof_4✝ }

@[simp]

theorem TauCeti.SU2.coe_torusHom (z : Circle) : ↑(torusHom z) = torusMatrix z

theorem TauCeti.SU2.continuous_torusHom : Continuous ⇑torusHom

noncomputable def TauCeti.SU2.torus : Subgroup SU2

The maximal torus of SU(2): the diagonal circle subgroup.

Equations

• TauCeti.SU2.torus = TauCeti.SU2.torusHom.range

theorem TauCeti.SU2.torusHom_mem_torus (z : Circle) : torusHom z ∈ torus

theorem TauCeti.SU2.mem_torus_iff_exists_torusHom {g : SU2} : g ∈ torus ↔ ∃ (z : Circle), torusHom z = g

An element of SU(2) lies in the maximal torus exactly when it is diag (z, z⁻¹) for a point z of the unit circle. This is the definition of TauCeti.SU2.torus as a range, restated as the membership lemma that puts a hand on the circle parameter of a torus element.

@[simp]

theorem TauCeti.SU2.mem_torus_iff {g : SU2} : g ∈ torus ↔ (↑g).IsDiag

An element of SU(2) lies in the maximal torus exactly when it is a diagonal matrix: unitarity makes the (0, 0) entry a point of the unit circle, and the determinant condition then forces the (1, 1) entry to be its inverse.

theorem TauCeti.SU2.torusHom_injective : Function.Injective ⇑torusHom

noncomputable def TauCeti.SU2.torusContinuousMulEquiv : Circle ≃ₜ* ↥torus

The maximal torus of SU(2) is the circle group, as a topological group.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.SU2.instCompactSpaceSubtypeMemSubgroupTorus : CompactSpace ↥torus

The diagonal maximal torus is compact, so it carries Haar probability measure.

@[simp]

theorem TauCeti.SU2.torusContinuousMulEquiv_apply (z : Circle) : ↑(torusContinuousMulEquiv z) = torusHom z

@[simp]

theorem TauCeti.SU2.torusHom_torusContinuousMulEquiv_symm (g : ↥torus) : torusHom (torusContinuousMulEquiv.symm g) = ↑g

The inverse of torusContinuousMulEquiv reads off the circle parameter of an element of the maximal torus: it is the point of Circle that torusHom sends back to that element.

instance TauCeti.SU2.instIsMulCommutativeSubtypeMemSubgroupTorus : IsMulCommutative ↥torus

Maximality

theorem TauCeti.SU2.mem_torus_of_commute_torusHom {z : Circle} (hz : ↑z ^ 2 ≠ 1) {g : SU2} (h : torusHom z * g = g * torusHom z) : g ∈ torus

An element of SU(2) commuting with a single torus element diag (z, z⁻¹) with z² ≠ 1 already lies in the maximal torus. Reading off the off-diagonal entries of diag (z, z⁻¹) g = g diag (z, z⁻¹) gives g₀₁ (z - z⁻¹) = 0 and g₁₀ (z⁻¹ - z) = 0, and z² ≠ 1 gives z ≠ z⁻¹ (TauCeti.circle_sub_inv_ne_zero).

theorem TauCeti.SU2.centralizer_torusHom {z : Circle} (hz : ↑z ^ 2 ≠ 1) : Subgroup.centralizer {torusHom z} = torus

A single torus element diag (z, z⁻¹) with z² ≠ 1 already has centralizer the maximal torus. This sharpens TauCeti.SU2.centralizer_torus, which centralizes the whole of T rather than one well-chosen element of it.

theorem TauCeti.SU2.exists_centralizer_torusHom_eq_torus : ∃ (z : Circle), Subgroup.centralizer {torusHom z} = torus

The maximal torus contains a regular element: some single element diag (z, z⁻¹) of T has centralizer exactly T. This is TauCeti.SU2.centralizer_torusHom at a point of the circle satisfying its rigidity hypothesis z² ≠ 1; the particular witness, z = i, is a proof detail of this file, and a downstream computation that must detect T by a single element needs only the existence.

theorem TauCeti.SU2.centralizer_torus : Subgroup.centralizer ↑torus = torus

The maximal torus is its own centralizer in SU(2).

theorem TauCeti.SU2.eq_torus_of_isMulCommutative {H : Subgroup SU2} [IsMulCommutative ↥H] (hH : torus ≤ H) : H = torus

The maximal torus is a maximal abelian subgroup of SU(2): a commutative subgroup containing it is equal to it.

Conjugating a torus element back into the torus

theorem TauCeti.SU2.eq_or_eq_inv_of_trace_torusMatrix_eq {z w : Circle} (h : (torusMatrix w).trace = (torusMatrix z).trace) : w = z ∨ w = z⁻¹

The trace separates the torus elements up to inversion: z and z⁻¹ are the only two points of the circle at which diag (z, z⁻¹) has a given trace, being the two roots of X² - (z + z⁻¹) X + 1.

theorem TauCeti.SU2.eq_or_eq_inv_of_conj_torusHom {z w : Circle} {g : SU2} (h : g * torusHom z * g⁻¹ = torusHom w) : w = z ∨ w = z⁻¹

Conjugating a torus element back into the maximal torus returns it or its inverse. Conjugation preserves the trace (TauCeti.SU2.trace_eq_of_isConj), and the trace separates torus elements up to inversion (TauCeti.SU2.eq_or_eq_inv_of_trace_torusMatrix_eq).

The angle parametrisation

noncomputable def TauCeti.SU2.torusExp (θ : ℝ) : SU2

The torus element diag (e^{iθ}, e^{-iθ}) of SU(2).

Equations

• TauCeti.SU2.torusExp θ = TauCeti.SU2.torusHom (Circle.exp θ)

theorem TauCeti.SU2.torusExp_def (θ : ℝ) : torusExp θ = torusHom (Circle.exp θ)

Unfolding lemma for TauCeti.SU2.torusExp: it is torusHom (Circle.exp θ). Since torusExp is not @[expose]d, this is how lemmas about torusHom are brought to bear on it.

@[simp]

theorem TauCeti.SU2.coe_torusExp (θ : ℝ) : ↑(torusExp θ) = Matrix.diagonal ![Complex.exp (↑θ * Complex.I), Complex.exp (-(↑θ * Complex.I))]

theorem TauCeti.SU2.trace_torusExp (θ : ℝ) : (↑(torusExp θ)).trace = 2 * ↑(Real.cos θ)

The trace of the torus element diag (e^{iθ}, e^{-iθ}) is 2 cos θ. This is not a simp lemma: TauCeti.SU2.coe_torusExp already rewrites the underlying matrix to a diagonal one, so its left-hand side is not in simp-normal form.

theorem TauCeti.SU2.torusExp_mem_torus (θ : ℝ) : torusExp θ ∈ torus

@[simp]

theorem TauCeti.SU2.torusExp_add (θ φ : ℝ) : torusExp (θ + φ) = torusExp θ * torusExp φ

@[simp]

theorem TauCeti.SU2.torusExp_zero : torusExp 0 = 1

@[simp]

theorem TauCeti.SU2.torusExp_neg (θ : ℝ) : torusExp (-θ) = (torusExp θ)⁻¹

theorem TauCeti.SU2.continuous_torusExp : Continuous torusExp

theorem TauCeti.SU2.mem_torus_iff_exists_torusExp {g : SU2} : g ∈ torus ↔ ∃ (θ : ℝ), g = torusExp θ

Every element of the maximal torus is diag (e^{iθ}, e^{-iθ}) for some angle θ.