Metrics of Weyl fermions #

We define the metrics for Weyl fermions, often denoted ε in the literature. These allow us to go from left-handed to alt-left-handed Weyl fermions and back, and from right-handed to alt-right-handed Weyl fermions and back.

source

def Fermion.metricRaw :

Matrix (Fin 2) (Fin 2) ℂ

The raw 2x2 matrix corresponding to the metric for fermions.

Equations

Fermion.metricRaw = !![0, 1; -1, 0]

Instances For

source

theorem Fermion.comm_metricRaw (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :

↑M * metricRaw = metricRaw * (↑M)⁻¹.transpose

Multiplying an element of SL(2, ℂ) on the left with the metric 𝓔 is equivalent to multiplying the inverse-transpose of that element on the right with the metric.

source

theorem Fermion.metricRaw_comm (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :

metricRaw * ↑M = (↑M)⁻¹.transpose * metricRaw

source

theorem Fermion.star_comm_metricRaw (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :

(↑M).map star * metricRaw = metricRaw * (↑M)⁻¹.conjTranspose

source

theorem Fermion.metricRaw_comm_star (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :

metricRaw * (↑M).map star = (↑M)⁻¹.conjTranspose * metricRaw

source

def Fermion.leftMetricVal :

↑(CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded leftHanded).V

The metric εᵃᵃ as an element of (leftHanded ⊗ leftHanded).V.

Equations

Fermion.leftMetricVal = Fermion.leftLeftToMatrix.symm (-Fermion.metricRaw)

Instances For

source

theorem Fermion.leftMetricVal_expand_tmul :

leftMetricVal = -leftBasis 0 ⊗ₜ[ℂ ] leftBasis 1 + leftBasis 1 ⊗ₜ[ℂ ] leftBasis 0

Expansion of leftMetricVal into the left basis.

source

def Fermion.leftMetric :

𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded leftHanded

The metric εᵃᵃ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded, making manifest its invariance under the action of SL(2,ℂ).

Equations

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

Instances For

source

theorem Fermion.leftMetric_apply_one :

(CategoryTheory.ConcreteCategory.hom leftMetric.hom) 1 = leftMetricVal

source

def Fermion.altLeftMetricVal :

↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded altLeftHanded).V

The metric εₐₐ as an element of (altLeftHanded ⊗ altLeftHanded).V.

Equations

Fermion.altLeftMetricVal = Fermion.altLeftaltLeftToMatrix.symm Fermion.metricRaw

Instances For

source

theorem Fermion.altLeftMetricVal_expand_tmul :

altLeftMetricVal = altLeftBasis 0 ⊗ₜ[ℂ ] altLeftBasis 1 - altLeftBasis 1 ⊗ₜ[ℂ ] altLeftBasis 0

Expansion of altLeftMetricVal into the left basis.

source

def Fermion.altLeftMetric :

𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded altLeftHanded

The metric εₐₐ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHanded, making manifest its invariance under the action of SL(2,ℂ).

Equations

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

Instances For

source

theorem Fermion.altLeftMetric_apply_one :

(CategoryTheory.ConcreteCategory.hom altLeftMetric.hom) 1 = altLeftMetricVal

source

def Fermion.rightMetricVal :

↑(CategoryTheory.MonoidalCategoryStruct.tensorObj rightHanded rightHanded).V

The metric ε^{dot a}^{dot a} as an element of (rightHanded ⊗ rightHanded).V.

Equations

Fermion.rightMetricVal = Fermion.rightRightToMatrix.symm (-Fermion.metricRaw)

Instances For

source

theorem Fermion.rightMetricVal_expand_tmul :

rightMetricVal = -rightBasis 0 ⊗ₜ[ℂ ] rightBasis 1 + rightBasis 1 ⊗ₜ[ℂ ] rightBasis 0

Expansion of rightMetricVal into the left basis.

source

def Fermion.rightMetric :

𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj rightHanded rightHanded

The metric ε^{dot a}^{dot a} as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded, making manifest its invariance under the action of SL(2,ℂ).

Equations

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

Instances For

source

theorem Fermion.rightMetric_apply_one :

(CategoryTheory.ConcreteCategory.hom rightMetric.hom) 1 = rightMetricVal

source

def Fermion.altRightMetricVal :

↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altRightHanded altRightHanded).V

The metric ε_{dot a}_{dot a} as an element of (altRightHanded ⊗ altRightHanded).V.

Equations

Fermion.altRightMetricVal = Fermion.altRightAltRightToMatrix.symm Fermion.metricRaw

Instances For

source

theorem Fermion.altRightMetricVal_expand_tmul :

altRightMetricVal = altRightBasis 0 ⊗ₜ[ℂ ] altRightBasis 1 - altRightBasis 1 ⊗ₜ[ℂ ] altRightBasis 0

Expansion of rightMetricVal into the left basis.

source

def Fermion.altRightMetric :

𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj altRightHanded altRightHanded

The metric ε_{dot a}_{dot a} as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHanded, making manifest its invariance under the action of SL(2,ℂ).

Equations

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

Instances For

source

theorem Fermion.altRightMetric_apply_one :

(CategoryTheory.ConcreteCategory.hom altRightMetric.hom) 1 = altRightMetricVal

Contraction of metrics #

source

theorem Fermion.leftAltContraction_apply_metric :

source

theorem Fermion.altLeftContraction_apply_metric :

source

theorem Fermion.rightAltContraction_apply_metric :

source

theorem Fermion.altRightContraction_apply_metric :

PhysLean Documentation

PhysLean.Relativity.Lorentz.Weyl.Metric

Metrics of Weyl fermions #

Contraction of metrics #