The Exercise

The Fredkin gate is the controlled swap on three qubits.^✦ The first qubit is the control, and the gate acts on the three qubits by $$\lvert 0, x, y \rangle \mapsto \lvert 0, x, y \rangle, \qquad \lvert 1, x, y \rangle \mapsto \lvert 1, y, x \rangle .$$(1) Three Toffoli gates (the NOT on the third qubit controlled by the first two) make it, and the first and last of them can be replaced by controlled NOT (CNOT) gates with control on the second qubit and target on the third. Going further, the Fredkin gate is a circuit of six two qubit gates, and also of only five.

Three Qubits

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space, and the composite system $S \otimes T$ of two systems $S$ and $T$ is the system whose state space is the tensor product of theirs. A pure state $\lvert \psi \rangle$ of $S$ is a unit vector in the state space of $S$.^✦ The qubit is the system with state space $\mathbb{C}^2$; its basis states $\lvert 0 \rangle$ and $\lvert 1 \rangle$ are the pure states given by the standard basis vectors $(1, 0)$ and $(0, 1)$. Three qubits form the composite $\mathrm{qubit} \otimes (\mathrm{qubit} \otimes \mathrm{qubit})$, whose factors are the first, second and third qubit from the left.

A unitary $U$ of a system $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$.^✦ The identity $1$ is a unitary, and for two unitaries $U$ and $V$ of $S$, $U$ after $V$ is the unitary $UV$, first $V$ then $U$. For unitaries $U$ of $S$ and $V$ of $T$, the product unitary $U \otimes V$ of $S \otimes T$ is the tensor product of the two operators; $U \otimes 1$ is the gate $U$ on the first factor and $1 \otimes V$ the gate $V$ on the last.

The Gates

The Pauli $X$, the quantum NOT, is the unitary of the qubit with matrix $$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}.$$(2)^✦ For a unitary $U$ of a system $S$, the controlled gate $C(U)$ is the unitary of $\mathrm{qubit} \otimes S$, a control qubit and the target $S$, given by $$C(U) = \lvert 0 \rangle\langle 0 \rvert \otimes 1 + \lvert 1 \rangle\langle 1 \rvert \otimes U .$$(3) The CNOT gate is the controlled gate $C(X)$ of two qubits.^✦

The SWAP of two copies of a system $S$ is the unitary of $S \otimes S$ given by the isometry $\lvert \phi \rangle \otimes \lvert \chi \rangle \mapsto \lvert \chi \rangle \otimes \lvert \phi \rangle$. The CNOT with control below, $\mathrm{CNOT}^{\mathrm{rev}} = \mathrm{SWAP}\,\mathrm{CNOT}\,\mathrm{SWAP}$, has its control on the second qubit and its target on the first.^✦

For a unitary $U$ of the qubit, the doubly controlled gate $C^2(U) = C(C(U))$ is the unitary of three qubits that applies $U$ to the third when the first two are both $\lvert 1 \rangle$.^✦ The Toffoli gate $T$ is the doubly controlled NOT, and the Fredkin gate $F$ and the middle Toffoli gate $M$ are the controlled SWAP and the controlled $\mathrm{CNOT}^{\mathrm{rev}}$: $$T = C^2(X) = C(\mathrm{CNOT}), \qquad F = C(\mathrm{SWAP}), \qquad M = C(\mathrm{CNOT}^{\mathrm{rev}}).$$(4) The middle Toffoli gate flips the second qubit when the first and third are both $\lvert 1 \rangle$.^✦

Circuits of Two Qubit Gates

A two qubit gate $g$ on three qubits is a gate of one of four kinds, each with its unitary $U_g$ of the three qubits: an arbitrary two qubit unitary $V$ on the second and third qubits, $U_g = 1 \otimes V$; a unitary $W$ of the qubit acting on the second or the third qubit, controlled by the first, $U_g = C(W \otimes 1)$ or $U_g = C(1 \otimes W)$; an arbitrary two qubit unitary $V$ on the first and second qubits, the third idle; and one on the first and third, the second idle.^✦

The last two kinds act on qubits that the bracketing $\mathrm{qubit} \otimes (\mathrm{qubit} \otimes \mathrm{qubit})$ does not group together, and they are placed by identifications of systems. An identification $e$ of a system $S$ with a system $T$ is a linear isometric bijection from the state space of $S$ onto that of $T$.^✦ An identification $e$ of $S$ with $T$ carries a unitary $U$ of $S$ to the unitary $e\,U e^{-1}$ of $T$, the relabelling of $U$ along $e$.^✦ For three systems $A$, $B$ and $C$, the regrouping $\alpha_{A,B,C}$ identifies $A \otimes (B \otimes C)$ with $(A \otimes B) \otimes C$ by $\lvert u \rangle \otimes (\lvert v \rangle \otimes \lvert w \rangle) \mapsto (\lvert u \rangle \otimes \lvert v \rangle) \otimes \lvert w \rangle$, and the swap $\mathrm{swap}_{A,B}$ identifies $A \otimes B$ with $B \otimes A$ by $\lvert u \rangle \otimes \lvert v \rangle \mapsto \lvert v \rangle \otimes \lvert u \rangle$. Together they interchange the first two factors: $$\lambda_{A,B,C} = \alpha_{B,A,C}^{-1} \circ (\mathrm{swap}_{A,B} \otimes 1_C) \circ \alpha_{A,B,C} \colon A \otimes (B \otimes C) \to B \otimes (A \otimes C),$$(5)^✦ where $\alpha^{-1}$ is the inverse identification, $\circ$ composes identifications, the right one first, and $\mathrm{swap}_{A,B} \otimes 1_C$ is the product of the swap with the identity of $C$, acting factor by factor.

For three qubits, the gate of the third kind is $U_g = \alpha^{-1} (V \otimes 1)\, \alpha$, the relabelling of $V \otimes 1$ along $\alpha^{-1}$, and the gate of the fourth kind is $U_g = \lambda^{-1} (1 \otimes V)\, \lambda$.

A circuit of two qubit gates on three qubits is a sequence $g_1, \dots, g_n$ of such gates; its number of gates is $n$, and its unitary is the product of the unitaries of its gates, $$U(g_1, \dots, g_n) = U_{g_1} U_{g_2} \cdots U_{g_n}.$$(6)

The Claim

What Is Checked

The four equalities are stated over the Fredkin gate $F = C(\mathrm{SWAP})$ of three qubits, the Toffoli gate, the middle Toffoli gate, the CNOT gate on the second and third qubits, and, for the last two, the unitary (6) of a circuit of two qubit gates together with its number of gates.

About these constructions the library proves that each is a unitary. For every unitary $U$ of a system $S$, the controlled gate (3) satisfies $C(U)^\dagger C(U) = C(U)\, C(U)^\dagger = 1$; the matrix (2) is unitary; and products $UV$, tensor products $U \otimes V$ and relabellings $e\,U e^{-1}$ of unitaries are again unitary.