Lean, informalized

Nielsen & Chuang · Chapter 2, Introduction to quantum mechanics · p. 84

Exercise 2.56 - Every unitary matrix written as eiKe^{iK} with KK Hermitian, its argument giving one such KK

Unitaries as exponentials of Hermitian matrices.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

The evolution of a closed quantum system whose state space has dimension nn is a unitary operator UU. The exercise asks to show that every such UU can be written U=eiKU = e^{iK} with KK a Hermitian operator.✦

Unitary and Hermitian Matrices

The library states the claim for complex n×nn \times n matrices, the operators on ℂn\mathbb{C}^n written in its standard basis. A unitary matrix UU is an n×nn \times n complex matrix with U†U=UU†=I.U^\dagger U = U U^\dagger = I .(1) A Hermitian, or self-adjoint, matrix KK is an n×nn \times n complex matrix with K†=K.K^\dagger = K .(2)

The Claim

For a Hermitian matrix KK, eiKe^{iK} is the matrix exponential of iKiK.

Theorem 1. Let UU be a unitary n×nn \times n complex matrix. Then there is a Hermitian matrix KK with eiK=U.e^{iK} = U .(3)✦

To each unitary UU the library assigns the Hermitian matrix arg⁡U=−ilog⁡U\arg U = -i\log U, the argument of UU.

Theorem 2. Let UU be a unitary n×nn \times n complex matrix. Then eiarg⁡U=U.e^{i \arg U} = U .(4)✦

What Is Checked

Both claims, (3) and (4), are stated over the unitary n×nn \times n complex matrices of (1) and the Hermitian ones of (2), through the exponential eiKe^{iK} and the argument arg⁡U\arg U.

About these constructions the library proves that eiKe^{iK} is unitary for every Hermitian KK, and that the argument arg⁡U\arg U of a unitary UU is Hermitian.