The Clifford Algebra

This file defines the Gamma matrices and their relationship to the Clifford algebra.

Main Definitions

• γ0, γ1, γ2, γ3: The four gamma matrices in the Dirac representation (4×4 complex matrices)
• γSet: The set of gamma matrices
• diracForm: The quadratic form with Minkowski signature (+,-,-,-) corresponding to the gamma matrices
• diracAlgebra: The algebra generated by the gamma matrices over ℝ
• ofCliffordAlgebra: The algebra homomorphism from the Clifford algebra to diracAlgebra

Main Results

• ofCliffordAlgebra_surjective: The homomorphism ofCliffordAlgebra is surjective

TODO

• Complete the isomorphism by proving injectivity of ofCliffordAlgebra (requires dimension theory)
• Construct the AlgEquiv between CliffordAlgebra diracForm and diracAlgebra

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]

theorem Matrix.one_fin_four {α : Type u_1} [Zero α] [One α] : 1 = !![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, 1, 0; 0, 0, 0, 1]

@[simp]

theorem spaceTime.γ0_mul_γ0 : γ0 * γ0 = 1

@[simp]

theorem spaceTime.γ1_mul_γ1 : γ1 * γ1 = -1

@[simp]

theorem spaceTime.γ2_mul_γ2 : γ2 * γ2 = -1

@[simp]

theorem spaceTime.γ3_mul_γ3 : γ3 * γ3 = -1

@[simp]

theorem spaceTime.γ1_mul_γ0 : γ1 * γ0 = -(γ0 * γ1)

@[simp]

theorem spaceTime.γ2_mul_γ0 : γ2 * γ0 = -(γ0 * γ2)

@[simp]

theorem spaceTime.γ3_mul_γ0 : γ3 * γ0 = -(γ0 * γ3)

@[simp]

theorem spaceTime.γ2_mul_γ1 : γ2 * γ1 = -(γ1 * γ2)

@[simp]

theorem spaceTime.γ3_mul_γ1 : γ3 * γ1 = -(γ1 * γ3)

@[simp]

theorem spaceTime.γ3_mul_γ2 : γ3 * γ2 = -(γ2 * γ3)

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

def spaceTime.γ.diracForm : QuadraticForm ℝ (Fin 4 → ℝ)

The quadratic form of the clifford algebra corresponding to the γ matrices.

Equations

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

@[simp]

theorem spaceTime.γ.diracForm_apply (a : Fin 4 → ℝ) : diracForm a = a 0 * a 0 - a 1 * a 1 - a 2 * a 2 - a 3 * a 3

def spaceTime.γ.ofCliffordAlgebra : CliffordAlgebra diracForm →ₐ[ℝ] ↥diracAlgebra

The injection from the clifford algebra over diracForm into the algebra generated by the γ matrices.

Equations

• spaceTime.γ.ofCliffordAlgebra = (CliffordAlgebra.lift spaceTime.γ.diracForm) ⟨∑ i : Fin 4, (LinearMap.proj i).smulRight ⟨spaceTime.γ i, ⋯⟩, ⋯⟩

@[simp]

theorem spaceTime.γ.ofCliffordAlgebra_ι_single (i : Fin 4) (r : ℝ) : ofCliffordAlgebra ((CliffordAlgebra.ι diracForm) (Pi.single i r)) = r • ⟨γ i, ⋯⟩

The generators of the clifford algebra correspond to the elements γ.

Surjectivity of ofCliffordAlgebra

theorem spaceTime.γ.γ_subtype_in_range (i : Fin 4) : ⟨γ i, ⋯⟩ ∈ ofCliffordAlgebra.range

Each gamma matrix (as an element of diracAlgebra) is in the range of ofCliffordAlgebra.

theorem spaceTime.γ.ofCliffordAlgebra_range_eq_top : ofCliffordAlgebra.range = ⊤

The range of ofCliffordAlgebra equals the top subalgebra (i.e., all of diracAlgebra).

theorem spaceTime.γ.ofCliffordAlgebra_surjective : Function.Surjective ⇑ofCliffordAlgebra

The homomorphism ofCliffordAlgebra is surjective.