1. Physlib
  2. Relativity
  3. PauliMatrices
  4. CliffordAlgebra
Imports
/- Copyright (c) 2025 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ module public import Physlib.Relativity.PauliMatrices.Basic public import Mathlib.LinearAlgebra.CliffordAlgebra.Basic

The Pauli matrices, interpreted as a Clifford algebra

@[expose] public section

The euclidean norm as a quadratic form.

@[simps!] protected noncomputable def form : QuadraticForm ℝ (Fin 3 → ℝ) := ∑ i, QuadraticMap.sq.comp (LinearMap.proj i)

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

def ofCliffordAlgebra : CliffordAlgebra PauliMatrix.form →ₐ[ℝ] Algebra.adjoin ℝ {σ1, σ2, σ3} := CliffordAlgebra.lift _ ⟨∑ i, (LinearMap.proj i).smulRight ⟨![σ1, σ2, σ3] i, Algebra.subset_adjoin <| i:Fin (Nat.succ 0).succ.succ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] i ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)} ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨0, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)}⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨1, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)}⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨2, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)} ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨0, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)}⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨1, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)}⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨2, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)} All goals completed! 🐙⟩, fun v => v:Fin 3 → ℝ⊢ (∑ i, (LinearMap.proj i).smulRight ⟨![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] i, ⋯⟩) v * (∑ i, (LinearMap.proj i).smulRight ⟨![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] i, ⋯⟩) v = (algebraMap ℝ ↥ℝ[σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)]) (PauliMatrix.form v) v:Fin 3 → ℝ⊢ ↑((∑ i, (LinearMap.proj i).smulRight ⟨![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] i, ⋯⟩) v * (∑ i, (LinearMap.proj i).smulRight ⟨![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] i, ⋯⟩) v) = ↑((algebraMap ℝ ↥ℝ[σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)]) (PauliMatrix.form v)) v:Fin 3 → ℝ⊢ v 0 • v 0 • 1 + -(v 0 • v 1 • (σ (Sum.inr 0) * σ (Sum.inr 1))) + -(v 0 • v 2 • (σ (Sum.inr 0) * σ (Sum.inr 2))) + (v 1 • v 0 • (σ (Sum.inr 0) * σ (Sum.inr 1)) + v 1 • v 1 • 1 + -(v 1 • v 2 • (σ (Sum.inr 1) * σ (Sum.inr 2)))) + (v 2 • v 0 • (σ (Sum.inr 0) * σ (Sum.inr 2)) + v 2 • v 1 • (σ (Sum.inr 1) * σ (Sum.inr 2)) + v 2 • v 2 • 1) = (v 0 * v 0 + (v 1 * v 1 + v 2 * v 2)) • 1 All goals completed! 🐙⟩

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

@[simp] lemma ofCliffordAlgebra_ι_single (i : Fin 3) (r : ℝ) : ofCliffordAlgebra (CliffordAlgebra.ι _ (Pi.single i r)) = r • ⟨![σ1, σ2, σ3] i, Algebra.subset_adjoin <| i:Fin 3r:ℝ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] i ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)} r:ℝ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨0, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)}r:ℝ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨1, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)}r:ℝ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨2, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)} r:ℝ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨0, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)}r:ℝ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨1, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)}r:ℝ⊢ ![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] ((fun i => i) ⟨2, ⋯⟩) ∈ {σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)} All goals completed! 🐙⟩ := CliffordAlgebra.lift_ι_apply _ _ _ |>.trans <| Subtype.ext <| i:Fin 3r:ℝ⊢ ↑((∑ i, (LinearMap.proj i).smulRight ⟨![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] i, ⋯⟩) (Pi.single i r)) = ↑(r • ⟨![σ (Sum.inr 0), σ (Sum.inr 1), σ (Sum.inr 2)] i, ⋯⟩) All goals completed! 🐙