The diagonal torus of the unitary group

The diagonal unitary matrices form a subgroup TauCeti.unitaryTorus n of the unitary group U(n) = Matrix.unitaryGroup n ℂ. A diagonal matrix is unitary exactly when its diagonal entries have modulus one (Matrix.diagonal_mem_unitaryGroup_iff), so this subgroup is the image of the injective homomorphism TauCeti.unitaryTorusHom n : (n → Circle) →* U(n), z ↦ diag (z₁, …, zₙ): a product of card n circles.

The main result is that every element of U(n) is conjugate into this torus (TauCeti.exists_conj_mem_unitaryTorus). A unitary matrix is normal, so by the spectral theorem for normal matrices (Matrix.exists_mem_unitaryGroup_star_mul_mul_eq_diagonal) it is diagonalized by a unitary change of basis, and the resulting diagonal matrix is again unitary. Read through the parametrization, every unitary matrix is conjugate in U(n) to diag (z₁, …, zₙ) for some points zᵢ of the circle, namely its eigenvalues (TauCeti.exists_isConj_unitaryTorusHom). The diagonal torus is a maximal torus of U(n), although maximality is not proved here, so this is the U(n) case of the theorem that a compact connected Lie group is the union of the conjugates of a maximal torus; for SU(2) the same statement is TauCeti.SU2.exists_conj_mem_torus.

Main definitions

• TauCeti.unitaryTorusHom: the homomorphism (n → Circle) →* U(n) onto the diagonal matrices.
• TauCeti.unitaryTorus: the diagonal torus of U(n), its range.

Main results

• TauCeti.mem_unitaryTorus_iff: the diagonal torus consists of the diagonal unitary matrices.
• TauCeti.exists_conj_mem_unitaryTorus: every element of U(n) is conjugate into the diagonal torus.
• TauCeti.exists_isConj_unitaryTorusHom: every element of U(n) is conjugate to diag (z₁, …, zₙ) for some points zᵢ of the circle.

References

• T. Bröcker, T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter IV, §1.

noncomputable def TauCeti.unitaryTorusHom (n : Type u_1) [Fintype n] [DecidableEq n] : (n → Circle) →* ↥(Matrix.unitaryGroup n ℂ)

The homomorphism (n → Circle) →* U(n) sending z to the diagonal matrix with diagonal entries z i. Its range is the diagonal torus TauCeti.unitaryTorus n.

Equations

• TauCeti.unitaryTorusHom n = { toFun := fun (z : n → Circle) => ⟨Matrix.diagonal fun (i : n) => ↑(z i), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.coe_unitaryTorusHom {n : Type u_1} [Fintype n] [DecidableEq n] (z : n → Circle) : ↑((unitaryTorusHom n) z) = Matrix.diagonal fun (i : n) => ↑(z i)

As a matrix, TauCeti.unitaryTorusHom n z is the diagonal matrix with diagonal entries z i.

theorem TauCeti.unitaryTorusHom_injective {n : Type u_1} [Fintype n] [DecidableEq n] : Function.Injective ⇑(unitaryTorusHom n)

The parametrization TauCeti.unitaryTorusHom n of the diagonal torus by card n circles is injective: distinct tuples of circle points give distinct diagonal matrices.

noncomputable def TauCeti.unitaryTorus (n : Type u_1) [Fintype n] [DecidableEq n] : Subgroup ↥(Matrix.unitaryGroup n ℂ)

The diagonal torus of the unitary group U(n): the subgroup of diagonal unitary matrices, the image of (n → Circle) under TauCeti.unitaryTorusHom n.

Equations

• TauCeti.unitaryTorus n = (TauCeti.unitaryTorusHom n).range

theorem TauCeti.mem_unitaryTorus_iff_exists_unitaryTorusHom {n : Type u_1} [Fintype n] [DecidableEq n] {g : ↥(Matrix.unitaryGroup n ℂ)} : g ∈ unitaryTorus n ↔ ∃ (z : n → Circle), (unitaryTorusHom n) z = g

An element of U(n) lies in the diagonal torus exactly when it is TauCeti.unitaryTorusHom n z for some tuple z of circle points.

theorem TauCeti.unitaryTorusHom_mem_unitaryTorus {n : Type u_1} [Fintype n] [DecidableEq n] (z : n → Circle) : (unitaryTorusHom n) z ∈ unitaryTorus n

The diagonal matrix TauCeti.unitaryTorusHom n z lies in the diagonal torus.

theorem TauCeti.mem_unitaryTorus_iff {n : Type u_1} [Fintype n] [DecidableEq n] {g : ↥(Matrix.unitaryGroup n ℂ)} : g ∈ unitaryTorus n ↔ (↑g).IsDiag

The diagonal torus of U(n) consists of exactly the unitary matrices that are diagonal.

theorem TauCeti.exists_conj_mem_unitaryTorus {n : Type u_1} [Fintype n] [DecidableEq n] (g : ↥(Matrix.unitaryGroup n ℂ)) : ∃ (u : ↥(Matrix.unitaryGroup n ℂ)), u * g * u⁻¹ ∈ unitaryTorus n

Every element of U(n) is conjugate into the diagonal torus. A unitary matrix is normal, so a unitary change of basis diagonalizes it.

theorem TauCeti.exists_isConj_unitaryTorusHom {n : Type u_1} [Fintype n] [DecidableEq n] (g : ↥(Matrix.unitaryGroup n ℂ)) : ∃ (z : n → Circle), IsConj g ((unitaryTorusHom n) z)

Every element of U(n) is conjugate to diag (z₁, …, zₙ) for some points zᵢ of the circle: TauCeti.exists_conj_mem_unitaryTorus read through the parametrization TauCeti.unitaryTorusHom of the diagonal torus.