Contraction of Weyl fermions

We define the contraction of Weyl fermions.

Contraction of Weyl fermions.

def Fermion.leftAltBi : ↑leftHanded.V →ₗ[ℂ] ↑altLeftHanded.V →ₗ[ℂ] ℂ

The bi-linear map corresponding to contraction of a left-handed Weyl fermion with a alt-left-handed Weyl fermion.

Equations

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

def Fermion.altLeftBi : ↑altLeftHanded.V →ₗ[ℂ] ↑leftHanded.V →ₗ[ℂ] ℂ

The bi-linear map corresponding to contraction of a alt-left-handed Weyl fermion with a left-handed Weyl fermion.

Equations

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

def Fermion.rightAltBi : ↑rightHanded.V →ₗ[ℂ] ↑altRightHanded.V →ₗ[ℂ] ℂ

The bi-linear map corresponding to contraction of a right-handed Weyl fermion with a alt-right-handed Weyl fermion.

Equations

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

def Fermion.altRightBi : ↑altRightHanded.V →ₗ[ℂ] ↑rightHanded.V →ₗ[ℂ] ℂ

The bi-linear map corresponding to contraction of a alt-right-handed Weyl fermion with a right-handed Weyl fermion.

Equations

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

def Fermion.leftAltContraction : CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded altLeftHanded ⟶ 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ))

The linear map from leftHandedWeyl ⊗ altLeftHandedWeyl to ℂ given by summing over components of leftHandedWeyl and altLeftHandedWeyl in the standard basis (i.e. the dot product). Physically, the contraction of a left-handed Weyl fermion with a alt-left-handed Weyl fermion. In index notation this is ψ^a φ_a.

Equations

• Fermion.leftAltContraction = { hom := ModuleCat.ofHom (TensorProduct.lift Fermion.leftAltBi), comm := Fermion.leftAltContraction.proof_1 }

theorem Fermion.leftAltContraction_hom_tmul (ψ : ↑leftHanded.V) (φ : ↑altLeftHanded.V) : (CategoryTheory.ConcreteCategory.hom leftAltContraction.hom) (ψ ⊗ₜ[ℂ] φ) = LeftHandedModule.toFin2ℂ ψ ⬝ᵥ AltLeftHandedModule.toFin2ℂ φ

theorem Fermion.leftAltContraction_basis (i j : Fin 2) : (CategoryTheory.ConcreteCategory.hom leftAltContraction.hom) (leftBasis i ⊗ₜ[ℂ] altLeftBasis j) = if ↑i = ↑j then 1 else 0

def Fermion.altLeftContraction : CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded leftHanded ⟶ 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ))

The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by summing over components of altLeftHandedWeyl and leftHandedWeyl in the standard basis (i.e. the dot product). Physically, the contraction of a alt-left-handed Weyl fermion with a left-handed Weyl fermion. In index notation this is φ_a ψ^a.

Equations

• Fermion.altLeftContraction = { hom := ModuleCat.ofHom (TensorProduct.lift Fermion.altLeftBi), comm := Fermion.altLeftContraction.proof_1 }

theorem Fermion.altLeftContraction_hom_tmul (φ : ↑altLeftHanded.V) (ψ : ↑leftHanded.V) : (CategoryTheory.ConcreteCategory.hom altLeftContraction.hom) (φ ⊗ₜ[ℂ] ψ) = AltLeftHandedModule.toFin2ℂ φ ⬝ᵥ LeftHandedModule.toFin2ℂ ψ

theorem Fermion.altLeftContraction_basis (i j : Fin 2) : (CategoryTheory.ConcreteCategory.hom altLeftContraction.hom) (altLeftBasis i ⊗ₜ[ℂ] leftBasis j) = if ↑i = ↑j then 1 else 0

def Fermion.rightAltContraction : CategoryTheory.MonoidalCategoryStruct.tensorObj rightHanded altRightHanded ⟶ 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ))

The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by summing over components of rightHandedWeyl and altRightHandedWeyl in the standard basis (i.e. the dot product). The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion. In index notation this is ψ^{dot a} φ_{dot a}.

Equations

• Fermion.rightAltContraction = { hom := ModuleCat.ofHom (TensorProduct.lift Fermion.rightAltBi), comm := Fermion.rightAltContraction.proof_1 }

theorem Fermion.rightAltContraction_hom_tmul (ψ : ↑rightHanded.V) (φ : ↑altRightHanded.V) : (CategoryTheory.ConcreteCategory.hom rightAltContraction.hom) (ψ ⊗ₜ[ℂ] φ) = RightHandedModule.toFin2ℂ ψ ⬝ᵥ AltRightHandedModule.toFin2ℂ φ

theorem Fermion.rightAltContraction_basis (i j : Fin 2) : (CategoryTheory.ConcreteCategory.hom rightAltContraction.hom) (rightBasis i ⊗ₜ[ℂ] altRightBasis j) = if ↑i = ↑j then 1 else 0

def Fermion.altRightContraction : CategoryTheory.MonoidalCategoryStruct.tensorObj altRightHanded rightHanded ⟶ 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ))

The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by summing over components of altRightHandedWeyl and rightHandedWeyl in the standard basis (i.e. the dot product). The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion. In index notation this is φ_{dot a} ψ^{dot a}.

Equations

• Fermion.altRightContraction = { hom := ModuleCat.ofHom (TensorProduct.lift Fermion.altRightBi), comm := Fermion.altRightContraction.proof_1 }

theorem Fermion.altRightContraction_hom_tmul (φ : ↑altRightHanded.V) (ψ : ↑rightHanded.V) : (CategoryTheory.ConcreteCategory.hom altRightContraction.hom) (φ ⊗ₜ[ℂ] ψ) = AltRightHandedModule.toFin2ℂ φ ⬝ᵥ RightHandedModule.toFin2ℂ ψ

theorem Fermion.altRightContraction_basis (i j : Fin 2) : (CategoryTheory.ConcreteCategory.hom altRightContraction.hom) (altRightBasis i ⊗ₜ[ℂ] rightBasis j) = if ↑i = ↑j then 1 else 0

Symmetry properties

theorem Fermion.leftAltContraction_tmul_symm (ψ : ↑leftHanded.V) (φ : ↑altLeftHanded.V) : (CategoryTheory.ConcreteCategory.hom leftAltContraction.hom) (ψ ⊗ₜ[ℂ] φ) = (CategoryTheory.ConcreteCategory.hom altLeftContraction.hom) (φ ⊗ₜ[ℂ] ψ)

theorem Fermion.altLeftContraction_tmul_symm (φ : ↑altLeftHanded.V) (ψ : ↑leftHanded.V) : (CategoryTheory.ConcreteCategory.hom altLeftContraction.hom) (φ ⊗ₜ[ℂ] ψ) = (CategoryTheory.ConcreteCategory.hom leftAltContraction.hom) (ψ ⊗ₜ[ℂ] φ)

theorem Fermion.rightAltContraction_tmul_symm (ψ : ↑rightHanded.V) (φ : ↑altRightHanded.V) : (CategoryTheory.ConcreteCategory.hom rightAltContraction.hom) (ψ ⊗ₜ[ℂ] φ) = (CategoryTheory.ConcreteCategory.hom altRightContraction.hom) (φ ⊗ₜ[ℂ] ψ)

theorem Fermion.altRightContraction_tmul_symm (φ : ↑altRightHanded.V) (ψ : ↑rightHanded.V) : (CategoryTheory.ConcreteCategory.hom altRightContraction.hom) (φ ⊗ₜ[ℂ] ψ) = (CategoryTheory.ConcreteCategory.hom rightAltContraction.hom) (ψ ⊗ₜ[ℂ] φ)