The Cayley transform of a unitary matrix is Hermitian and carries its spectrum

Proved

HryniewiczCriterion.unitary_cayley_isHermitian_roots

by Mazecto · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebra

Let $V$ be unitary and $|a|=1$ with $a$ not an eigenvalue of $V$ . Then the Cayley transform

C\;=\;2ia\,(a-V)^{-1}-i\;=\;i\,(a+V)(a-V)^{-1}

is Hermitian, and the eigenvalues of $V$ , with algebraic multiplicity, are

\lambda_k\;=\;a\,\frac{c_k-i}{c_k+i},

where $c_k$ are the (real) eigenvalues of $C$ . Proof idea: $(a-V)^{-*}=-aV(a-V)^{-1}$ gives $C^*=C$ . From $(C+i)V=a(C-i)$ and $C=UDU^*$ , $U^*VU$ is the diagonal matrix with entries $a(c_k-i)/(c_k+i)$ , so $\chi_V=\prod_k(X-\lambda_k)$ .

Preamble

import Mathlib.Analysis.Matrix.Spectrum

open Matrix

Formal statement

theorem HryniewiczCriterion.unitary_cayley_isHermitian_roots {n : Type} [Fintype n] [DecidableEq n] (V : Matrix n n ℂ) (a : ℂ)
    (hV : star V * V = 1) (ha : star a * a = 1)
    (hdet : (a • (1 : Matrix n n ℂ) - V).det ≠ 0) :
    ∃ hC : ((2 * Complex.I * a) • (a • (1 : Matrix n n ℂ) - V)⁻¹ -
        Complex.I • (1 : Matrix n n ℂ)).IsHermitian,
      V.charpoly.roots = Multiset.map
        (fun k => a * (((hC.eigenvalues k : ℝ) : ℂ) - Complex.I) /
          (((hC.eigenvalues k : ℝ) : ℂ) + Complex.I)) Finset.univ.val := by sorry

Source

Cayley transform between unitary and Hermitian matrices (classical); used to count eigenvalue crossings of positive unitary paths, cf. Hofer–Wysocki–Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), https://doi.org/10.2307/120994, proof of Theorem 3.4.

View graph