The Exercise

Two qubits pass through a controlled NOT (CNOT) gate $U$, the first qubit as control and the second as target. On the pair act the Pauli operators $X_1$ and $Z_1$ on the first qubit and $X_2$ and $Z_2$ on the second. The exercise is to compute the image of each of the four under conjugation by the gate, $g \mapsto U g U^\dagger$ with $U^\dagger$ the adjoint of $U$, and to write it as a product of the same four operators.

Conjugation says how an operator applied before the gate looks after it.

Two Qubits

The $4 \times 4$ matrix of an operator $M$ on two qubits, whose rows and columns are labelled by pairs of bits $(i, j)$, is $M$ with both relabelled through $(i, j) \mapsto 2i + j$, so that they follow the computational basis in the order $$|00\rangle, \quad |01\rangle, \quad |10\rangle, \quad |11\rangle .$$(1)^✦

On a single qubit, the identity $I$, the bit flip $X$ and the phase flip $Z$ are the complex $2 \times 2$ matrices $$I = \begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix}, \qquad X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}$$(2) in the basis $|0\rangle, |1\rangle$.

A Pauli operator on one qubit of the pair is the tensor product of $X$ or $Z$ on that qubit with $I$ on the other, written as a $4 \times 4$ matrix in the order (1): $$X_1 = X \otimes I ,$$(3)^✦ $$X_2 = I \otimes X ,$$(4)^✦ $$Z_1 = Z \otimes I ,$$(5)^✦ $$Z_2 = I \otimes Z .$$(6)^✦

The CNOT gate $U$ with the first qubit as control is the $4 \times 4$ matrix that exchanges $|10\rangle$ and $|11\rangle$ and fixes $|00\rangle$ and $|01\rangle$, so that it flips the second qubit exactly when the first is $1$: $$U = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{pmatrix} .$$(7)^✦

The Claim

What Is Checked

The claim is stated over the matrix $U$ of the CNOT gate (7) and the four Pauli operators (3), (4), (5) and (6), each a tensor product of matrices from (2) written in the order (1).

About these matrices the library proves the four relations (8), (9), (10) and (11), each an equality of complex $4 \times 4$ matrices.