Physlib.Relativity.Fermions.Weyl.DualRightHanded

Physlib
Relativity
Fermions
Weyl
DualRightHanded

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 right handed Weyl fermions

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

@[expose] public section

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

The underlying value in Fin 2 → ℂ.

structure DualRightHandedWeyl where val : Fin 2 → ℂ

Underlying module structure

The equivalence between DualRightHandedWeyl and Fin 2 → ℂ.

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

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

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

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

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

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

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

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

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

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

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

Basis

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

def basis : Basis (Fin 2) ℂ DualRightHandedWeyl := Basis.ofEquivFun
  (Equiv.linearEquiv ℂ DualRightHandedWeyl.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 (ψ : DualRightHandedWeyl) : ψ = ∑ i, ψ.1 i • basis i := byψ:DualRightHandedWeyl⊢ ψ = ∑ i, ψ.val i • basis i
  conv_lhs => rw [← basis.sum_repr ψ]ψ:DualRightHandedWeyl| ∑ 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 this corresponds to a Weyl fermion with index ψ_{dot a}.


def rep : Representation ℂ SL(2,ℂ) DualRightHandedWeyl where
  toFun := fun M => {
    toFun := fun (ψ : DualRightHandedWeyl) =>
      DualRightHandedWeyl.toFin2ℂEquiv.symm ((M.1⁻¹).conjTranspose *ᵥ ψ.toFin2ℂ),
    map_add' := byM:SL(2, ℂ)⊢ ∀ (x y : DualRightHandedWeyl),
  toFin2ℂEquiv.symm ((↑M)⁻¹ᴴ *ᵥ (x + y).toFin2ℂ) =
    toFin2ℂEquiv.symm ((↑M)⁻¹ᴴ *ᵥ x.toFin2ℂ) + toFin2ℂEquiv.symm ((↑M)⁻¹ᴴ *ᵥ y.toFin2ℂ)
      intro ψ ψ'M:SL(2, ℂ)ψ:DualRightHandedWeylψ':DualRightHandedWeyl⊢ 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 : DualRightHandedWeyl),
  toFin2ℂEquiv.symm ((↑M)⁻¹ᴴ *ᵥ (m • x).toFin2ℂ) = (RingHom.id ℂ) m • toFin2ℂEquiv.symm ((↑M)⁻¹ᴴ *ᵥ x.toFin2ℂ)
      intro r ψM:SL(2, ℂ)r:ℂψ:DualRightHandedWeyl⊢ 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:DualRightHandedWeyl⊢ { 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:DualRightHandedWeyl⊢ { 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:DualRightHandedWeyl⊢ (↑M * ↑N)⁻¹ᴴ *ᵥ x.toFin2ℂ = ((↑M)⁻¹ᴴ * (↑N)⁻¹ᴴ) *ᵥ x.toFin2ℂ
    refine (congrFun (congrArg _ ?_) _)M:SL(2, ℂ)N:SL(2, ℂ)x:DualRightHandedWeyl⊢ (↑M * ↑N)⁻¹ᴴ = (↑M)⁻¹ᴴ * (↑N)⁻¹ᴴ
    rw [Matrix.mul_inv_revM:SL(2, ℂ)N:SL(2, ℂ)x:DualRightHandedWeyl⊢ ((↑N)⁻¹ * (↑M)⁻¹)ᴴ = (↑M)⁻¹ᴴ * (↑N)⁻¹ᴴM:SL(2, ℂ)N:SL(2, ℂ)x:DualRightHandedWeyl⊢ ((↑N)⁻¹ * (↑M)⁻¹)ᴴ = (↑M)⁻¹ᴴ * (↑N)⁻¹ᴴ]M:SL(2, ℂ)N:SL(2, ℂ)x:DualRightHandedWeyl⊢ ((↑N)⁻¹ * (↑M)⁻¹)ᴴ = (↑M)⁻¹ᴴ * (↑N)⁻¹ᴴ
    exact conjTranspose_mul _ _All goals completed! 🐙

              lemma rep_apply (M : SL(2,ℂ)) (ψ : DualRightHandedWeyl) :
    rep M ψ = ⟨(M.1⁻¹).conjTranspose *ᵥ ψ.1⟩ := rfl

lemma rep_apply_eq_sum_basis (M : SL(2,ℂ)) (ψ : DualRightHandedWeyl) :
    rep M ψ = ∑ i, (∑ j, (M.1⁻¹).conjTranspose i j * ψ.1 j) • basis i := byM:SL(2, ℂ)ψ:DualRightHandedWeyl⊢ (rep M) ψ = ∑ i, (∑ j, (↑M)⁻¹ᴴ i j * ψ.val j) • basis i
  rw [eq_sum_basis (rep M ψ)M:SL(2, ℂ)ψ:DualRightHandedWeyl⊢ ∑ i, ((rep M) ψ).val i • basis i = ∑ i, (∑ j, (↑M)⁻¹ᴴ i j * ψ.val j) • basis iM:SL(2, ℂ)ψ:DualRightHandedWeyl⊢ ∑ i, ((rep M) ψ).val i • basis i = ∑ i, (∑ j, (↑M)⁻¹ᴴ i j * ψ.val j) • basis i]M:SL(2, ℂ)ψ:DualRightHandedWeyl⊢ ∑ 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⁻¹).conjTranspose 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⁻¹).conjTranspose := 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⁻¹).conjTranspose *ᵥ (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 = star (M.1⁻¹ i j) := byM:SL(2, ℂ)i:Fin 2j:Fin 2⊢ (basis.repr ((rep M) (basis i))) j = star ((↑M)⁻¹ i j)
  fin_cases j«0»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨0, ⋯⟩) = star ((↑M)⁻¹ i ((fun i => i) ⟨0, ⋯⟩))«1»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨1, ⋯⟩) = star ((↑M)⁻¹ i ((fun i => i) ⟨1, ⋯⟩)) <;>«0»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨0, ⋯⟩) = star ((↑M)⁻¹ i ((fun i => i) ⟨0, ⋯⟩))«1»M:SL(2, ℂ)i:Fin 2⊢ (basis.repr ((rep M) (basis i))) ((fun i => i) ⟨1, ⋯⟩) = star ((↑M)⁻¹ i ((fun i => i) ⟨1, ⋯⟩)) simp [rep_apply_basis]All goals completed! 🐙