Lean, informalized

Nielsen & Chuang · Chapter 9, Distance measures for quantum information · p. 411

Exercise 9.16 - A matrix element of a tensor product in the maximally entangled vector is a trace with the transpose, not the adjoint

The maximally entangled vector gives the transpose, not the adjoint.

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 operators on a space of finite dimension with orthonormal basis {|i⟩}\{|i\rangle\}, and let |m⟩|m\rangle be the unnormalized maximally entangled vector of two copies of that space. The exercise asks to show that the trace inner product of AA and BB is a single matrix element of their tensor product, tr(A†B)=⟨m|A⊗B|m⟩\mathrm{tr}(A^\dagger B) = \langle m|A\otimes B|m\rangle.

The library refutes this identity and states the one that holds, with the transpose A⊤A^\top in place of the adjoint A†A^\dagger.

The Maximally Entangled Vector

The maximally entangled vector |m⟩|m\rangle of two copies of a system whose basis vectors |i⟩|i\rangle are labelled by a set II, over a commutative ring RR, is the identity matrix written out as a vector of the product space: its components along the product basis |i⟩|j⟩|i\rangle|j\rangle are mij=δij,i,j∈I.m_{ij} = \delta_{ij}, \qquad i, j \in I.(1)✦

The Claim

Theorem 1. Let |m⟩|m\rangle be the maximally entangled vector (1) of two copies of a complex space of dimension one. There are operators AA and BB on that space with tr(A†B)≠⟨m|A⊗B|m⟩.\mathrm{tr}(A^\dagger B) \neq \langle m|A\otimes B|m\rangle .(2)✦

Theorem 2. Let RR be a commutative ring with a conjugation r↦r*r \mapsto r^*, such as the complex numbers, let II be a finite set, and let AA and BB be square matrices over RR with rows and columns labelled by II. With |m⟩|m\rangle the maximally entangled vector (1), ⟨m|A⊗B|m⟩=tr(A⊤B).\langle m|A\otimes B|m\rangle = \mathrm{tr}(A^\top B).(3)✦

What Is Checked

Both theorems are stated over the maximally entangled vector (1) and the tensor product A⊗BA\otimes B of two square matrices. What the library proves about them is (3), over every commutative ring with a conjugation, and (2), over the complex numbers in dimension one.