Units of Weyl fermions

We define the units for Weyl fermions, often denoted δ in the literature.

def Fermion.leftAltLeftUnitVal : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj leftHanded altLeftHanded).V

The left-alt-left unit δᵃₐ as an element of (leftHanded ⊗ altLeftHanded).V.

Equations

• Fermion.leftAltLeftUnitVal = Fermion.leftAltLeftToMatrix.symm 1

theorem Fermion.leftAltLeftUnitVal_expand_tmul : leftAltLeftUnitVal = leftBasis 0 ⊗ₜ[ℂ] altLeftBasis 0 + leftBasis 1 ⊗ₜ[ℂ] altLeftBasis 1

Expansion of leftAltLeftUnitVal into the basis.

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

The left-alt-left unit δᵃₐ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded , manifesting the invariance under the SL(2,ℂ) action.

Equations

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

theorem Fermion.leftAltLeftUnit_apply_one : (CategoryTheory.ConcreteCategory.hom leftAltLeftUnit.hom) 1 = leftAltLeftUnitVal

def Fermion.altLeftLeftUnitVal : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altLeftHanded leftHanded).V

The alt-left-left unit δₐᵃ as an element of (altLeftHanded ⊗ leftHanded).V.

Equations

• Fermion.altLeftLeftUnitVal = Fermion.altLeftLeftToMatrix.symm 1

theorem Fermion.altLeftLeftUnitVal_expand_tmul : altLeftLeftUnitVal = altLeftBasis 0 ⊗ₜ[ℂ] leftBasis 0 + altLeftBasis 1 ⊗ₜ[ℂ] leftBasis 1

Expansion of altLeftLeftUnitVal into the basis.

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

The alt-left-left unit δₐᵃ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded , manifesting the invariance under the SL(2,ℂ) action.

Equations

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

theorem Fermion.altLeftLeftUnit_apply_one : (CategoryTheory.ConcreteCategory.hom altLeftLeftUnit.hom) 1 = altLeftLeftUnitVal

Applying the morphism altLeftLeftUnit to 1 returns altLeftLeftUnitVal.

def Fermion.rightAltRightUnitVal : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj rightHanded altRightHanded).V

The right-alt-right unit δ^{dot a}_{dot a} as an element of (rightHanded ⊗ altRightHanded).V.

Equations

• Fermion.rightAltRightUnitVal = Fermion.rightAltRightToMatrix.symm 1

theorem Fermion.rightAltRightUnitVal_expand_tmul : rightAltRightUnitVal = rightBasis 0 ⊗ₜ[ℂ] altRightBasis 0 + rightBasis 1 ⊗ₜ[ℂ] altRightBasis 1

Expansion of rightAltRightUnitVal into the basis.

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

The right-alt-right unit δ^{dot a}_{dot a} as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHanded, manifesting the invariance under the SL(2,ℂ) action.

Equations

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

theorem Fermion.rightAltRightUnit_apply_one : (CategoryTheory.ConcreteCategory.hom rightAltRightUnit.hom) 1 = rightAltRightUnitVal

def Fermion.altRightRightUnitVal : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj altRightHanded rightHanded).V

The alt-right-right unit δ_{dot a}^{dot a} as an element of (rightHanded ⊗ altRightHanded).V.

Equations

• Fermion.altRightRightUnitVal = Fermion.altRightRightToMatrix.symm 1

theorem Fermion.altRightRightUnitVal_expand_tmul : altRightRightUnitVal = altRightBasis 0 ⊗ₜ[ℂ] rightBasis 0 + altRightBasis 1 ⊗ₜ[ℂ] rightBasis 1

Expansion of altRightRightUnitVal into the basis.

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

The alt-right-right unit δ_{dot a}^{dot a} as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHanded, manifesting the invariance under the SL(2,ℂ) action.

Equations

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

theorem Fermion.altRightRightUnit_apply_one : (CategoryTheory.ConcreteCategory.hom altRightRightUnit.hom) 1 = altRightRightUnitVal

Contraction of the units

theorem Fermion.contr_altLeftLeftUnit (x : ↑leftHanded.V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor leftHanded).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight leftAltContraction leftHanded).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator leftHanded altLeftHanded leftHanded).inv.hom) (x ⊗ₜ[ℂ] (CategoryTheory.ConcreteCategory.hom altLeftLeftUnit.hom) 1))) = x

Contraction on the right with altLeftLeftUnit does nothing.

theorem Fermion.contr_leftAltLeftUnit (x : ↑altLeftHanded.V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor altLeftHanded).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight altLeftContraction altLeftHanded).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator altLeftHanded leftHanded altLeftHanded).inv.hom) (x ⊗ₜ[ℂ] (CategoryTheory.ConcreteCategory.hom leftAltLeftUnit.hom) 1))) = x

Contraction on the right with leftAltLeftUnit does nothing.

theorem Fermion.contr_altRightRightUnit (x : ↑rightHanded.V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor rightHanded).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight rightAltContraction rightHanded).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator rightHanded altRightHanded rightHanded).inv.hom) (x ⊗ₜ[ℂ] (CategoryTheory.ConcreteCategory.hom altRightRightUnit.hom) 1))) = x

Contraction on the right with altRightRightUnit does nothing.

theorem Fermion.contr_rightAltRightUnit (x : ↑altRightHanded.V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor altRightHanded).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight altRightContraction altRightHanded).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator altRightHanded rightHanded altRightHanded).inv.hom) (x ⊗ₜ[ℂ] (CategoryTheory.ConcreteCategory.hom rightAltRightUnit.hom) 1))) = x

Contraction on the right with rightAltRightUnit does nothing.

Symmetry properties of the units

theorem Fermion.altLeftLeftUnit_symm : (CategoryTheory.ConcreteCategory.hom altLeftLeftUnit.hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft altLeftHanded (CategoryTheory.CategoryStruct.id leftHanded)).hom) ((CategoryTheory.ConcreteCategory.hom (β_ leftHanded altLeftHanded).hom.hom) ((CategoryTheory.ConcreteCategory.hom leftAltLeftUnit.hom) 1))

theorem Fermion.leftAltLeftUnit_symm : (CategoryTheory.ConcreteCategory.hom leftAltLeftUnit.hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft leftHanded (CategoryTheory.CategoryStruct.id altLeftHanded)).hom) ((CategoryTheory.ConcreteCategory.hom (β_ altLeftHanded leftHanded).hom.hom) ((CategoryTheory.ConcreteCategory.hom altLeftLeftUnit.hom) 1))

theorem Fermion.altRightRightUnit_symm : (CategoryTheory.ConcreteCategory.hom altRightRightUnit.hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft altRightHanded (CategoryTheory.CategoryStruct.id rightHanded)).hom) ((CategoryTheory.ConcreteCategory.hom (β_ rightHanded altRightHanded).hom.hom) ((CategoryTheory.ConcreteCategory.hom rightAltRightUnit.hom) 1))

theorem Fermion.rightAltRightUnit_symm : (CategoryTheory.ConcreteCategory.hom rightAltRightUnit.hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft rightHanded (CategoryTheory.CategoryStruct.id altRightHanded)).hom) ((CategoryTheory.ConcreteCategory.hom (β_ altRightHanded rightHanded).hom.hom) ((CategoryTheory.ConcreteCategory.hom altRightRightUnit.hom) 1))