Units of Weyl fermions

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

def Fermion.leftAltLeftUnitVal : ↑(CategoryTheory.MonoidalCategory.tensorObj Fermion.leftHanded Fermion.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 : Fermion.leftAltLeftUnitVal = Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.altLeftBasis 0 + Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.altLeftBasis 1

Expansion of leftAltLeftUnitVal into the basis.

def Fermion.leftAltLeftUnit : 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategory.tensorObj Fermion.leftHanded Fermion.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 : Fermion.leftAltLeftUnit.hom 1 = Fermion.leftAltLeftUnitVal

def Fermion.altLeftLeftUnitVal : ↑(CategoryTheory.MonoidalCategory.tensorObj Fermion.altLeftHanded Fermion.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 : Fermion.altLeftLeftUnitVal = Fermion.altLeftBasis 0 ⊗ₜ[ℂ] Fermion.leftBasis 0 + Fermion.altLeftBasis 1 ⊗ₜ[ℂ] Fermion.leftBasis 1

Expansion of altLeftLeftUnitVal into the basis.

def Fermion.altLeftLeftUnit : 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategory.tensorObj Fermion.altLeftHanded Fermion.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 : Fermion.altLeftLeftUnit.hom 1 = Fermion.altLeftLeftUnitVal

Applying the morphism altLeftLeftUnit to 1 returns altLeftLeftUnitVal.

def Fermion.rightAltRightUnitVal : ↑(CategoryTheory.MonoidalCategory.tensorObj Fermion.rightHanded Fermion.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 : Fermion.rightAltRightUnitVal = Fermion.rightBasis 0 ⊗ₜ[ℂ] Fermion.altRightBasis 0 + Fermion.rightBasis 1 ⊗ₜ[ℂ] Fermion.altRightBasis 1

Expansion of rightAltRightUnitVal into the basis.

def Fermion.rightAltRightUnit : 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategory.tensorObj Fermion.rightHanded Fermion.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 : Fermion.rightAltRightUnit.hom 1 = Fermion.rightAltRightUnitVal

def Fermion.altRightRightUnitVal : ↑(CategoryTheory.MonoidalCategory.tensorObj Fermion.altRightHanded Fermion.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 : Fermion.altRightRightUnitVal = Fermion.altRightBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 0 + Fermion.altRightBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 1

Expansion of altRightRightUnitVal into the basis.

def Fermion.altRightRightUnit : 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategory.tensorObj Fermion.altRightHanded Fermion.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 : Fermion.altRightRightUnit.hom 1 = Fermion.altRightRightUnitVal

Contraction of the units

theorem Fermion.contr_altLeftLeftUnit (x : CoeSort.coe Fermion.leftHanded) : (CategoryTheory.MonoidalCategory.leftUnitor Fermion.leftHanded).hom.hom ((CategoryTheory.MonoidalCategory.whiskerRight Fermion.leftAltContraction Fermion.leftHanded).hom ((CategoryTheory.MonoidalCategory.associator Fermion.leftHanded Fermion.altLeftHanded Fermion.leftHanded).inv.hom (x ⊗ₜ[ℂ] Fermion.altLeftLeftUnit.hom 1))) = x

Contraction on the right with altLeftLeftUnit does nothing.

theorem Fermion.contr_leftAltLeftUnit (x : CoeSort.coe Fermion.altLeftHanded) : (CategoryTheory.MonoidalCategory.leftUnitor Fermion.altLeftHanded).hom.hom ((CategoryTheory.MonoidalCategory.whiskerRight Fermion.altLeftContraction Fermion.altLeftHanded).hom ((CategoryTheory.MonoidalCategory.associator Fermion.altLeftHanded Fermion.leftHanded Fermion.altLeftHanded).inv.hom (x ⊗ₜ[ℂ] Fermion.leftAltLeftUnit.hom 1))) = x

Contraction on the right with leftAltLeftUnit does nothing.

theorem Fermion.contr_altRightRightUnit (x : CoeSort.coe Fermion.rightHanded) : (CategoryTheory.MonoidalCategory.leftUnitor Fermion.rightHanded).hom.hom ((CategoryTheory.MonoidalCategory.whiskerRight Fermion.rightAltContraction Fermion.rightHanded).hom ((CategoryTheory.MonoidalCategory.associator Fermion.rightHanded Fermion.altRightHanded Fermion.rightHanded).inv.hom (x ⊗ₜ[ℂ] Fermion.altRightRightUnit.hom 1))) = x

Contraction on the right with altRightRightUnit does nothing.

theorem Fermion.contr_rightAltRightUnit (x : CoeSort.coe Fermion.altRightHanded) : (CategoryTheory.MonoidalCategory.leftUnitor Fermion.altRightHanded).hom.hom ((CategoryTheory.MonoidalCategory.whiskerRight Fermion.altRightContraction Fermion.altRightHanded).hom ((CategoryTheory.MonoidalCategory.associator Fermion.altRightHanded Fermion.rightHanded Fermion.altRightHanded).inv.hom (x ⊗ₜ[ℂ] Fermion.rightAltRightUnit.hom 1))) = x

Contraction on the right with rightAltRightUnit does nothing.

Symmetry properties of the units

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

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

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

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