refactor: Pauli matrices
This commit is contained in:
jstoobysmith
parent
e761463e8f
commit
83ff8f5358
2 changed files with 60 additions and 141 deletions
|
|
@ -3,8 +3,13 @@ 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
|
||||
-/
|
||||
import HepLean.Tensors.ComplexLorentz.PauliLower
|
||||
import HepLean.Tensors.ComplexLorentz.PauliMatrices.Basic
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermProd
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
|
||||
import HepLean.Tensors.Tree.NodeIdentities.Congr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
|
||||
/-!
|
||||
|
|
@ -28,145 +33,59 @@ noncomputable section
|
|||
namespace complexLorentzTensor
|
||||
open Lorentz
|
||||
|
||||
/-!
|
||||
|
||||
## Definitions
|
||||
|
||||
-/
|
||||
|
||||
/-- A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`. -/
|
||||
def contrBispinorUp (p : complexContr) :=
|
||||
{p | μ ⊗ pauliCo | μ α β}ᵀ.tensor
|
||||
|
||||
lemma tensorNode_contrBispinorUp (p : complexContr) :
|
||||
(tensorNode (contrBispinorUp p)).tensor = {p | μ ⊗ pauliCo | μ α β}ᵀ.tensor := by
|
||||
rw [contrBispinorUp, tensorNode_tensor]
|
||||
|
||||
/-- An up-bispinor is equal to `pauliCo | μ α β ⊗ p | μ`-/
|
||||
lemma contrBispinorUp_eq_pauliCo_self (p : complexContr) :
|
||||
{contrBispinorUp p | α β = pauliCo | μ α β ⊗ p | μ}ᵀ := by
|
||||
rw [tensorNode_contrBispinorUp]
|
||||
conv_lhs =>
|
||||
rw [contr_tensor_eq <| prod_comm _ _ _ _]
|
||||
rw [perm_contr]
|
||||
rw [perm_tensor_eq <| contr_swap _ _]
|
||||
rw [perm_perm]
|
||||
apply perm_congr
|
||||
· apply OverColor.Hom.ext
|
||||
ext x
|
||||
match x with
|
||||
| (0 : Fin 2) => rfl
|
||||
| (1 : Fin 2) => rfl
|
||||
· rfl
|
||||
|
||||
set_option maxRecDepth 2000 in
|
||||
lemma altRightMetric_contr_contrBispinorUp_assoc (p : complexContr) :
|
||||
{Fermion.altRightMetric | β β' ⊗ contrBispinorUp p | α β =
|
||||
Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β ⊗ p | μ}ᵀ := by
|
||||
conv_lhs =>
|
||||
rw [contr_tensor_eq <| prod_tensor_eq_snd <| contrBispinorUp_eq_pauliCo_self _]
|
||||
rw [contr_tensor_eq <| prod_perm_right _ _ _ _]
|
||||
rw [perm_contr]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| prod_assoc _ _ _ _ _ _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
conv_rhs =>
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
erw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
rw [perm_tensor_eq <| contr_contr _ _ _]
|
||||
rw [perm_perm]
|
||||
apply perm_congr (_) rfl
|
||||
· apply OverColor.Hom.fin_ext
|
||||
intro i
|
||||
fin_cases i
|
||||
exact rfl
|
||||
exact rfl
|
||||
{pauliCo | μ α β ⊗ p | μ}ᵀ.tensor
|
||||
|
||||
/-- A bispinor `pₐₐ` created from a lorentz vector `p^μ`. -/
|
||||
def contrBispinorDown (p : complexContr) :=
|
||||
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β' ⊗
|
||||
(contrBispinorUp p) | α β}ᵀ.tensor
|
||||
contrBispinorUp p | α β}ᵀ.tensor
|
||||
|
||||
/-- Expands the tensor node of `contrBispinorDown` into a tensor tree based on
|
||||
`contrBispinorUp`. -/
|
||||
/-- A bispinor `pᵃᵃ` created from a lorentz vector `p_μ`. -/
|
||||
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
|
||||
|
||||
/-!
|
||||
|
||||
## Tensor nodes
|
||||
|
||||
-/
|
||||
|
||||
/-- The definitional tensor node relation for `contrBispinorUp`. -/
|
||||
lemma tensorNode_contrBispinorUp (p : complexContr) :
|
||||
{contrBispinorUp p | α β}ᵀ.tensor = {pauliCo | μ α β ⊗ p | μ}ᵀ.tensor := by
|
||||
rw [contrBispinorUp, tensorNode_tensor]
|
||||
|
||||
/-- The definitional tensor node relation for `contrBispinorDown`. -/
|
||||
lemma tensorNode_contrBispinorDown (p : complexContr) :
|
||||
{contrBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β' ⊗ (contrBispinorUp p) | α β}ᵀ.tensor := by
|
||||
{contrBispinorDown p | α β}ᵀ.tensor =
|
||||
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β'
|
||||
⊗ contrBispinorUp p | α β}ᵀ.tensor := by
|
||||
rw [contrBispinorDown, tensorNode_tensor]
|
||||
|
||||
set_option maxRecDepth 10000 in
|
||||
lemma contrBispinorDown_eq_metric_contr_contrBispinorUp (p : complexContr) :
|
||||
{contrBispinorDown p | α' β' = Fermion.altLeftMetric | α α' ⊗
|
||||
(Fermion.altRightMetric | β β' ⊗ contrBispinorUp p | α β)}ᵀ := by
|
||||
rw [tensorNode_contrBispinorDown]
|
||||
conv_lhs =>
|
||||
rw [contr_tensor_eq <| contr_tensor_eq <| prod_assoc' _ _ _ _ _ _]
|
||||
rw [contr_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_contr]
|
||||
rw [perm_tensor_eq <| contr_contr _ _ _]
|
||||
rw [perm_perm]
|
||||
conv_rhs =>
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _ ]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
apply perm_congr
|
||||
· apply OverColor.Hom.ext
|
||||
ext x
|
||||
match x with
|
||||
| (0 : Fin 2) => rfl
|
||||
| (1 : Fin 2) => rfl
|
||||
· rfl
|
||||
/-- The definitional tensor node relation for `coBispinorUp`. -/
|
||||
lemma tensorNode_coBispinorUp (p : complexCo) :
|
||||
{coBispinorUp p | α β}ᵀ.tensor = {pauliContr | μ α β ⊗ p | μ}ᵀ.tensor := by
|
||||
rw [coBispinorUp, tensorNode_tensor]
|
||||
|
||||
/- TODO: Remove maxHeartbeats from this result. -/
|
||||
set_option maxHeartbeats 400000 in
|
||||
set_option maxRecDepth 2000 in
|
||||
lemma contrBispinorDown_eq_contr_with_self (p : complexContr) :
|
||||
{contrBispinorDown p | α' β' = (Fermion.altLeftMetric | α α' ⊗
|
||||
(Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β)) ⊗ p | μ}ᵀ := by
|
||||
rw [contrBispinorDown_eq_metric_contr_contrBispinorUp]
|
||||
conv_lhs =>
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| altRightMetric_contr_contrBispinorUp_assoc _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_right _ _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _ ]
|
||||
rw [perm_perm]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <|
|
||||
prod_assoc _ _ _ _ _ _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
conv =>
|
||||
rhs
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| contr_prod _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
erw [perm_tensor_eq <| contr_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_tensor_eq <| perm_contr _ _]
|
||||
rw [perm_perm]
|
||||
rw [perm_tensor_eq <| contr_contr _ _ _]
|
||||
rw [perm_perm]
|
||||
apply congrArg
|
||||
apply congrFun
|
||||
apply congrArg
|
||||
apply OverColor.Hom.fin_ext
|
||||
intro i
|
||||
fin_cases i
|
||||
· exact rfl
|
||||
· exact rfl
|
||||
|
||||
/-- Expansion of a `contrBispinorDown` into the original contravariant tensor nested
|
||||
between pauli matrices and metrics. -/
|
||||
lemma contrBispinorDown_eq_metric_mul_self_mul_pauli (p : complexContr) :
|
||||
{contrBispinorDown p | α β}ᵀ.tensor = {Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β' ⊗ (p | μ ⊗ pauliCo | μ α β)}ᵀ.tensor := by
|
||||
conv =>
|
||||
lhs
|
||||
rw [tensorNode_contrBispinorDown]
|
||||
rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| tensorNode_contrBispinorUp p]
|
||||
/-- The definitional tensor node relation for `coBispinorDown`. -/
|
||||
lemma tensorNode_coBispinorDown (p : complexCo) :
|
||||
{coBispinorDown p | α β}ᵀ.tensor =
|
||||
{Fermion.altLeftMetric | α α' ⊗ Fermion.altRightMetric | β β'
|
||||
⊗ coBispinorUp p | α β}ᵀ.tensor := by
|
||||
rw [coBispinorDown, tensorNode_tensor]
|
||||
|
||||
end complexLorentzTensor
|
||||
end
|
||||
|
|
|
|||
|
|
@ -33,19 +33,19 @@ open Fermion
|
|||
|
||||
-/
|
||||
|
||||
/- The Pauli matrices as `σ^μ^α^{dot β}`. -/
|
||||
/- The Pauli matrices as the complex Lorentz tensor `σ^μ^α^{dot β}`. -/
|
||||
def pauliContr := {PauliMatrix.asConsTensor | ν α β}ᵀ.tensor
|
||||
|
||||
/-- The Pauli matrices as `σ_μ^α^{dot β}`. -/
|
||||
/-- The Pauli matrices as the complex Lorentz tensor `σ_μ^α^{dot β}`. -/
|
||||
def pauliCo := {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | ν α β}ᵀ.tensor
|
||||
|
||||
/-- The Pauli matrices as `σ_μ_α_{dot β}`. -/
|
||||
def pauliCoDown := {Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β}ᵀ.tensor
|
||||
/-- The Pauli matrices as the complex Lorentz tensor `σ_μ_α_{dot β}`. -/
|
||||
def pauliCoDown := {pauliCo | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β'}ᵀ.tensor
|
||||
|
||||
/-- The Pauli matrices as `σ^μ_α_{dot β}`. -/
|
||||
def pauliContrDown := {Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ.tensor
|
||||
/-- The Pauli matrices as the complex Lorentz tensor `σ^μ_α_{dot β}`. -/
|
||||
def pauliContrDown := {pauliContr | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β'}ᵀ.tensor
|
||||
|
||||
/-!
|
||||
|
||||
|
|
@ -65,14 +65,14 @@ lemma tensorNode_pauliCo : {pauliCo | μ α β}ᵀ.tensor =
|
|||
|
||||
/-- The definitional tensor node relation for `pauliCoDown`. -/
|
||||
lemma tensorNode_pauliCoDown : {pauliCoDown | μ α β}ᵀ.tensor =
|
||||
{Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β' ⊗ pauliCo | μ α β}ᵀ.tensor := by
|
||||
{pauliCo | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β'}ᵀ.tensor := by
|
||||
rfl
|
||||
|
||||
/-- The definitional tensor node relation for `pauliContrDown`. -/
|
||||
lemma tensorNode_pauliContrDown : {pauliContrDown | μ α β}ᵀ.tensor =
|
||||
{Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β' ⊗ pauliContr | μ α β}ᵀ.tensor := by
|
||||
{pauliContr | μ α β ⊗ Fermion.altLeftMetric | α α' ⊗
|
||||
Fermion.altRightMetric | β β'}ᵀ.tensor := by
|
||||
rfl
|
||||
|
||||
end complexLorentzTensor
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue