Lean, informalized

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

Exercise 2.47 - The commutator of two self-adjoint elements, times a skew-adjoint scalar, is self-adjoint

An imaginary multiple of a commutator of Hermitian operators is Hermitian.

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

Let AA and BB be Hermitian operators on a Hilbert space, and multiply their commutator by a purely imaginary number, such as ii. The exercise asks to show that the result is a Hermitian operator.

A Ring with an Adjoint

The library states the claim for elements of a ring RR, not necessarily associative and not necessarily with a unit. An adjoint on RR is a map X↦X†X \mapsto X^\dagger of RR to itself such that, for all XX and YY in RR, (X+Y)†=X†+Y†,(XY)†=Y†X†,(X†)†=X.(X + Y)^\dagger = X^\dagger + Y^\dagger, \qquad (XY)^\dagger = Y^\dagger X^\dagger, \qquad (X^\dagger)^\dagger = X.(1)

The scalars form a second ring SS, associative and with a unit, carrying a conjugation s↦s*s \mapsto s^* that is additive and gives back ss when applied twice. RR is a module over SS, and the adjoint of a multiple is the conjugate multiple of the adjoint: (sX)†=s*X†for all s∈S,X∈R.(sX)^\dagger = s^* X^\dagger \qquad \text{for all } s \in S,\ X \in R.(2)

An element AA of RR is Hermitian, or self-adjoint, if A†=AA^\dagger = A.

A scalar ss of SS is skew-adjoint if s*=−ss^* = -s.

The commutator of two elements AA and BB of RR is the element [A,B]=AB−BA.[A,B] = AB - BA.(3)

The Claim

Theorem 1. Let RR be a ring with an adjoint and a module over a ring SS of scalars with a conjugation, the two related by (2). If AA and BB are Hermitian elements of RR and ss is a skew-adjoint scalar of SS, then s[A,B]s[A,B] is Hermitian: (s[A,B])†=s[A,B].\bigl(s\,[A,B]\bigr)^\dagger = s\,[A,B].(4)✦

For the operators on a Hilbert space, with the complex numbers as scalars and complex conjugation as their conjugation, the skew-adjoint scalars are the purely imaginary numbers, and this is the exercise.

What Is Checked

What the library proves about these constructions is (4), for every such pair of rings.