Spectrum of a Kronecker product of Hermitian matrices #
For Hermitian matrices A and B over ℂ, the eigenvalues of the Kronecker
product A ⊗ₖ B are exactly the pairwise products λᵢ · μⱼ of the eigenvalues
of A and B. Because eigenvalues are stored as sorted tuples, the pointwise
statement is false; the correct invariant is the equality of the multisets of
eigenvalues, which is what eigenvalues_kronecker_multiset records.
The proof is the cleanest available route: the spectral theorem writes
A = U Dₐ Uᴴ and B = V D_b Vᴴ with U, V unitary and Dₐ, D_b real
diagonal, so A ⊗ₖ B = W (Dₐ ⊗ₖ D_b) Wᴴ with W = U ⊗ₖ V unitary. Hence
A ⊗ₖ B and the diagonal matrix Dₐ ⊗ₖ D_b = diagonal (λ q, λ_{q.1} μ_{q.2})
have the same characteristic polynomial, and the eigenvalue multiset is read off
from Matrix.IsHermitian.roots_charpoly_eq_eigenvalues together with the roots
of a product of linear factors.
The Kronecker product of two Hermitian matrices is Hermitian.
The multiset of roots of ∏ i, (X - C (d i)) over a finite index type is the
image multiset of d.
Eigenvalues of a Kronecker product. For Hermitian A, B over ℂ, the
multiset of eigenvalues of A ⊗ₖ B equals the multiset of pairwise products
λ_{q.1} · μ_{q.2} of the eigenvalues of A and B.