Clifford group

import Set_normalizer
import Pauli_group

/--
Clifford group

"The group of unitaries that normalize the Pauli group."
-/
def Clifford := {U : U(dⁿ) | ∀ M ∈ P d n, U M U† ∈ P d n} / U(1)
  • “The Clifford gates are then defined as elements in the Clifford group.”
-- Why is clifford group a group?
lemma : U₁, U₂ ∈ cliff → U₁ U₂ ∈ cliff := sorry

-- Not obvious to see that inverse is in the clifford group.
lemma : U ∈ cliff → U† ∈ cliff := sorry

-- use this lemma
lemma : α ≠ β  → α' ≠ β' := sorry

-- Cliff is stabilizer of Pauli group

-- Immediate consequence: Cliff is finite group.

lemma : |cliff| < ∞ := sorry

----- Time for some examples.

-- Single qubit first

-- phase gate
def S := (1  0
          0  i)

-- Hadamard gate
def H := 1/\sqrt{2} (1  1
                     1 -1)

-- Why are they clifford? Let them act on Paulis
-- They stabilize the Pauli group:

lemma : S X S† = Y := sorry
lemma : S Y S† = - X := sorry
lemma : S Z S† = Z := sorry

-- Do same for Hadamard

lemma : H X H† = Z := sorry
lemma : H Y H† = - Y := sorry
lemma : H Z H† = X := sorry

-- Implies `H S` operator  stabilizes Pauli group.

  • Every finite group is subgroup of Permutation group.

    • The Clifford group is a finite group.

  • Single qubit cliff induce permutation on {X, Y, Z} up to phases:

    • S corresponds to permutation between first and second element: S → (1 2).

    • HS correspond to all permutations: HS → (1 2 3).

-- If want to find clifford that maps things backwards we can find it.


/-
Geometric interpretation of single qubit cliff
-/

-- Recall Bloch representation

-- ρ = (1 + r . σ)/2

-- U ρ U† = (1 + (Rₙ(θ) r).σ))/2


-- Homomoprhism: 

-- U(2) → SO(3)

-- U → Rₙ(θ)

---- Wonderful classification of all finite groups of 

def fixes_plane := sorry --

-- rotations around axis commute so subgroup instance

def is_platonic_group G := G ∈ (T, O, I)

theorem [finite_subgroup_of_SO(3) G] : 
fixes_plane G  ∨  is_platonic_group G := sorry

-- It will turn out that ¬ fixes_plane cliff
lemma : ¬ fixes_plane cliff := sorry


-- The platonic groups

def T := sorry -- Symmetry group of the tetrahedron

def O := sorry -- Symmetry group of the Octahedron

-- Called O not C because there is a duality ... so that the new solid is an octahedron

def I := sorry -- Icoblabla

lemma : O ≅ S₄ := 
begin
  -- simple geometric construction
  -- set of diagonals of the cube
  sorry
end

lemma temp : Cliff_pereserves_hermiticity := sorry

lemma temp : Cliff_permutes_vertices_of_octahedron

-- since it doesn't fix the plane it must be platonic
lemma : is_platonic_group cliff := sorry

-- Specifically it's isomorphic to the O platonic group
theorem : cliff ≅ O := sorry

-- isomorphism between cliff and O
def φ := sorry 

lemma : φ(S) = R(π/2) → (1 2 3 4) := sorry

lemma : φ(H) = R(π) → (1 2) := sorry

lemma : surjective φ := sorry

lemma : φ(U₁) = φ(U₂) := sorry

lemma : injective φ := sorry

-- Whatever you can do to octahedron, you can do to the Paulis.

/-
How many gates from {S, H} needed to generate all single qubit clifford operations?
How many times we need to pick gate from this set to get a give cliffor operation?
Answer is 6

Example: Y = i(H S²)²  -- Might be slightly off.
-/

Gottesman many have written a paper about generalization to many qudits.

References