Weyl fermions

A good reference for the material in this file is: https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf

def Fermion.leftHanded : Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)

The vector space ℂ^2 carrying the fundamental representation of SL(2,C). In index notation corresponds to a Weyl fermion with indices ψ^a.

Equations

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

def Fermion.leftBasis : Basis (Fin 2) ℂ ↑leftHanded.V

The standard basis on left-handed Weyl fermions.

Equations

• Fermion.leftBasis = Basis.ofEquivFun (Equiv.linearEquiv ℂ Fermion.LeftHandedModule.toFin2ℂFun)

@[simp]

theorem Fermion.leftBasis_ρ_apply (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (i j : Fin 2) : (LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M) i j = ↑M i j

@[simp]

theorem Fermion.leftBasis_toFin2ℂ (i : Fin 2) : LeftHandedModule.toFin2ℂ (leftBasis i) = Pi.single i 1

def Fermion.altLeftHanded : Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)

The vector space ℂ^2 carrying the representation of SL(2,C) given by M → (M⁻¹)ᵀ. In index notation corresponds to a Weyl fermion with indices ψ_a.

Equations

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

def Fermion.altLeftBasis : Basis (Fin 2) ℂ ↑altLeftHanded.V

The standard basis on alt-left-handed Weyl fermions.

Equations

• Fermion.altLeftBasis = Basis.ofEquivFun (Equiv.linearEquiv ℂ Fermion.AltLeftHandedModule.toFin2ℂFun)

@[simp]

theorem Fermion.altLeftBasis_toFin2ℂ (i : Fin 2) : AltLeftHandedModule.toFin2ℂ (altLeftBasis i) = Pi.single i 1

@[simp]

theorem Fermion.altLeftBasis_ρ_apply (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (i j : Fin 2) : (LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M) i j = (↑M)⁻¹.transpose i j

def Fermion.rightHanded : Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)

The vector space ℂ^2 carrying the conjugate representation of SL(2,C). In index notation corresponds to a Weyl fermion with indices ψ^{dot a}.

Equations

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

def Fermion.rightBasis : Basis (Fin 2) ℂ ↑rightHanded.V

The standard basis on right-handed Weyl fermions.

Equations

• Fermion.rightBasis = Basis.ofEquivFun (Equiv.linearEquiv ℂ Fermion.RightHandedModule.toFin2ℂFun)

@[simp]

theorem Fermion.rightBasis_toFin2ℂ (i : Fin 2) : RightHandedModule.toFin2ℂ (rightBasis i) = Pi.single i 1

@[simp]

theorem Fermion.rightBasis_ρ_apply (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (i j : Fin 2) : (LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M) i j = (↑M).map star i j

def Fermion.altRightHanded : Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)

The vector space ℂ^2 carrying the representation of SL(2,C) given by M → (M⁻¹)^†. In index notation this corresponds to a Weyl fermion with index ψ_{dot a}.

Equations

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

def Fermion.altRightBasis : Basis (Fin 2) ℂ ↑altRightHanded.V

The standard basis on alt-right-handed Weyl fermions.

Equations

• Fermion.altRightBasis = Basis.ofEquivFun (Equiv.linearEquiv ℂ Fermion.AltRightHandedModule.toFin2ℂFun)

@[simp]

theorem Fermion.altRightBasis_toFin2ℂ (i : Fin 2) : AltRightHandedModule.toFin2ℂ (altRightBasis i) = Pi.single i 1

@[simp]

theorem Fermion.altRightBasis_ρ_apply (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (i j : Fin 2) : (LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M) i j = (↑M)⁻¹.conjTranspose i j

Equivalences between Weyl fermion vector spaces.

def Fermion.leftHandedToAlt : leftHanded ⟶ altLeftHanded

The morphism between the representation leftHanded and the representation altLeftHanded defined by multiplying an element of leftHanded by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].

Equations

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

theorem Fermion.leftHandedToAlt_hom_apply (ψ : ↑leftHanded.V) : (CategoryTheory.ConcreteCategory.hom leftHandedToAlt.hom) ψ = AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0].mulVec (LeftHandedModule.toFin2ℂ ψ))

def Fermion.leftHandedAltTo : altLeftHanded ⟶ leftHanded

The morphism from altLeftHanded to leftHanded defined by multiplying an element of altLeftHandedWeyl by the matrix εₐ₁ₐ₂ = !![0, -1; 1, 0].

Equations

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

theorem Fermion.leftHandedAltTo_hom_apply (ψ : ↑altLeftHanded.V) : (CategoryTheory.ConcreteCategory.hom leftHandedAltTo.hom) ψ = LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0].mulVec (AltLeftHandedModule.toFin2ℂ ψ))

def Fermion.leftHandedAltEquiv : leftHanded ≅ altLeftHanded

The equivalence between the representation leftHanded and the representation altLeftHanded defined by multiplying an element of leftHanded by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].

Equations

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

theorem Fermion.leftHandedAltEquiv_hom_hom_apply (ψ : ↑leftHanded.V) : (CategoryTheory.ConcreteCategory.hom leftHandedAltEquiv.hom.hom) ψ = AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0].mulVec (LeftHandedModule.toFin2ℂ ψ))

leftHandedAltEquiv acting on an element ψ : leftHanded corresponds to multiplying ψ by the matrix !![0, 1; -1, 0].

theorem Fermion.leftHandedAltEquiv_inv_hom_apply (ψ : ↑altLeftHanded.V) : (CategoryTheory.ConcreteCategory.hom leftHandedAltEquiv.inv.hom) ψ = LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0].mulVec (AltLeftHandedModule.toFin2ℂ ψ))

The inverse of leftHandedAltEquiv acting on an elementψ : altLeftHanded corresponds to multiplying ψ by the matrix !![0, -1; 1, 0].

def Fermion.rightHandedWeylAltEquiv : InformalDefinition

The linear equivalence between rightHandedWeyl and altRightHandedWeyl given by multiplying an element of rightHandedWeyl by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].

Equations

• Fermion.rightHandedWeylAltEquiv = { deps := [`Fermion.rightHanded, `Fermion.altRightHanded] }

def Fermion.rightHandedWeylAltEquiv_equivariant : InformalLemma

The linear equivalence rightHandedWeylAltEquiv is equivariant with respect to the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl.

Equations

• Fermion.rightHandedWeylAltEquiv_equivariant = { deps := [`Fermion.rightHandedWeylAltEquiv] }