Physlib.Relativity.Fermions.Weyl.DualLeftHanded

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

Dual left handed Weyl fermions

In this file we define dual Left handed Weyl fermions. These sit in the dual of the fundamental representation of SL(2,ℂ), and we consider them to have down indices ψ_α with α = 1,2.

References

A good reference for the material in this file is: https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf Although a different index convention is used there.

@[expose] public section

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

The underlying value in Fin 2 → ℂ.

structure DualLeftHandedWeyl where val : Fin 2 → ℂ

Underlying module structure

The equivalence between DualLeftHandedWeyl and Fin 2 → ℂ.

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

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

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

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

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

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

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

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

@[simps!]
def toFin2ℂEquiv : DualLeftHandedWeyl ≃ₗ[ℂ] (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 DualLeftHandedWeyl defined through the linear equivalence toFin2ℂEquiv.

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

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

Basis

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

def basis : Basis (Fin 2) ℂ DualLeftHandedWeyl := Basis.ofEquivFun
  (Equiv.linearEquiv ℂ DualLeftHandedWeyl.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 (ψ : DualLeftHandedWeyl) : ψ = ∑ i, ψ.1 i • basis i := byψ:DualLeftHandedWeyl⊢ ψ = ∑ i, ψ.val i • basis i
  conv_lhs => rw [← basis.sum_repr ψ]ψ:DualLeftHandedWeyl| ∑ 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 representation of SL(2,C) given by M → (M⁻¹)ᵀ. In index notation corresponds to a left-handed Weyl fermion with indices ψ_a.


def rep : Representation ℂ SL(2,ℂ) DualLeftHandedWeyl where
  toFun := fun M => {
    toFun := fun (ψ : DualLeftHandedWeyl) =>
      DualLeftHandedWeyl.toFin2ℂEquiv.symm ((M.1⁻¹)ᵀ *ᵥ ψ.toFin2ℂ),
    map_add' := byM:SL(2, ℂ)⊢ ∀ (x y : DualLeftHandedWeyl),
  toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ (x + y).toFin2ℂ) =
    toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ x.toFin2ℂ) + toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ y.toFin2ℂ)
      intro ψ ψ'M:SL(2, ℂ)ψ:DualLeftHandedWeylψ':DualLeftHandedWeyl⊢ toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ (ψ + ψ').toFin2ℂ) =
  toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ ψ.toFin2ℂ) + toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ ψ'.toFin2ℂ)
      simp [mulVec_add]All goals completed! 🐙
    map_smul' := byM:SL(2, ℂ)⊢ ∀ (m : ℂ) (x : DualLeftHandedWeyl),
  toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ (m • x).toFin2ℂ) = (RingHom.id ℂ) m • toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ x.toFin2ℂ)
      intro r ψM:SL(2, ℂ)r:ℂψ:DualLeftHandedWeyl⊢ toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ (r • ψ).toFin2ℂ) = (RingHom.id ℂ) r • toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ ψ.toFin2ℂ)
      simp [mulVec_smul]All goals completed! 🐙}
  map_one' := by⊢ { toFun := fun ψ => toFin2ℂEquiv.symm ((↑1)⁻¹ᵀ *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } = 1
    ext ii:DualLeftHandedWeyl⊢ { toFun := fun ψ => toFin2ℂEquiv.symm ((↑1)⁻¹ᵀ *ᵥ ψ.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))⁻¹ᵀ *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } =
  { toFun := fun ψ => toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } *
    { toFun := fun ψ => toFin2ℂEquiv.symm ((↑N)⁻¹ᵀ *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ }
    ext1 xM:SL(2, ℂ)N:SL(2, ℂ)x:DualLeftHandedWeyl⊢ { toFun := fun ψ => toFin2ℂEquiv.symm ((↑(M * N))⁻¹ᵀ *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } x =
  ({ toFun := fun ψ => toFin2ℂEquiv.symm ((↑M)⁻¹ᵀ *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ } *
      { toFun := fun ψ => toFin2ℂEquiv.symm ((↑N)⁻¹ᵀ *ᵥ ψ.toFin2ℂ), map_add' := ⋯, map_smul' := ⋯ })
    x
    simp only [SpecialLinearGroup.coe_mul, LinearMap.coe_mk, AddHom.coe_mk, Module.End.mul_apply,
      LinearEquiv.apply_symm_apply, mulVec_mulVec, EmbeddingLike.apply_eq_iff_eq]M:SL(2, ℂ)N:SL(2, ℂ)x:DualLeftHandedWeyl⊢ (↑M * ↑N)⁻¹ᵀ *ᵥ x.toFin2ℂ = ((↑M)⁻¹ᵀ * (↑N)⁻¹ᵀ) *ᵥ x.toFin2ℂ
    refine (congrFun (congrArg _ ?_) _)M:SL(2, ℂ)N:SL(2, ℂ)x:DualLeftHandedWeyl⊢ (↑M * ↑N)⁻¹ᵀ = (↑M)⁻¹ᵀ * (↑N)⁻¹ᵀ
    rw [Matrix.mul_inv_revM:SL(2, ℂ)N:SL(2, ℂ)x:DualLeftHandedWeyl⊢ ((↑N)⁻¹ * (↑M)⁻¹)ᵀ = (↑M)⁻¹ᵀ * (↑N)⁻¹ᵀM:SL(2, ℂ)N:SL(2, ℂ)x:DualLeftHandedWeyl⊢ ((↑N)⁻¹ * (↑M)⁻¹)ᵀ = (↑M)⁻¹ᵀ * (↑N)⁻¹ᵀ]M:SL(2, ℂ)N:SL(2, ℂ)x:DualLeftHandedWeyl⊢ ((↑N)⁻¹ * (↑M)⁻¹)ᵀ = (↑M)⁻¹ᵀ * (↑N)⁻¹ᵀ
    exact transpose_mul _ _All goals completed! 🐙

              

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

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

lemma rep_toMatrix (M : SL(2,ℂ)) : (LinearMap.toMatrix basis basis) (rep M) = (M.1⁻¹)ᵀ := byM:SL(2, ℂ)⊢ (LinearMap.toMatrix basis basis) (rep M) = (↑M)⁻¹ᵀ
  ext i jM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (LinearMap.toMatrix basis basis) (rep M) i j = (↑M)⁻¹ᵀ i j
  rw [LinearMap.toMatrix_applyM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis j))) i = (↑M)⁻¹ᵀ i jM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis j))) i = (↑M)⁻¹ᵀ i j]M:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis j))) i = (↑M)⁻¹ᵀ 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)⁻¹ᵀ i j
  change ((M.1⁻¹)ᵀ *ᵥ (Pi.single j 1)) i = _M:SL(2, ℂ)i:Fin 2j:Fin 2⊢ ((↑M)⁻¹ᵀ *ᵥ Pi.single j 1) i = (↑M)⁻¹ᵀ i j
  simpAll goals completed! 🐙lemma rep_apply_basis_repr (M : SL(2,ℂ)) (i j : Fin 2) :
    basis.repr (rep M (basis i)) j = M.1⁻¹ i j := byM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis i))) j = (↑M)⁻¹ i j
  fin_cases j«0»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨0, ⋯⟩) = (↑M)⁻¹ i ((fun i => i) ⟨0, ⋯⟩)«1»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨1, ⋯⟩) = (↑M)⁻¹ i ((fun i => i) ⟨1, ⋯⟩) <;>«0»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨0, ⋯⟩) = (↑M)⁻¹ i ((fun i => i) ⟨0, ⋯⟩)«1»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨1, ⋯⟩) = (↑M)⁻¹ i ((fun i => i) ⟨1, ⋯⟩) simp [rep_apply_basis]All goals completed! 🐙