Lean, informalized

Nielsen & Chuang · Chapter 10, Quantum error-correction · p. 460

Exercise 10.37 - Conjugating the Pauli operator YY on the control qubit by a controlled NOT gate

YY on the control picks up XX on the target.

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

Two qubits pass through a controlled NOT gate UU, the first qubit acting as control and the second as target. The gate carries an operator gg on the two qubits to UgU†UgU^\dagger: if gg leaves a state |ψ⟩|\psi\rangle unchanged, then UgU†UgU^\dagger leaves U|ψ⟩U|\psi\rangle unchanged. The exercise takes for gg the Pauli operator YY acting on the control alone and asks for its image under the gate, written as a product of Pauli operators on the two qubits.

The library gives the answer in two forms: the image as a tensor product of two matrices on one qubit each, and as a product of an operator on the control with an operator on the target.

Two Qubits

The identity II and the Pauli matrices XX and YY of a qubit are the 2×22\times 2 complex matrices, in the computational basis |0⟩|0\rangle, |1⟩|1\rangle, I=(1001),X=(0110),Y=(0−ii0).I = \begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix}, \qquad X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}.(1)

The two qubits have the basis states |a,b⟩=|a⟩⊗|b⟩|a,b\rangle = |a\rangle\otimes|b\rangle with a,b∈{0,1}a,b\in\{0,1\}, the first label and the first factor of every tensor product belonging to the control. A matrix AA on the control acts on the pair as A1=A⊗IA_1 = A\otimes I, and a matrix BB on the target as B2=I⊗BB_2 = I\otimes B.

The controlled NOT gate UU on two qubits, with the first as control and the second as target, is the 4×44\times 4 complex matrix that flips the target exactly when the control is |1⟩|1\rangle: U|a,b⟩=|a,a⊕b⟩,U=(1000010000010010),U\,|a,b\rangle = |a,\,a\oplus b\rangle, \qquad U = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{pmatrix},(2)✦ with ⊕\oplus addition modulo 22 and the matrix written in the basis |00⟩|00\rangle, |01⟩|01\rangle, |10⟩|10\rangle, |11⟩|11\rangle. The adjoint U†U^\dagger is the conjugate transpose of UU.

The Claim

Theorem 1. Let UU be the controlled NOT gate on two qubits, with the first qubit as control. Conjugating YY on the control by UU gives UY1U†=Y⊗X,U\,Y_1\,U^\dagger = Y\otimes X ,(3)✦ and, as a product of an operator on each qubit, UY1U†=Y1X2.U\,Y_1\,U^\dagger = Y_1\,X_2 .(4)✦

What Is Checked

The claim is stated over the identity and the Pauli matrices XX and YY of (1), and over the controlled NOT gate (2) with the first qubit as control, all as complex matrices in the computational basis. About these the library proves the two identities (3) and (4), as equalities of 4×44\times 4 complex matrices.