Imports
/-
Copyright (c) 2024 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 Physlib.Relativity.Fermions.Weyl.LeftHanded
public import Physlib.Relativity.Fermions.Weyl.RightHanded
public import Physlib.Relativity.Fermions.Weyl.DualLeftHanded
public import Physlib.Relativity.Fermions.Weyl.DualRightHandedDirac fermions
In this file we define Dirac fermions. This corresponds to a combination of two Weyl fermions (ψ^α, χ_{dot α}) That is a LeftHandedWeyl and a DualRightHandedWeyl.
References
arXiv:0812.1594 page 197.
@[expose] public sectionA Dirac fermion, consisting of a left handed Weyl fermion and a dual right handed Weyl fermion.
The left handed component of the Dirac fermion.
The right handed component of the Dirac fermion.
The underlying module structure
We inherit the module structure on dirac fermions from the module structure on left handed and dual right handed Weyl fermions.
The decomposition of a Dirac fermion into its left handed and dual right handed components.
def decomposeEquiv : Dirac ≃ LeftHandedWeyl × DualRightHandedWeyl where
toFun d := (d.left, d.dualRight)
invFun p := ⟨p.1, p.2⟩
left_inv _ := rfl
right_inv _ := rflinstance : AddCommGroup Dirac := Equiv.addCommGroup decomposeEquivinstance : Module ℂ Dirac := Equiv.module ℂ decomposeEquiv@[simp]
lemma left_add (d₁ d₂ : Dirac) : (d₁ + d₂).left = d₁.left + d₂.left := rfl@[simp]
lemma dualRight_add (d₁ d₂ : Dirac) : (d₁ + d₂).dualRight = d₁.dualRight + d₂.dualRight := rfl@[simp]
lemma left_smul (c : ℂ) (d : Dirac) : (c • d).left = c • d.left := rfl@[simp]
lemma dualRight_smul (c : ℂ) (d : Dirac) : (c • d).dualRight = c • d.dualRight := rfl
The linear equivalence between Dirac and LeftHandedWeyl × DualRightHandedWeyl.
def decomposeLinEquiv : Dirac ≃ₗ[ℂ] LeftHandedWeyl × DualRightHandedWeyl where
toEquiv := decomposeEquiv
map_add' := ⊢ ∀ (x y : Dirac), decomposeEquiv.toFun (x + y) = decomposeEquiv.toFun x + decomposeEquiv.toFun y x✝:Diracy✝:Dirac⊢ decomposeEquiv.toFun (x✝ + y✝) = decomposeEquiv.toFun x✝ + decomposeEquiv.toFun y✝; All goals completed! 🐙
map_smul' := ⊢ ∀ (m : ℂ) (x : Dirac), decomposeEquiv.toFun (m • x) = (RingHom.id ℂ) m • decomposeEquiv.toFun x m✝:ℂx✝:Dirac⊢ decomposeEquiv.toFun (m✝ • x✝) = (RingHom.id ℂ) m✝ • decomposeEquiv.toFun x✝; All goals completed! 🐙The chiral basis
The chiral basis of the Dirac fermions.
def chiralBasis : Basis (Fin 4) ℂ Dirac :=
((LeftHandedWeyl.basis.prod DualRightHandedWeyl.basis).reindex finSumFinEquiv).map
decomposeLinEquiv.symmlemma chiralBasis_cast_add (i : Fin 2) : chiralBasis (Fin.castAdd 2 i) =
⟨LeftHandedWeyl.basis i, 0⟩ := i:Fin 2⊢ chiralBasis (Fin.castAdd 2 i) = { left := LeftHandedWeyl.basis i, dualRight := 0 }
⊢ chiralBasis (Fin.castAdd 2 ((fun i => i) ⟨0, ⋯⟩)) =
{ left := LeftHandedWeyl.basis ((fun i => i) ⟨0, ⋯⟩), dualRight := 0 }⊢ chiralBasis (Fin.castAdd 2 ((fun i => i) ⟨1, ⋯⟩)) =
{ left := LeftHandedWeyl.basis ((fun i => i) ⟨1, ⋯⟩), dualRight := 0 }
all_goals
⊢ decomposeLinEquiv.symm
(((fun x => (x, 0)) ∘ ⇑LeftHandedWeyl.basis ⊕ᵥ Prod.mk 0 ∘ ⇑DualRightHandedWeyl.basis)
(finSumFinEquiv.symm (Fin.castAdd 2 ⟨1, ⋯⟩))) =
{ left := LeftHandedWeyl.basis ⟨1, ⋯⟩, dualRight := 0 }
All goals completed! 🐙lemma chiralBasis_nat_add (i : Fin 2) : chiralBasis (Fin.natAdd 2 i) =
⟨0, DualRightHandedWeyl.basis i⟩ := i:Fin 2⊢ chiralBasis (Fin.natAdd 2 i) = { left := 0, dualRight := DualRightHandedWeyl.basis i }
⊢ chiralBasis (Fin.natAdd 2 ((fun i => i) ⟨0, ⋯⟩)) =
{ left := 0, dualRight := DualRightHandedWeyl.basis ((fun i => i) ⟨0, ⋯⟩) }⊢ chiralBasis (Fin.natAdd 2 ((fun i => i) ⟨1, ⋯⟩)) =
{ left := 0, dualRight := DualRightHandedWeyl.basis ((fun i => i) ⟨1, ⋯⟩) }
all_goals
⊢ decomposeLinEquiv.symm
(((fun x => (x, 0)) ∘ ⇑LeftHandedWeyl.basis ⊕ᵥ Prod.mk 0 ∘ ⇑DualRightHandedWeyl.basis)
(finSumFinEquiv.symm (Fin.natAdd 2 ⟨1, ⋯⟩))) =
{ left := 0, dualRight := DualRightHandedWeyl.basis ⟨1, ⋯⟩ }
All goals completed! 🐙The representation of the Lorentz group
The representation of SL(2, ℂ) on Dirac fermions.
def rep : Representation ℂ SL(2,ℂ) Dirac where
toFun g := decomposeLinEquiv.symm ∘ₗ
(((LeftHandedWeyl.rep).prod (DualRightHandedWeyl.rep)) g) ∘ₗ
decomposeLinEquiv
map_one' := ⊢ ↑decomposeLinEquiv.symm ∘ₗ (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) 1 ∘ₗ ↑decomposeLinEquiv = 1
i:Dirac⊢ (↑decomposeLinEquiv.symm ∘ₗ (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) 1 ∘ₗ ↑decomposeLinEquiv) i = 1 i
All goals completed! 🐙
map_mul' := fun M N => M:SL(2, ℂ)N:SL(2, ℂ)⊢ ↑decomposeLinEquiv.symm ∘ₗ (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) (M * N) ∘ₗ ↑decomposeLinEquiv =
↑decomposeLinEquiv.symm ∘ₗ (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) M ∘ₗ ↑decomposeLinEquiv *
↑decomposeLinEquiv.symm ∘ₗ (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) N ∘ₗ ↑decomposeLinEquiv
M:SL(2, ℂ)N:SL(2, ℂ)x:Dirac⊢ (↑decomposeLinEquiv.symm ∘ₗ (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) (M * N) ∘ₗ ↑decomposeLinEquiv) x =
(↑decomposeLinEquiv.symm ∘ₗ (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) M ∘ₗ ↑decomposeLinEquiv *
↑decomposeLinEquiv.symm ∘ₗ (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) N ∘ₗ ↑decomposeLinEquiv)
x
All goals completed! 🐙lemma rep_apply_mk (g : SL(2,ℂ)) (ψ : LeftHandedWeyl) (χ : DualRightHandedWeyl) :
rep g ⟨ψ, χ⟩ = ⟨LeftHandedWeyl.rep g ψ, DualRightHandedWeyl.rep g χ⟩ := rfl
The equivalence between the representation on Dirac and the representation
on LeftHandedWeyl × DualRightHandedWeyl.
def decomposeRepEquiv : rep.Equiv ((LeftHandedWeyl.rep).prod (DualRightHandedWeyl.rep)) where
toLinearEquiv := decomposeLinEquiv
isIntertwining' g := g:SL(2, ℂ)⊢ ↑decomposeLinEquiv ∘ₗ rep g = (LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) g ∘ₗ ↑decomposeLinEquiv
g:SL(2, ℂ)x:Dirac⊢ (↑decomposeLinEquiv ∘ₗ rep g) x = ((LeftHandedWeyl.rep.prod DualRightHandedWeyl.rep) g ∘ₗ ↑decomposeLinEquiv) x
g:SL(2, ℂ)x:Dirac⊢ decomposeLinEquiv ((rep g) x) =
((LeftHandedWeyl.rep g) (decomposeLinEquiv x).1, (DualRightHandedWeyl.rep g) (decomposeLinEquiv x).2)
All goals completed! 🐙