The Exercise

Two qubits sit on the two wires of a circuit. A Hadamard gate acts on one wire, and nothing acts on the other. The exercise asks for the $4 \times 4$ unitary matrix of this circuit in the computational basis $|00\rangle, |01\rangle, |10\rangle, |11\rangle$, once with the Hadamard on the first qubit and once with it on the second. The library states both matrices.

Two Qubits

A quantum system $S$ is given by its state space, a finite dimensional complex Hilbert space.^✦ The qubit $Q$ is the system whose state space is $\mathbb{C}^2$.^✦ The composite system $S \otimes T$ of two systems $S$ and $T$ is the system whose state space is the tensor product of the state spaces of $S$ and $T$; the two qubits of the exercise form the composite system $Q \otimes Q$.^✦

A pure state $\psi$ of $S$ is a unit vector in the state space of $S$, $\lVert \psi \rVert = 1$.^✦ For pure states $\psi$ of $S$ and $\varphi$ of $T$, the product $\psi \otimes \varphi$ is the pure state of $S \otimes T$ whose vector is the tensor product of the two vectors.^✦ The basis state $|i\rangle$ of the qubit, for a bit $i \in \{0, 1\}$, is the pure state whose vector is the standard basis vector $e_i$ of $\mathbb{C}^2$.^✦ The products $|i_1 i_2\rangle = |i_1\rangle \otimes |i_2\rangle$ are the computational basis states of $Q \otimes Q$.

Gates on Two Qubits

A unitary $U$ of a system $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = I$.^✦ The identity evolution $I$ of $S$ is the unitary whose operator is the identity.^✦ For unitaries $U$ of $S$ and $V$ of $T$, the product unitary $U \otimes V$ is the unitary of $S \otimes T$ whose operator is the tensor product of the operators of $U$ and $V$.^✦ The gate $U$ on the first wire of $S \otimes T$ is the product unitary $U \otimes I$, with the identity evolution on $T$; the gate $V$ on the last wire is $I \otimes V$.

The Hadamard $H$ is the unitary of the qubit whose operator is the matrix $$H = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}$$(1)^✦ acting on $\mathbb{C}^2$.

The matrix $[U]$ of a gate $U$ on two qubits, a unitary of $Q \otimes Q$, is the complex matrix with rows and columns labelled by pairs of bits and entries $$[U]_{(i_1, i_2),(j_1, j_2)} = \langle i_1 i_2 |\, U \,| j_1 j_2 \rangle .$$(2)^✦ The $4 \times 4$ matrix of a matrix $M$ labelled in this way relabels both its rows and its columns through $(i, j) \mapsto 2i + j$, so that they run through $|00\rangle, |01\rangle, |10\rangle, |11\rangle$ in this order.^✦

The Claim

What Is Checked

The claim is stated over the Hadamard $H$ of the qubit, placed on the first or the last wire of $Q \otimes Q$ as the product unitary $H \otimes I$ or $I \otimes H$ with the identity evolution, and over the matrix (2) of a gate on two qubits in the basis of product states $|i_1\rangle \otimes |i_2\rangle$, relabelled as a $4 \times 4$ matrix.

Of these constructions the library proves that the matrix (1) is unitary, so that its operator on $\mathbb{C}^2$ is a unitary of the qubit; that the tensor product of two unitaries is unitary, so that $H \otimes I$ and $I \otimes H$ are unitaries of $Q \otimes Q$; and that each product $|i_1\rangle \otimes |i_2\rangle$ is a unit vector, since the norm of a product vector is the product of the norms.