5. Displacement operators
This section uses the generalized Pauli X and Z matrices to define the displacement operators D_{x,z}.
These operators effectively constitute the generalized Pauli or Weyl–Heisenberg group on a single quantum system of dimension d.
Unless stated otherwise, we assume that d ≥ 1.
Lean code
variable (d : ℕ) [NeZero d]
We use the generalized Pauli X and Z to define the displacement operators, see Eq. (8) in Appleby (2005).
The displacement operator corresponding to x,z ∈ ℤ is defined as
D_{x,z} = τ^{xz} X^x Z^z
where τ comes from Definition 2.9, X comes from Definition 4.1, and Z comes from Definition 4.5.
Displacement operators behave nicely under complex conjugation, see Eq. (9) in Appleby (2005).
For all x,z ∈ ℤ,
D_{x,z}^† = D_{-x,-z}
where \dagger denotes the conjugate transpose.
Lean code for Lemma5.2
Associated Lean declarations
-
conjTranspose_D[sorry in proof]
-
conjTranspose_D[sorry in proof]
@[simp]
lemma conjTranspose_D (p : ℤ × ℤ) :
(D d p)† = D d (-p) := d:ℕinst✝:NeZero dp:ℤ × ℤ⊢ (D d p)† = D d (-p)
d:ℕinst✝:NeZero dp:ℤ × ℤ⊢ (τ d ^ (p.1 * p.2) • X d ^ p.1 * Z d ^ p.2)† = τ d ^ ((-p).1 * (-p).2) • X d ^ (-p).1 * Z d ^ (-p).2; d:ℕinst✝:NeZero dp:ℤ × ℤ⊢ (τ d ^ (p.1 * p.2))⁻¹ • ((Z d)⁻¹ ^ p.2 * (X d)⁻¹ ^ p.1) = τ d ^ (p.1 * p.2) • (X d ^ (-p.1) * Z d ^ (-p.2)); d:ℕinst✝:NeZero dp:ℤ × ℤ⊢ (τ d ^ (p.1 * p.2))⁻¹ • (Z d ^ (-p.2) * X d ^ (-p.1)) = τ d ^ (p.1 * p.2) • (X d ^ (-p.1) * Z d ^ (-p.2)); All goals completed! 🐙
-- need the backwards relation for ZX_XZ and the fact that τ^2 = ω
Multiplication of displacement operators corresponds to adding their subscripts and introducing a phase given by the symplectic inner product, see Eq. (10) in Appleby (2005).
For all \p, \q ∈ ℤ^2,
D_\p D_\q = τ^{\braket{\p,\q}} D_{\p+\q}
where τ is the root of unity from Definition 2.9 and \braket{\cdot,\cdot} is the symplectic inner product from Definition 3.1.
Lean code for Lemma5.3
Associated Lean declarations
-
D_mul[sorry in proof]
-
D_mul[sorry in proof]
lemma D_mul (p q : ℤ × ℤ) :
(D d p) * (D d q) =
τ d ^ (symp p q) •
D d (p + q) := d:ℕinst✝:NeZero dp:ℤ × ℤq:ℤ × ℤ⊢ D d p * D d q = τ d ^ ⟨p,q⟩ • D d (p + q)
d:ℕinst✝:NeZero dp:ℤ × ℤq:ℤ × ℤ⊢ τ d ^ (p.1 * p.2) • X d ^ p.1 * Z d ^ p.2 * (τ d ^ (q.1 * q.2) • X d ^ q.1 * Z d ^ q.2) =
τ d ^ ⟨p,q⟩ • (τ d ^ ((p + q).1 * (p + q).2) • X d ^ (p + q).1 * Z d ^ (p + q).2); d:ℕinst✝:NeZero dp:ℤ × ℤq:ℤ × ℤ⊢ τ d ^ (q.1 * q.2) • τ d ^ (p.1 * p.2) • (X d ^ p.1 * Z d ^ p.2 * (X d ^ q.1 * Z d ^ q.2)) =
τ d ^ ⟨p,q⟩ • τ d ^ ((p.1 + q.1) * (p.2 + q.2)) • (X d ^ (p.1 + q.1) * Z d ^ (p.2 + q.2)); All goals completed! 🐙
The n-th power of a displacement operator is again a displacement operator.
For all \p \in ℤ^2 and n \geq 0,
D_\p^n = D_{n\p}.
We proceed by induction on n. The base case n = 0 gives D_\p^0 = I = D_\mathbf{0}. For the inductive step, assuming D_\p^n = D_{n\p} we get
D_\p^{n+1} = D_\p^n · D_\p = D_{n\p} \cdot D_\p = \tau^{\langle n\p,\p\rangle} D_{(n+1)\p},
where the last step used Lemma 5.3.
The result follows since \langle n\p,\p\rangle = n \langle\p,\p\rangle = 0 thanks to Lemma 3.3.
Lean code for Lemma5.4
Associated Lean declarations
-
D_pow_nsmul[sorry in proof]
-
D_pow_nsmul[sorry in proof]
lemma D_pow_nsmul (p : ℤ × ℤ) (n : ℕ) :
D d p ^ n = D d (n • p) := d:ℕinst✝:NeZero dp:ℤ × ℤn:ℕ⊢ D d p ^ n = D d (n • p)
d:ℕinst✝:NeZero dp:ℤ × ℤn:ℕ⊢ (τ d ^ (p.1 * p.2) • X d ^ p.1 * Z d ^ p.2) ^ n = τ d ^ ((n • p).1 * (n • p).2) • X d ^ (n • p).1 * Z d ^ (n • p).2; d:ℕinst✝:NeZero dp:ℤ × ℤn:ℕ⊢ (τ d ^ (p.1 * p.2) • (X d ^ p.1 * Z d ^ p.2)) ^ n =
τ d ^ (↑n * p.1 * (↑n * p.2)) • (X d ^ (↑n * p.1) * Z d ^ (↑n * p.2)); All goals completed! 🐙
If d is odd, adding a multiple of d to the index of a displacement operator does not change it, see Eq. (11) in Appleby (2005).
If d is odd then D_{\p+d\q} = D_{\p} for all \p, \q ∈ ℤ^2.
Lean code for Lemma5.5
Associated Lean declarations
-
D_add_nsmul[sorry in proof]
-
D_add_nsmul[sorry in proof]
lemma D_add_nsmul (p q : ℤ × ℤ) (hodd : Odd d) :
D d (p + d • q)
= D d p := d:ℕinst✝:NeZero dp:ℤ × ℤq:ℤ × ℤhodd:Odd d⊢ D d (p + d • q) = D d p
d:ℕinst✝:NeZero dp:ℤ × ℤq:ℤ × ℤhodd:Odd d⊢ τ d ^ ((p + d • q).1 * (p + d • q).2) • X d ^ (p + d • q).1 * Z d ^ (p + d • q).2 =
τ d ^ (p.1 * p.2) • X d ^ p.1 * Z d ^ p.2; d:ℕinst✝:NeZero dp:ℤ × ℤq:ℤ × ℤhodd:Odd d⊢ τ d ^ ((p.1 + ↑d * q.1) * (p.2 + ↑d * q.2)) • (X d ^ (p.1 + ↑d * q.1) * Z d ^ (p.2 + ↑d * q.2)) =
τ d ^ (p.1 * p.2) • (X d ^ p.1 * Z d ^ p.2); All goals completed! 🐙
-- dsimp
-- rw [Matrix.zpow_add (isUnit_X_det d), Matrix.zpow_mul (X d) (isUnit_X_det d), zpow_natCast, X_pow_d_eq_one d,
-- Matrix.one_zpow, mul_one, Matrix.zpow_add (isUnit_Z_det d), Matrix.zpow_mul (Z d) (isUnit_Z_det d), zpow_natCast,
-- Z_pow_d_eq_one, Matrix.one_zpow, mul_one, zpow_mul]
-- nth_rewrite 2 [zpow_add' (by left; exact (tau_ne_zero d))]
-- rw [zpow_mul, zpow_natCast, tau_pow_d_eq_one_of_odd d hodd, one_zpow, mul_one, ← zpow_mul, mul_comm, add_comm,
-- add_mul, zpow_add' (by left; exact (tau_ne_zero d)), mul_assoc, zpow_mul, zpow_natCast,
-- tau_pow_d_eq_one_of_odd d hodd, one_zpow, one_mul, mul_comm]
If d is odd, the index \p of a displacement operator D_\p can be treated modulo d.
In other words, it makes sense to write \p \in ℤ_d^2.
If d is odd, then for all \p \in ℤ^2,
D_\p = D_{\p \pmod d}.
Lean code for Lemma5.6
Associated Lean declarations
-
D_mod_d[sorry in proof]
-
D_mod_d[sorry in proof]
@[default_instance]
instance : EuclideanDomain ℤ := Int.euclideanDomain
lemma D_mod_d (p : ℤ × ℤ) (hodd : Odd d):
D d p = D d ⟨p.1 % d, p.2 % d⟩ :=
d:ℕinst✝:NeZero dp:ℤ × ℤhodd:Odd d⊢ D d p = D d (p.1 % ↑d, p.2 % ↑d) d:ℕinst✝:NeZero dp:ℤ × ℤhodd:Odd d⊢ τ d ^ (p.1 * p.2) • X d ^ p.1 * Z d ^ p.2 =
τ d ^ ((p.1 % ↑d, p.2 % ↑d).1 * (p.1 % ↑d, p.2 % ↑d).2) • X d ^ (p.1 % ↑d, p.2 % ↑d).1 * Z d ^ (p.1 % ↑d, p.2 % ↑d).2; d:ℕinst✝:NeZero dp:ℤ × ℤhodd:Odd d⊢ τ d ^ (p.1 * p.2) • (X d ^ p.1 * Z d ^ p.2) = τ d ^ (p.1 % ↑d * (p.2 % ↑d)) • (X d ^ (p.1 % ↑d) * Z d ^ (p.2 % ↑d)); All goals completed! 🐙
/-
by calc
D d p.1 p.2 =
D d (p.1 % d + d * (p.1 / d))
(p.2 % d + d * (p.2 / d))
:= by rw[EuclideanDomain.mod_add_div p.1];
rw[EuclideanDomain.mod_add_div p.2]
_ = D d (p.1 % d) (p.2 % d)
:= D_add_nsmul d (p.1 % d, p.2 % d)
(p.1 / d, p.2 / d) hodd
-/
The displacement operators have order d.
If d is odd, then for all \p \in ℤ^2,
D_\p^d = I.
By Lemma 5.4, D_\p^d = D_{d\p} = D_\mathbf{0} = I, using d\p = \mathbf{0} in ℤ_d^2.
Lean code for Lemma5.7
Associated Lean declarations
-
D_pow_d_eq_one[sorry in proof]
-
D_pow_d_eq_one[sorry in proof]
lemma D_pow_d_eq_one (p : ℤ × ℤ) (hOdd : Odd d) :
D d p ^ d = 1 :=
d:ℕinst✝:NeZero dp:ℤ × ℤhOdd:Odd d⊢ D d p ^ d = 1 d:ℕinst✝:NeZero dp:ℤ × ℤhOdd:Odd d⊢ (τ d ^ (p.1 * p.2) • X d ^ p.1 * Z d ^ p.2) ^ d = 1; d:ℕinst✝:NeZero dp:ℤ × ℤhOdd:Odd d⊢ (τ d ^ (p.1 * p.2) • (X d ^ p.1 * Z d ^ p.2)) ^ d = 1; All goals completed! 🐙
Displacement operators with different \p (modulo d) are indeed different.
Let \p,\q \in ℤ^2 and assume α,β ∈ ℂ are both non-zero.
If
α D_\p = β D_\q
then \p \equiv \q \pmod{d}.
This theorem always holds when d = 1.
For d > 1, (to be continues... from the assumption, you work out the matrices, take the diagonal entries at 0 and 1, and find your proof)
Lean code for Lemma5.8
Associated Lean declarations
-
D_p_neq_D_q[sorry in proof]
-
D_p_neq_D_q[sorry in proof]
lemma D_p_neq_D_q
(p q : ℤ × ℤ)
(α β : ℂ) [NeZero α] [NeZero β] :
α • (D d p) = β • (D d q) →
p = q := d:ℕinst✝²:NeZero dp:ℤ × ℤq:ℤ × ℤα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • D d p = β • D d q → p = q
All goals completed! 🐙
Displacement operators with phases that are arbitrary powers of τ form a group.
The generalized Pauli group or discrete Weyl–Heisenberg group consists of
\GP(d) = \{τ^a D_\p : a ∈ ℤ_d, \p ∈ ℤ_d^2\}
where τ is from Definition 2.9 and D_\p is from Definition 5.1.
Lean code for Definition5.9
Associated Lean declarations
-
pauliGroup[sorry in proof]
-
pauliGroup[sorry in proof]
def pauliGroup (d : ℕ) [NeZero d] :
Subgroup (Matrix.unitaryGroup (ZMod d) ℂ) where
carrier := {U | ∃ (a : ℤ) (p : ℤ × ℤ),
(U : Matrix (ZMod d) (ZMod d) ℂ) =
(τ d) ^ a • D d p}
one_mem' := d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ 1 ∈ {U | ∃ a p, ↑U = τ d ^ a • D d p} d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ ∃ p, ↑1 = τ d ^ 0 • D d p; d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ ↑1 = τ d ^ 0 • D d (0, 0); d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ 1 = D d (0, 0); d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ 1 = τ d ^ ((0, 0).1 * (0, 0).2) • X d ^ (0, 0).1 * Z d ^ (0, 0).2; All goals completed! 🐙
mul_mem' := @fun A B A' B' => sorry -- Need 5.30
inv_mem' := sorry
We could have equivalently written
\GP(d) = \{τ^a X^x Z^z : a,x,z ∈ ℤ_d\}
where X and Z are the generalized Pauli matrices.
The generalized Pauli group \GP(d) modulo its center \{\tau^a I : a \in \Z_d\} is isomorphic to ℤ_d^2.