Singular values and two-sided unitary matrix orbits

Rectangular matrices lie in the same two-sided unitary orbit exactly when their singular values agree. The singular values are Mathlib's LinearMap.singularValues, applied through Matrix.toEuclideanLin; no second enumeration is introduced.

Matrix.exists_unitary_mul_diagonal_mul_unitary reads the operator singular value decomposition in the standard orthonormal basis. The orbit characterization then identifies the diagonal entries as complete invariants, including for singular matrices and in dimension zero.

For the special unitary group the determinant is a second invariant, and together with the singular values it is complete: Matrix.exists_specialUnitary_mul_mul_specialUnitary_iff_singularValues_eq_and_det_eq. The reason is that the two-sided stabilizer of a square matrix over a nonempty index type contains unitary pairs with arbitrary prescribed determinants whose product is one, and, for a singular matrix, with independently prescribed determinants (Matrix.exists_unitary_mul_mul_unitary_eq_self). Both come from rescaling one diagonal entry of the singular value decomposition.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Section 2.6.

theorem Matrix.singularValues_toEuclideanLin_unitary_mul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {κ : Type u_3} [Fintype κ] [DecidableEq κ] (A : Matrix ι κ 𝕜) (U : ↥(unitaryGroup ι 𝕜)) : (toEuclideanLin (↑U * A)).singularValues = (toEuclideanLin A).singularValues

Left multiplication by a unitary matrix preserves every singular value.

theorem Matrix.singularValues_toEuclideanLin_mul_unitary {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {κ : Type u_3} [Fintype κ] [DecidableEq κ] (A : Matrix ι κ 𝕜) (U : ↥(unitaryGroup κ 𝕜)) : (toEuclideanLin (A * ↑U)).singularValues = (toEuclideanLin A).singularValues

Right multiplication by a unitary matrix preserves every singular value.

theorem Matrix.exists_unitary_mul_diagonal_mul_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} (A : Matrix (Fin n) (Fin n) 𝕜) : ∃ (U : ↥(unitaryGroup (Fin n) 𝕜)) (V : ↥(unitaryGroup (Fin n) 𝕜)), A = (↑U * diagonal fun (i : Fin n) => ↑((toEuclideanLin A).singularValues ↑i)) * ↑V

Every square matrix is a product of two unitary matrices and the diagonal matrix of its singular values in decreasing order. Zero singular values are allowed.

theorem Matrix.singularValues_toEuclideanLin_of_unitary_mul_diagonal_mul_unitary {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} (A : Matrix (Fin n) (Fin n) 𝕜) (d : Fin n → ℝ) (hd : ∀ (i : Fin n), 0 ≤ d i) (hanti : Antitone d) (U V : ↥(unitaryGroup (Fin n) 𝕜)) (h : A = (↑U * diagonal fun (i : Fin n) => ↑(d i)) * ↑V) (i : Fin n) : (toEuclideanLin A).singularValues ↑i = d i

In a two-sided unitary factorization with a nonnegative decreasing real diagonal, the diagonal entries are the singular values.

theorem Matrix.exists_unitary_mul_mul_unitary_iff_singularValues_eq {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {κ : Type u_3} [Fintype κ] [DecidableEq κ] (A B : Matrix ι κ 𝕜) : (∃ (U : ↥(unitaryGroup ι 𝕜)) (V : ↥(unitaryGroup κ 𝕜)), B = ↑U * A * ↑V) ↔ (toEuclideanLin A).singularValues = (toEuclideanLin B).singularValues

Singular values classify two-sided unitary orbits of rectangular matrices. This is the matrix form of LinearMap.mem_twoSidedUnitaryOrbit_iff_singularValues_eq.

theorem Matrix.exists_unitary_mul_mul_unitary_eq_self {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Nonempty ι] (A : Matrix ι ι 𝕜) {a b : 𝕜} (ha : a ∈ unitary 𝕜) (hb : b ∈ unitary 𝕜) (hab : A.det = 0 ∨ a * b = 1) : ∃ (X : ↥(unitaryGroup ι 𝕜)) (Y : ↥(unitaryGroup ι 𝕜)), (↑X).det = a ∧ (↑Y).det = b ∧ ↑X * A * ↑Y = A

The two-sided stabilizer of a square matrix over a nonempty index type contains pairs of unitary matrices with any prescribed unitary determinants a and b such that a * b = 1. If the matrix is singular, a and b are arbitrary.

theorem Matrix.exists_specialUnitary_mul_mul_specialUnitary_iff_singularValues_eq_and_det_eq {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A B : Matrix ι ι 𝕜) : (∃ (U : ↥(specialUnitaryGroup ι 𝕜)) (V : ↥(specialUnitaryGroup ι 𝕜)), B = ↑U * A * ↑V) ↔ (toEuclideanLin A).singularValues = (toEuclideanLin B).singularValues ∧ A.det = B.det

Two square matrices lie in the same two-sided special unitary orbit exactly when their singular values and their determinants agree.