Physlib.Relativity.Fermions.Weyl.RightHanded

Imports

/-
Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Mathlib.Analysis.Complex.Basic
public import Physlib.Meta.TODO.Basic
public import Physlib.Relativity.SL2C.Basic
public import Physlib.Meta.Informal.Basic
public import Physlib.Meta.TODO.Basic

Right handed Weyl fermions

In this file we define Right handed Weyl fermions. These sit in the conjugate representation of SL(2,ℂ), and we consider them to have up indices ψ^{\dot α} with α = 1,2.

@[expose] public section

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

The underlying value in Fin 2 → ℂ.

structure RightHandedWeyl where val : Fin 2 → ℂ

Underlying module structure

The equivalence between RightHandedWeyl and Fin 2 → ℂ.

def toFin2ℂFun : RightHandedWeyl ≃ (Fin 2 → ℂ) where
  toFun v := v.val
  invFun f := ⟨f⟩
  left_inv _ := rfl
  right_inv _ := rfl

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

instance : AddCommMonoid RightHandedWeyl := Equiv.addCommMonoid toFin2ℂFun

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

instance : AddCommGroup RightHandedWeyl := Equiv.addCommGroup toFin2ℂFun

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

instance : Module ℂ RightHandedWeyl := Equiv.module ℂ toFin2ℂFun

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

@[simps!]
def toFin2ℂEquiv : RightHandedWeyl ≃ₗ[ℂ] (Fin 2 → ℂ) where
  toFun := toFin2ℂFun
  map_add' := fun _ _ => rfl
  map_smul' := fun _ _ => rfl
  invFun := toFin2ℂFun.symm
  left_inv := fun _ => rfl
  right_inv := fun _ => rfl

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

abbrev toFin2ℂ (ψ : RightHandedWeyl) := toFin2ℂEquiv ψ

lemma toFin2ℂ_eq_val (ψ : RightHandedWeyl) : ψ.toFin2ℂ = ψ.val := rfl

Basis

The standard basis on right-handed Weyl fermions.

def basis : Basis (Fin 2) ℂ RightHandedWeyl := Basis.ofEquivFun
  (Equiv.linearEquiv ℂ RightHandedWeyl.toFin2ℂFun)

              lemma basis_apply (i j : Fin 2) : (basis i).1 j = if j = i then 1 else 0 := byi:Fin 2j:Fin 2⊢ (basis i).val j = if j = i then 1 else 0
  simp only [basis, Equiv.linearEquiv, AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
    EquivLike.coe_coe, Equiv.invFun_as_coe, AddEquiv.coe_toEquiv_symm, Basis.coe_ofEquivFun,
    LinearEquiv.symm_mk, LinearMap.coe_mk, AddHom.coe_mk, LinearEquiv.coe_mk,
    Equiv.addEquiv_symm_apply]i:Fin 2j:Fin 2⊢ (toFin2ℂFun.symm (Pi.single i 1)).val j = if j = i then 1 else 0
  change Pi.single i 1 j = _i:Fin 2j:Fin 2⊢ Pi.single i 1 j = if j = i then 1 else 0
  simp [Pi.single_apply]All goals completed! 🐙lemma eq_sum_basis (ψ : RightHandedWeyl) : ψ = ∑ i, ψ.1 i • basis i := byψ:RightHandedWeyl⊢ ψ = ∑ i, ψ.val i • basis i
  conv_lhs => rw [← basis.sum_repr ψ]ψ:RightHandedWeyl| ∑ i, (basis.repr ψ) i • basis i
  rflAll goals completed! 🐙lemma basis_val (i : Fin 2) : (basis i).val = Pi.single i 1 := byi:Fin 2⊢ (basis i).val = Pi.single i 1
  ext ji:Fin 2j:Fin 2⊢ (basis i).val j = Pi.single i 1 j
  simp [basis_apply, Pi.single_apply]All goals completed! 🐙

Representation

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

def rep : Representation ℂ SL(2,ℂ) RightHandedWeyl where
  toFun := fun M => {
    toFun := fun (ψ : RightHandedWeyl) =>
      RightHandedWeyl.toFin2ℂEquiv.symm (M.1.map star *ᵥ ψ.toFin2ℂ),
    map_add' := byM:SL(2, ℂ)⊢ ∀ (x y : RightHandedWeyl),
  toFin2ℂEquiv.symm ((↑M).map star *ᵥ (x + y).toFin2ℂ) =
    toFin2ℂEquiv.symm ((↑M).map star *ᵥ x.toFin2ℂ) + toFin2ℂEquiv.symm ((↑M).map star *ᵥ y.toFin2ℂ)
      intro ψ ψ'M:SL(2, ℂ)ψ:RightHandedWeylψ':RightHandedWeyl⊢ toFin2ℂEquiv.symm ((↑M).map star *ᵥ (ψ + ψ').toFin2ℂ) =
  toFin2ℂEquiv.symm ((↑M).map star *ᵥ ψ.toFin2ℂ) + toFin2ℂEquiv.symm ((↑M).map star *ᵥ ψ'.toFin2ℂ)
      simp [mulVec_add]All goals completed! 🐙
    map_smul' := byM:SL(2, ℂ)⊢ ∀ (m : ℂ) (x : RightHandedWeyl),
  toFin2ℂEquiv.symm ((↑M).map star *ᵥ (m • x).toFin2ℂ) =
    (RingHom.id ℂ) m • toFin2ℂEquiv.symm ((↑M).map star *ᵥ x.toFin2ℂ)
      intro r ψM:SL(2, ℂ)r:ℂψ:RightHandedWeyl⊢ toFin2ℂEquiv.symm ((↑M).map star *ᵥ (r • ψ).toFin2ℂ) = (RingHom.id ℂ) r • toFin2ℂEquiv.symm ((↑M).map star *ᵥ ψ.toFin2ℂ)
      simp [mulVec_smul]All goals completed! 🐙}
  map_one' := by⊢ { toFun := fun ψ => toFin2ℂEquiv.symm ((↑1).map star *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } = 1
    ext ii:RightHandedWeyl⊢ { toFun := fun ψ => toFin2ℂEquiv.symm ((↑1).map star *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } i = 1 i
    simpAll goals completed! 🐙
  map_mul' := fun M N => byM:SL(2, ℂ)N:SL(2, ℂ)⊢ { toFun := fun ψ => toFin2ℂEquiv.symm ((↑(M * N)).map star *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } =
  { toFun := fun ψ => toFin2ℂEquiv.symm ((↑M).map star *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } *
    { toFun := fun ψ => toFin2ℂEquiv.symm ((↑N).map star *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ }
    ext1 xM:SL(2, ℂ)N:SL(2, ℂ)x:RightHandedWeyl⊢ { toFun := fun ψ => toFin2ℂEquiv.symm ((↑(M * N)).map star *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } x =
  ({ toFun := fun ψ => toFin2ℂEquiv.symm ((↑M).map star *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun ψ => toFin2ℂEquiv.symm ((↑N).map star *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ })
    x
    simp only [SpecialLinearGroup.coe_mul, RCLike.star_def, Matrix.map_mul, LinearMap.coe_mk,
      AddHom.coe_mk, Module.End.mul_apply, LinearEquiv.apply_symm_apply, mulVec_mulVec]All goals completed! 🐙

              lemma rep_apply (M : SL(2,ℂ)) (ψ : RightHandedWeyl) : rep M ψ = ⟨M.1.map star *ᵥ ψ.1⟩ := rfl

lemma rep_apply_eq_sum_basis (M : SL(2,ℂ)) (ψ : RightHandedWeyl) :
    rep M ψ = ∑ i, (∑ j, M.1.map star i j * ψ.1 j) • basis i := byM:SL(2, ℂ)ψ:RightHandedWeyl⊢ (rep M) ψ = ∑ i, (∑ j, (↑M).map star i j * ψ.val j) • basis i
  rw [eq_sum_basis (rep M ψ)M:SL(2, ℂ)ψ:RightHandedWeyl⊢ ∑ i, ((rep M) ψ).val i • basis i = ∑ i, (∑ j, (↑M).map star i j * ψ.val j) • basis iM:SL(2, ℂ)ψ:RightHandedWeyl⊢ ∑ i, ((rep M) ψ).val i • basis i = ∑ i, (∑ j, (↑M).map star i j * ψ.val j) • basis i]M:SL(2, ℂ)ψ:RightHandedWeyl⊢ ∑ i, ((rep M) ψ).val i • basis i = ∑ i, (∑ j, (↑M).map star i j * ψ.val j) • basis i
  rflAll goals completed! 🐙

lemma rep_apply_basis (M : SL(2,ℂ)) (i : Fin 2) :
    rep M (basis i) = ∑ j, M.1.map star j i • basis j := byM:SL(2, ℂ)i:Fin 2⊢ (rep M) (basis i) = ∑ j, (↑M).map star j i • basis j
  rw [rep_apply_eq_sum_basisM:SL(2, ℂ)i:Fin 2⊢ ∑ i_1, (∑ j, (↑M).map star i_1 j * (basis i).val j) • basis i_1 = ∑ j, (↑M).map star j i • basis jM:SL(2, ℂ)i:Fin 2⊢ ∑ i_1, (∑ j, (↑M).map star i_1 j * (basis i).val j) • basis i_1 = ∑ j, (↑M).map star j i • basis j]M:SL(2, ℂ)i:Fin 2⊢ ∑ i_1, (∑ j, (↑M).map star i_1 j * (basis i).val j) • basis i_1 = ∑ j, (↑M).map star j i • basis j
  congre_fM:SL(2, ℂ)i:Fin 2⊢ (fun i_1 => (∑ j, (↑M).map star i_1 j * (basis i).val j) • basis i_1) = fun j => (↑M).map star j i • basis j
  funext je_fM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (∑ j_1, (↑M).map star j j_1 * (basis i).val j_1) • basis j = (↑M).map star j i • basis j
  simp [basis_apply]All goals completed! 🐙

lemma rep_toMatrix (M : SL(2,ℂ)) : (LinearMap.toMatrix basis basis) (rep M) = M.1.map star := byM:SL(2, ℂ)⊢ (LinearMap.toMatrix basis basis) (rep M) = (↑M).map star
  ext i jM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (LinearMap.toMatrix basis basis) (rep M) i j = (↑M).map star i j
  rw [LinearMap.toMatrix_applyM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis j))) i = (↑M).map star i jM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis j))) i = (↑M).map star i j]M:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis j))) i = (↑M).map star i j
  simp only [basis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]M:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (Equiv.linearEquiv ℂ toFin2ℂFun) ((rep M) ((Equiv.linearEquiv ℂ toFin2ℂFun).symm (Pi.single j 1))) i = (↑M).map star i j
  change (M.1.map star *ᵥ (Pi.single j 1)) i = _M:SL(2, ℂ)i:Fin 2j:Fin 2⊢ ((↑M).map star *ᵥ Pi.single j 1) i = (↑M).map star i j
  simpAll goals completed! 🐙lemma rep_apply_basis_repr (M : SL(2,ℂ)) (i j : Fin 2) :
    basis.repr (rep M (basis i)) j = star (M.1 j i) := byM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis i))) j = star (↑M j i)
  fin_cases j«0»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨0, ⋯⟩) = star (↑M ((fun i => i) ⟨0, ⋯⟩) i)«1»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨1, ⋯⟩) = star (↑M ((fun i => i) ⟨1, ⋯⟩) i) <;>«0»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨0, ⋯⟩) = star (↑M ((fun i => i) ⟨0, ⋯⟩) i)«1»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨1, ⋯⟩) = star (↑M ((fun i => i) ⟨1, ⋯⟩) i) simp [rep_apply_basis]All goals completed! 🐙