6. Clifford group🔗

Clifford group is defined as the normalizer of the Pauli group. Here we assume that d ≥ 1.

Definition6.55

group✓L∃∀N

Used by 5

Hover a use site to preview it.

Preview

Lemma 6.56

Loading preview

Hover a use site to preview it.

Owner

Maris OzolsEffortmedium

The Clifford group \Cliff(d) consists of all d × d unitaries U such that U \GP(d) U^† = \GP(d), i.e., it is the normalizer of the Generalized Pauli group \GP(d), see Definition 5.54.

Lean code for Definition6.55

def cliffordGroup (d : ℕ) [NeZero d] :=
  Subgroup.normalizer (pauliGroup d).carrier

Note that according to this definition the Clifford group is infinite since U ∈ \Cliff(d) implies that e^{i \varphi} U ∈ \Cliff(d) for all \varphi ∈ ℝ. To get a finite group we need to mod out the center of \Cliff(d) which consists of all e^{i\varphi} I where \varphi ∈ ℝ.

The following lemma gives a slightly more explicit description of how Clifford group elements act on displacement operators under conjugation.

Lemma6.56

group⚠L∃∀Nused by 0

Owner

Maris OzolsEffortmedium

For each Clifford unitary U ∈ \Cliff(d) (see Definition 6.55) there exist functions f: ℤ_d^2 → ℤ_d^2 and g: ℤ_d^2 → ℝ such that U D_\p U^† = e^{i g(\p)} D_{f(\p)} for all \p ∈ ℤ_d^2.

Lean code for Lemma6.56

lemma declaration uses `sorry`cliffordGroupAction (d : ℕ) [NeZero d]
  (U : Matrix.unitaryGroup (ZMod d) ℂ)
  (hU : U ∈ cliffordGroup d)
  (p : ZMod d × ZMod d) :
    ∃ f : ZMod d × ZMod d → ZMod d × ZMod d,
    ∃ g : ZMod d × ZMod d → ℝ,
    U * (D d p.1.val p.2.val) * U.val.conjTranspose
    = Complex.exp (Complex.I * g p)
    • (D d (f p).1.val (f p).2.val) :=
  sorry