Lean, informalized

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

Exercise 10.29 - The vectors fixed by every operator of a set, closed under linear combinations and cut out by eigenspaces

The stabilized space as a subspace and an intersection.

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

In the stabilizer formalism a quantum state is described by the operators that leave it unchanged. Given a set SS of operators on a state space VV, the exercise looks at the vectors of VV fixed by every operator in SS and asks for two facts about them. The space VSV_S stabilized by SS is the set of vectors of VV left unchanged by every operator in SS.✦

The Stabilized Space

The library states both facts for any set SS of linear operators on a module VV over a ring RR, which is a vector space when RR is a field; a quantum state space is the case where RR is the complex numbers.

The space VSV_S stabilized by SS is the set of vectors |ψ⟩|\psi\rangle of VV with g|ψ⟩=|ψ⟩g|\psi\rangle = |\psi\rangle for every operator gg in SS: VS={|ψ⟩∈V:g|ψ⟩=|ψ⟩for every g∈S}.V_S = \{\, |\psi\rangle \in V \;:\; g|\psi\rangle = |\psi\rangle \ \text{for every } g \in S \,\}.(1)✦

The eigenspace E1(g)E_1(g) of a linear operator gg on VV for the eigenvalue one is the subspace of vectors |ψ⟩|\psi\rangle of VV with g|ψ⟩=|ψ⟩g|\psi\rangle = |\psi\rangle.

The Claim

Theorem 1. Let SS be a set of linear operators on VV. If |ψ⟩|\psi\rangle and |φ⟩|\varphi\rangle lie in VSV_S, then for all scalars cc and dd in RR c|ψ⟩+d|φ⟩∈VS.c\,|\psi\rangle + d\,|\varphi\rangle \in V_S .(2)✦ Moreover, VSV_S equals the following: VS=⋂g∈SE1(g).V_S = \bigcap_{g \in S} E_1(g) .(3)✦

What Is Checked

About VSV_S itself the library also proves that it contains the zero vector.