Lean, informalized

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

Exercise 2.45 - The identity for any two elements of a ring with involution

The adjoint of a commutator is a commutator of adjoints.

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 linear operators on a Hilbert space, with adjoints A†A^\dagger and B†B^\dagger. Their commutator is the operator [A,B]=AB−BA.[A,B] = AB - BA .(1) The exercise asks for the adjoint [A,B]†[A,B]^\dagger of the commutator, written in terms of A†A^\dagger and B†B^\dagger.

A Ring with Involution

The library states the answer not for operators alone but for the elements of any ring with involution. A ring with involution is a ring RR, not necessarily associative and not necessarily with a unit, together with a map x↦x†x \mapsto x^\dagger from 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 .(2) The commutator of two elements of RR is given by the same formula (1), with the product and the difference of the ring.

The Claim

Theorem 1. Let RR be a ring with involution, and let AA and BB be elements of RR. Then [A,B]†=[B†,A†].[A,B]^\dagger = [B^\dagger, A^\dagger] .(3)✦

When RR is the ring of linear operators on a Hilbert space and †\dagger is the adjoint, this is the exercise.

What Is Checked

The claim is stated over two constructions: the involution of a ring, with the three conditions (2), and the commutator (1) formed in that ring. What the library establishes about them is the identity (3).