U(n) = Circle · SU(n)

The determinant of a complex unitary matrix has modulus one, and every point of the circle has a card n-th root there, so a unitary matrix can be rescaled by a scalar of modulus one until its determinant is one: the unitary group is the product of the scalars of modulus one with the special unitary group. Rescaling by a scalar of modulus one keeps a matrix unitary, so nothing is lost.

Main results

• Circle.coe_mem_unitary: a point of the circle is a unitary complex number.
• Matrix.diagonal_mem_unitaryGroup_iff: a diagonal matrix is unitary exactly when its diagonal entries are.
• Matrix.exists_circle_smul_mem_specialUnitaryGroup: every complex unitary matrix becomes special unitary after multiplication by a suitable scalar of modulus one.

@[simp]

theorem Matrix.diagonal_mem_unitaryGroup_iff {n : Type u_1} {α : Type u_2} [Fintype n] [DecidableEq n] [CommRing α] [StarRing α] {d : n → α} : diagonal d ∈ unitaryGroup n α ↔ ∀ (i : n), d i ∈ unitary α

A diagonal matrix is unitary exactly when each of its diagonal entries is unitary.

theorem Circle.coe_mem_unitary (z : Circle) : ↑z ∈ unitary ℂ

A point of the circle is a unitary complex number.

theorem Matrix.exists_circle_smul_mem_specialUnitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(unitaryGroup n ℂ)) : ∃ (c : Circle), ↑c • ↑U ∈ specialUnitaryGroup n ℂ

U(n) = Circle · SU(n): every complex unitary matrix becomes special unitary after multiplication by a suitable scalar of modulus one. The scalar is a card n-th root of the inverse of the determinant, which has modulus one; the root is taken through Circle.exp.