The Clifford Algebra

This file defines the Gamma matrices.

def spaceTime.γ0 : Matrix (Fin 4) (Fin 4) ℂ

The γ⁰ gamma matrix in the Dirac representation.

Equations

• spaceTime.γ0 = !![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, -1, 0; 0, 0, 0, -1]

def spaceTime.γ1 : Matrix (Fin 4) (Fin 4) ℂ

The γ¹ gamma matrix in the Dirac representation.

Equations

• spaceTime.γ1 = !![0, 0, 0, 1; 0, 0, 1, 0; 0, -1, 0, 0; -1, 0, 0, 0]

def spaceTime.γ2 : Matrix (Fin 4) (Fin 4) ℂ

The γ² gamma matrix in the Dirac representation.

Equations

• spaceTime.γ2 = !![0, 0, 0, -Complex.I; 0, 0, Complex.I, 0; 0, Complex.I, 0, 0; -Complex.I, 0, 0, 0]

def spaceTime.γ3 : Matrix (Fin 4) (Fin 4) ℂ

The γ³ gamma matrix in the Dirac representation.

Equations

• spaceTime.γ3 = !![0, 0, 1, 0; 0, 0, 0, -1; -1, 0, 0, 0; 0, 1, 0, 0]

def spaceTime.γ5 : Matrix (Fin 4) (Fin 4) ℂ

The γ⁵ gamma matrix in the Dirac representation.

Equations

• spaceTime.γ5 = Complex.I • (spaceTime.γ0 * spaceTime.γ1 * spaceTime.γ2 * spaceTime.γ3)

def spaceTime.γ : Fin 4 → Matrix (Fin 4) (Fin 4) ℂ

The γ gamma matrices in the Dirac representation.

Equations

• spaceTime.γ = ![spaceTime.γ0, spaceTime.γ1, spaceTime.γ2, spaceTime.γ3]

def spaceTime.γ.γSet : Set (Matrix (Fin 4) (Fin 4) ℂ)

The subset of Matrix (Fin 4) (Fin 4) ℂ formed by the gamma matrices in the Dirac representation.

Equations

• spaceTime.γ.γSet = {x : Matrix (Fin 4) (Fin 4) ℂ | ∃ (i : Fin 4), spaceTime.γ i = x}

theorem spaceTime.γ.γ_in_γSet (μ : Fin 4) : γ μ ∈ γSet

def spaceTime.γ.diracAlgebra : Subalgebra ℝ (Matrix (Fin 4) (Fin 4) ℂ)

The algebra generated by the gamma matrices in the Dirac representation.

Equations

• spaceTime.γ.diracAlgebra = Algebra.adjoin ℝ spaceTime.γ.γSet

theorem spaceTime.γ.γSet_subset_diracAlgebra : γSet ⊆ ↑diracAlgebra

theorem spaceTime.γ.γ_in_diracAlgebra (μ : Fin 4) : γ μ ∈ diracAlgebra