When is a given operation U a Valid encoded operation in a Stabilizer code?

“Suppose UMU† ∈ 𝒢. Then if we want an operation that takes an encoded codeword to another valid codeword, we need UMU† ∈ S. If this is true for all M ∈ S, then U|ψ〉∈ T as well, and U is a valid encoded operation.”

“The set of U such that UAU† ∈ 𝒢 for all A ∈ 𝒢 is the normalizer N(𝒢) of 𝒢 in U(n). It turns out that N(𝒢) is generated by the Hadamard gate H, the phase gate P and the CNOT. These are the gates that form a Stabilizer circuit.

lemma UMU†_stabilizes_Uψ_of_M_stabilizes_ψ (ψ : pure_state) (M : operator) (U : unitary) : 
M ψ = ψ → (U M U†) U ψ = U ψ :=
begin
  sorry
end

-- "U takes the eigenvectors of M to eigenvectors of UMU†, 
-- effectively transforming M → UMU†."

example {ψ : pure_state} : 
(X⊗X) ψ = ψ → (X⊗Z) (I⊗H) ψ = (I⊗H) ψ := 
begin
  -- intro h1,
  -- Z = HXH†,
  -- exact UMU†_stabilizes_Uψ_of_M_stabilizes_ψ (ψ) (X⊗X) (I⊗H)
  sorry
end

The set of U such that UMU† ∈ S for all M ∈ S is the normalizer N(S) of S in U(n), which need not be a subset of N(𝒢).”

“The operators in N(𝒢) acting on G by conjugation permute tensor products of X, Y, and Z.”

-- For instance: H and P generate all possible permutations of X, Y, Z.

example : HXH† = Z := by simp,
example : HZH† = X := by simp,
example : HYH† = -Y := by simp,
example : PYP† = X := by simp,
example : PXP† = Y := by simp,
example : PZP† = Z := by simp,

“Any element of N(𝒢) gives a permutation of 𝒢. These permutations are automorphisms of 𝒢: They always preserve the group structure of 𝒢.”

“Given an automorphism of 𝒢, we can always find an element of N(𝒢) that produces that automorphism, modulo the automorphism iI → −iI.

We can find the matrix of a given transformation U corresponding to some automorphism by determining the action of U on basis states. |0〉 is an eigenvector of Z, so it is mapped to an eigenvector of UZU† |1〉 = X|0〉, so it becomes (UXU†)U|0〉. For instance, the automorphism T : X → Y, Z → X maps |0〉 → (1/√2) (|0〉+ |1〉) and |1〉 → YT|0〉 = −(i/√2) (|0〉−|1〉). Thus, the matrix of T is

T = 1/√2 (1  -i)
         (1   i).

”