Modules associated with Fermions

Weyl fermions live in the vector space ℂ^2, defined here as Fin 2 → ℂ. However if we simply define the Module of Weyl fermions as Fin 2 → ℂ we get casting problems, where e.g. left-handed fermions can be cast to right-handed fermions etc. To overcome this, for each type of Weyl fermion we define a structure that wraps Fin 2 → ℂ, and these structures we define the instance of a module. This prevents casting between different types of fermions.

structure Fermion.LeftHandedModule : Type

The module in which left handed fermions live. This is equivalent to Fin 2 → ℂ.

• val : Fin 2 → ℂ

  The underlying value in Fin 2 → ℂ.

def Fermion.LeftHandedModule.toFin2ℂFun : LeftHandedModule ≃ (Fin 2 → ℂ)

The equivalence between LeftHandedModule and Fin 2 → ℂ.

Equations

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

instance Fermion.LeftHandedModule.instAddCommMonoid : AddCommMonoid LeftHandedModule

The instance of AddCommMonoid on LeftHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.LeftHandedModule.instAddCommMonoid = Fermion.LeftHandedModule.toFin2ℂFun.addCommMonoid

instance Fermion.LeftHandedModule.instAddCommGroup : AddCommGroup LeftHandedModule

The instance of AddCommGroup on LeftHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.LeftHandedModule.instAddCommGroup = Fermion.LeftHandedModule.toFin2ℂFun.addCommGroup

instance Fermion.LeftHandedModule.instModuleComplex : Module ℂ LeftHandedModule

The instance of Module on LeftHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.LeftHandedModule.instModuleComplex = Equiv.module ℂ Fermion.LeftHandedModule.toFin2ℂFun

def Fermion.LeftHandedModule.toFin2ℂEquiv : LeftHandedModule ≃ₗ[ℂ] Fin 2 → ℂ

The linear equivalence between LeftHandedModule and (Fin 2 → ℂ).

Equations

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

@[simp]

theorem Fermion.LeftHandedModule.toFin2ℂEquiv_apply (a : LeftHandedModule) (a✝ : Fin 2) : toFin2ℂEquiv a a✝ = toFin2ℂFun a a✝

@[simp]

theorem Fermion.LeftHandedModule.toFin2ℂEquiv_symm_apply_val (a : Fin 2 → ℂ) (a✝ : Fin 2) : (toFin2ℂEquiv.symm a).val a✝ = a a✝

@[reducible, inline]

abbrev Fermion.LeftHandedModule.toFin2ℂ (ψ : LeftHandedModule) : Fin 2 → ℂ

The underlying element of Fin 2 → ℂ of a element in LeftHandedModule defined through the linear equivalence toFin2ℂEquiv.

Equations

• ψ.toFin2ℂ = Fermion.LeftHandedModule.toFin2ℂEquiv ψ

structure Fermion.AltLeftHandedModule : Type

The module in which alt-left handed fermions live. This is equivalent to Fin 2 → ℂ.

• val : Fin 2 → ℂ

  The underlying value in Fin 2 → ℂ.

def Fermion.AltLeftHandedModule.toFin2ℂFun : AltLeftHandedModule ≃ (Fin 2 → ℂ)

The equivalence between AltLeftHandedModule and Fin 2 → ℂ.

Equations

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

instance Fermion.AltLeftHandedModule.instAddCommMonoid : AddCommMonoid AltLeftHandedModule

The instance of AddCommMonoid on AltLeftHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.AltLeftHandedModule.instAddCommMonoid = Fermion.AltLeftHandedModule.toFin2ℂFun.addCommMonoid

instance Fermion.AltLeftHandedModule.instAddCommGroup : AddCommGroup AltLeftHandedModule

The instance of AddCommGroup on AltLeftHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.AltLeftHandedModule.instAddCommGroup = Fermion.AltLeftHandedModule.toFin2ℂFun.addCommGroup

instance Fermion.AltLeftHandedModule.instModuleComplex : Module ℂ AltLeftHandedModule

The instance of Module on AltLeftHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.AltLeftHandedModule.instModuleComplex = Equiv.module ℂ Fermion.AltLeftHandedModule.toFin2ℂFun

def Fermion.AltLeftHandedModule.toFin2ℂEquiv : AltLeftHandedModule ≃ₗ[ℂ] Fin 2 → ℂ

The linear equivalence between AltLeftHandedModule and (Fin 2 → ℂ).

Equations

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

@[simp]

theorem Fermion.AltLeftHandedModule.toFin2ℂEquiv_apply (a : AltLeftHandedModule) (a✝ : Fin 2) : toFin2ℂEquiv a a✝ = toFin2ℂFun a a✝

@[simp]

theorem Fermion.AltLeftHandedModule.toFin2ℂEquiv_symm_apply_val (a : Fin 2 → ℂ) (a✝ : Fin 2) : (toFin2ℂEquiv.symm a).val a✝ = a a✝

@[reducible, inline]

abbrev Fermion.AltLeftHandedModule.toFin2ℂ (ψ : AltLeftHandedModule) : Fin 2 → ℂ

The underlying element of Fin 2 → ℂ of a element in AltLeftHandedModule defined through the linear equivalence toFin2ℂEquiv.

Equations

• ψ.toFin2ℂ = Fermion.AltLeftHandedModule.toFin2ℂEquiv ψ

structure Fermion.RightHandedModule : Type

The module in which right handed fermions live. This is equivalent to Fin 2 → ℂ.

• val : Fin 2 → ℂ

  The underlying value in Fin 2 → ℂ.

def Fermion.RightHandedModule.toFin2ℂFun : RightHandedModule ≃ (Fin 2 → ℂ)

The equivalence between RightHandedModule and Fin 2 → ℂ.

Equations

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

instance Fermion.RightHandedModule.instAddCommMonoid : AddCommMonoid RightHandedModule

The instance of AddCommMonoid on RightHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.RightHandedModule.instAddCommMonoid = Fermion.RightHandedModule.toFin2ℂFun.addCommMonoid

instance Fermion.RightHandedModule.instAddCommGroup : AddCommGroup RightHandedModule

The instance of AddCommGroup on RightHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.RightHandedModule.instAddCommGroup = Fermion.RightHandedModule.toFin2ℂFun.addCommGroup

instance Fermion.RightHandedModule.instModuleComplex : Module ℂ RightHandedModule

The instance of Module on RightHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.RightHandedModule.instModuleComplex = Equiv.module ℂ Fermion.RightHandedModule.toFin2ℂFun

def Fermion.RightHandedModule.toFin2ℂEquiv : RightHandedModule ≃ₗ[ℂ] Fin 2 → ℂ

The linear equivalence between RightHandedModule and (Fin 2 → ℂ).

Equations

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

@[simp]

theorem Fermion.RightHandedModule.toFin2ℂEquiv_symm_apply_val (a : Fin 2 → ℂ) (a✝ : Fin 2) : (toFin2ℂEquiv.symm a).val a✝ = a a✝

@[simp]

theorem Fermion.RightHandedModule.toFin2ℂEquiv_apply (a : RightHandedModule) (a✝ : Fin 2) : toFin2ℂEquiv a a✝ = toFin2ℂFun a a✝

@[reducible, inline]

abbrev Fermion.RightHandedModule.toFin2ℂ (ψ : RightHandedModule) : Fin 2 → ℂ

The underlying element of Fin 2 → ℂ of a element in RightHandedModule defined through the linear equivalence toFin2ℂEquiv.

Equations

• ψ.toFin2ℂ = Fermion.RightHandedModule.toFin2ℂEquiv ψ

structure Fermion.AltRightHandedModule : Type

The module in which alt-right handed fermions live. This is equivalent to Fin 2 → ℂ.

• val : Fin 2 → ℂ

  The underlying value in Fin 2 → ℂ.

def Fermion.AltRightHandedModule.toFin2ℂFun : AltRightHandedModule ≃ (Fin 2 → ℂ)

The equivalence between AltRightHandedModule and Fin 2 → ℂ.

Equations

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

instance Fermion.AltRightHandedModule.instAddCommMonoid : AddCommMonoid AltRightHandedModule

The instance of AddCommMonoid on AltRightHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.AltRightHandedModule.instAddCommMonoid = Fermion.AltRightHandedModule.toFin2ℂFun.addCommMonoid

instance Fermion.AltRightHandedModule.instAddCommGroup : AddCommGroup AltRightHandedModule

The instance of AddCommGroup on AltRightHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.AltRightHandedModule.instAddCommGroup = Fermion.AltRightHandedModule.toFin2ℂFun.addCommGroup

instance Fermion.AltRightHandedModule.instModuleComplex : Module ℂ AltRightHandedModule

The instance of Module on AltRightHandedModule defined via its equivalence with Fin 2 → ℂ.

Equations

• Fermion.AltRightHandedModule.instModuleComplex = Equiv.module ℂ Fermion.AltRightHandedModule.toFin2ℂFun

def Fermion.AltRightHandedModule.toFin2ℂEquiv : AltRightHandedModule ≃ₗ[ℂ] Fin 2 → ℂ

The linear equivalence between AltRightHandedModule and (Fin 2 → ℂ).

Equations

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

@[simp]

theorem Fermion.AltRightHandedModule.toFin2ℂEquiv_apply (a : AltRightHandedModule) (a✝ : Fin 2) : toFin2ℂEquiv a a✝ = toFin2ℂFun a a✝

@[simp]

theorem Fermion.AltRightHandedModule.toFin2ℂEquiv_symm_apply_val (a : Fin 2 → ℂ) (a✝ : Fin 2) : (toFin2ℂEquiv.symm a).val a✝ = a a✝

@[reducible, inline]

abbrev Fermion.AltRightHandedModule.toFin2ℂ (ψ : AltRightHandedModule) : Fin 2 → ℂ

The underlying element of Fin 2 → ℂ of a element in AltRightHandedModule defined through the linear equivalence toFin2ℂEquiv.

Equations

• ψ.toFin2ℂ = Fermion.AltRightHandedModule.toFin2ℂEquiv ψ