DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Results for bispinors

Browse source
This commit is contained in:
jstoobysmith 2024-10-31 14:42:10 +00:00
parent d5fe9c0db6
commit 933d34bd54
1 changed files with 7 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

19
HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
View file

@ -45,17 +45,14 @@ def contrBispinorUp (p : complexContr) :=
/-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/
def contrBispinorDown (p : complexContr) :=
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
contrBispinorUp p | α β}ᵀ.tensor
{εL' | α α' ⊗ εR' | β β' ⊗ contrBispinorUp p | α β}ᵀ.tensor
/-- A bispinor `pᵃᵃ` created from a lorentz vector `p_μ`. -/
def coBispinorUp (p : complexCo) :=
{pauliContr | μ α β ⊗ p | μ}ᵀ.tensor
def coBispinorUp (p : complexCo) := {pauliContr | μ α β ⊗ p | μ}ᵀ.tensor
/-- A bispinor `pₐₐ` created from a lorentz vector `p_μ`. -/
def coBispinorDown (p : complexCo) :=
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
coBispinorUp p | α β}ᵀ.tensor
{εL' | α α' ⊗ εR' | β β' ⊗ coBispinorUp p | α β}ᵀ.tensor
/-!
@ -71,8 +68,7 @@ lemma tensorNode_contrBispinorUp (p : complexContr) :
/-- The definitional tensor node relation for `contrBispinorDown`. -/
lemma tensorNode_contrBispinorDown (p : complexContr) :
{contrBispinorDown p | α β}ᵀ.tensor =
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β'
⊗ contrBispinorUp p | α β}ᵀ.tensor := by
{εL' | α α' ⊗ εR' | β β' ⊗ contrBispinorUp p | α β}ᵀ.tensor := by
rw [contrBispinorDown, tensorNode_tensor]
/-- The definitional tensor node relation for `coBispinorUp`. -/
@ -83,8 +79,7 @@ lemma tensorNode_coBispinorUp (p : complexCo) :
/-- The definitional tensor node relation for `coBispinorDown`. -/
lemma tensorNode_coBispinorDown (p : complexCo) :
{coBispinorDown p | α β}ᵀ.tensor =
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β'
⊗ coBispinorUp p | α β}ᵀ.tensor := by
{εL' | α α' ⊗ εR' | β β' ⊗ coBispinorUp p | α β}ᵀ.tensor := by
rw [coBispinorDown, tensorNode_tensor]
/-!
@ -95,14 +90,14 @@ lemma tensorNode_coBispinorDown (p : complexCo) :
lemma contrBispinorDown_expand (p : complexContr) :
{contrBispinorDown p | α β}ᵀ.tensor =
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
{εL' | α α' ⊗ εR' | β β' ⊗
(pauliCo | μ α β ⊗ p | μ)}ᵀ.tensor := by
rw [tensorNode_contrBispinorDown p]
rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_contrBispinorUp p]
lemma coBispinorDown_expand (p : complexCo) :
{coBispinorDown p | α β}ᵀ.tensor =
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
{εL' | α α' ⊗ εR' | β β' ⊗
(pauliContr | μ α β ⊗ p | μ)}ᵀ.tensor := by
rw [tensorNode_coBispinorDown p]
rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_coBispinorUp p]