The Clifford Algebra #

This file defines the Gamma matrices.

source

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]

Instances For

source

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]

Instances For

source

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]

Instances For

source

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]

Instances For

source

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]

source

@[simp]

theorem spaceTime.γ0_mul_γ0 :

γ0 * γ0 = 1

source

@[simp]

theorem spaceTime.γ1_mul_γ1 :

γ1 * γ1 = -1

source

@[simp]

theorem spaceTime.γ2_mul_γ2 :

γ2 * γ2 = -1

source

@[simp]

theorem spaceTime.γ3_mul_γ3 :

γ3 * γ3 = -1

source

@[simp]

theorem spaceTime.γ1_mul_γ0 :

γ1 * γ0 = -(γ0 * γ1)

source

@[simp]

theorem spaceTime.γ2_mul_γ0 :

γ2 * γ0 = -(γ0 * γ2)

source

@[simp]

theorem spaceTime.γ3_mul_γ0 :

γ3 * γ0 = -(γ0 * γ3)

source

@[simp]

theorem spaceTime.γ2_mul_γ1 :

γ2 * γ1 = -(γ1 * γ2)

source

@[simp]

theorem spaceTime.γ3_mul_γ1 :

γ3 * γ1 = -(γ1 * γ3)

source

@[simp]

theorem spaceTime.γ3_mul_γ2 :

γ3 * γ2 = -(γ2 * γ3)

source

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)

Instances For

source

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 ]

Instances For

source

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}

Instances For

source

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

γ μ ∈ γSet

source

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

Instances For

source

theorem spaceTime.γ.γSet_subset_diracAlgebra :

γSet ⊆ ↑diracAlgebra

source

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

γ μ ∈ diracAlgebra

source

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.

Instances For

source

@[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

source

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, ⋯⟩, spaceTime.γ.ofCliffordAlgebra._proof_9 ⟩

Instances For

source

@[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 γ.

PhysLean Documentation

PhysLean.Relativity.SpaceTime.CliffordAlgebra

The Clifford Algebra #