Physlib.Relativity.Fermions.Weyl.LeftHanded

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

Left handed Weyl fermions

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

@[expose] public section

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

The underlying value in Fin 2 → ℂ.

structure LeftHandedWeyl where val : Fin 2 → ℂ

Underlying module structure

The equivalence between LeftHandedWeyl and Fin 2 → ℂ.

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

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

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

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

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

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

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

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

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

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

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

Basis

The standard basis on left-handed Weyl fermions.

def basis : Basis (Fin 2) ℂ LeftHandedWeyl := Basis.ofEquivFun
  (Equiv.linearEquiv ℂ LeftHandedWeyl.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 (ψ : LeftHandedWeyl) : ψ = ∑ i, ψ.1 i • basis i := byψ:LeftHandedWeyl⊢ ψ = ∑ i, ψ.val i • basis i
  conv_lhs => rw [← basis.sum_repr ψ]ψ:LeftHandedWeyl| ∑ 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 fundamental representation of SL(2,C). In index notation corresponds to a Weyl fermion with indices ψ^a.

def rep : Representation ℂ SL(2,ℂ) LeftHandedWeyl where
  toFun := fun M => {
    toFun := fun (ψ : LeftHandedWeyl) =>
      LeftHandedWeyl.toFin2ℂEquiv.symm (M.1 *ᵥ ψ.toFin2ℂ),
    map_add' := byM:SL(2, ℂ)⊢ ∀ (x y : LeftHandedWeyl),
  toFin2ℂEquiv.symm (↑M *ᵥ (x + y).toFin2ℂ) = toFin2ℂEquiv.symm (↑M *ᵥ x.toFin2ℂ) + toFin2ℂEquiv.symm (↑M *ᵥ y.toFin2ℂ)
      intro ψ ψ'M:SL(2, ℂ)ψ:LeftHandedWeylψ':LeftHandedWeyl⊢ 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 : LeftHandedWeyl),
  toFin2ℂEquiv.symm (↑M *ᵥ (m • x).toFin2ℂ) = (RingHom.id ℂ) m • toFin2ℂEquiv.symm (↑M *ᵥ x.toFin2ℂ)
      intro r ψM:SL(2, ℂ)r:ℂψ:LeftHandedWeyl⊢ 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:LeftHandedWeyl⊢ { 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' := ⋯ }
    simp only [SpecialLinearGroup.coe_mul]M: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:LeftHandedWeyl⊢ { 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 [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,ℂ)) (ψ : LeftHandedWeyl) : rep M ψ = ⟨M.1 *ᵥ ψ.1⟩ := rfl

lemma rep_apply_eq_sum_basis (M : SL(2,ℂ)) (ψ : LeftHandedWeyl) :
    rep M ψ = ∑ i, (∑ j, M.1 i j * ψ.1 j) • basis i := byM:SL(2, ℂ)ψ:LeftHandedWeyl⊢ (rep M) ψ = ∑ i, (∑ j, ↑M i j * ψ.val j) • basis i
  rw [eq_sum_basis (rep M ψ)M:SL(2, ℂ)ψ:LeftHandedWeyl⊢ ∑ i, ((rep M) ψ).val i • basis i = ∑ i, (∑ j, ↑M i j * ψ.val j) • basis iM:SL(2, ℂ)ψ:LeftHandedWeyl⊢ ∑ i, ((rep M) ψ).val i • basis i = ∑ i, (∑ j, ↑M i j * ψ.val j) • basis i]M:SL(2, ℂ)ψ:LeftHandedWeyl⊢ ∑ i, ((rep M) ψ).val i • basis i = ∑ i, (∑ j, ↑M 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 j i • basis j := byM:SL(2, ℂ)i:Fin 2⊢ (rep M) (basis i) = ∑ j, ↑M j i • basis j
  rw [rep_apply_eq_sum_basisM:SL(2, ℂ)i:Fin 2⊢ ∑ i_1, (∑ j, ↑M i_1 j * (basis i).val j) • basis i_1 = ∑ j, ↑M j i • basis jM:SL(2, ℂ)i:Fin 2⊢ ∑ i_1, (∑ j, ↑M i_1 j * (basis i).val j) • basis i_1 = ∑ j, ↑M j i • basis j]M:SL(2, ℂ)i:Fin 2⊢ ∑ i_1, (∑ j, ↑M i_1 j * (basis i).val j) • basis i_1 = ∑ j, ↑M j i • basis j
  congre_fM:SL(2, ℂ)i:Fin 2⊢ (fun i_1 => (∑ j, ↑M i_1 j * (basis i).val j) • basis i_1) = fun j => ↑M j i • basis j
  funext je_fM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (∑ j_1, ↑M j j_1 * (basis i).val j_1) • basis j = ↑M j i • 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 j i := byM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis i))) j = ↑M j i
  fin_cases j«0»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨0, ⋯⟩) = ↑M ((fun i => i) ⟨0, ⋯⟩) i«1»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨1, ⋯⟩) = ↑M ((fun i => i) ⟨1, ⋯⟩) i <;>«0»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨0, ⋯⟩) = ↑M ((fun i => i) ⟨0, ⋯⟩) i«1»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨1, ⋯⟩) = ↑M ((fun i => i) ⟨1, ⋯⟩) i simp [rep_apply_basis]All goals completed! 🐙