The Pauli matrices, interpreted as a Clifford algebra

noncomputable def PauliMatrix.form : QuadraticForm ℝ (Fin 3 → ℝ)

The euclidean norm as a quadratic form.

Equations

• PauliMatrix.form = ∑ i : Fin 3, QuadraticMap.sq.comp (LinearMap.proj i)

@[simp]

theorem PauliMatrix.form_apply (a : Fin 3 → ℝ) : PauliMatrix.form a = a 0 * a 0 + (a 1 * a 1 + a ⟨2, ⋯⟩ * a ⟨2, ⋯⟩)

def PauliMatrix.ofCliffordAlgebra : CliffordAlgebra PauliMatrix.form →ₐ[ℝ] ↥(Algebra.adjoin ℝ {pauliMatrix (Sum.inr 0), pauliMatrix (Sum.inr 1), pauliMatrix (Sum.inr 2)})

The injection from the Clifford algebra over PauliMatrix.form into the algebra generated by the σ matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PauliMatrix.ofCliffordAlgebra_ι_single (i : Fin 3) (r : ℝ) : ofCliffordAlgebra ((CliffordAlgebra.ι PauliMatrix.form) (Pi.single i r)) = r • ⟨![pauliMatrix (Sum.inr 0), pauliMatrix (Sum.inr 1), pauliMatrix (Sum.inr 2)] i, ⋯⟩

The generators of the Clifford algebra correspond to the elements σ.