Pauli matrices and the basis of complex Lorentz tensors #
Expanding pauliContr in a basis. #
theorem
PauliMatrix.pauliContr_in_basis :
(TensorTree.tensorNode pauliContr).tensor = (((((((complexLorentzTensor.basisVector
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 0
| 1 => 0
| 2 => 0) + complexLorentzTensor.basisVector
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 0
| 1 => 1
| 2 => 1) + complexLorentzTensor.basisVector
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 1
| 1 => 0
| 2 => 1) + complexLorentzTensor.basisVector
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 1
| 1 => 1
| 2 => 0) - Complex.I • complexLorentzTensor.basisVector
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 2
| 1 => 0
| 2 => 1) + Complex.I • complexLorentzTensor.basisVector
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 2
| 1 => 1
| 2 => 0) + complexLorentzTensor.basisVector
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 3
| 1 => 0
| 2 => 0) - complexLorentzTensor.basisVector
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 3
| 1 => 1
| 2 => 1
The expansion of the Pauli matrices σ^μ^a^{dot a} in terms of basis vectors.
theorem
PauliMatrix.pauliContr_tensorBasis :
pauliContr = ((((((((complexLorentzTensor.tensorBasis
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 0
| 1 => 0
| 2 => 0) + (complexLorentzTensor.tensorBasis
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 0
| 1 => 1
| 2 => 1) + (complexLorentzTensor.tensorBasis
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 1
| 1 => 0
| 2 => 1) + (complexLorentzTensor.tensorBasis
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 1
| 1 => 1
| 2 => 0) - Complex.I • (complexLorentzTensor.tensorBasis
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 2
| 1 => 0
| 2 => 1) + Complex.I • (complexLorentzTensor.tensorBasis
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 2
| 1 => 1
| 2 => 0) + (complexLorentzTensor.tensorBasis
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 3
| 1 => 0
| 2 => 0) - (complexLorentzTensor.tensorBasis
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])
fun (x : Fin (Nat.succ 0).succ.succ) =>
match x with
| 0 => 3
| 1 => 1
| 2 => 1
Expanding pauliCo in a basis. #
The map to color one gets when lowering the indices of pauli matrices.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ofRat for pauli matrices. #
theorem
PauliMatrix.pauliContr_ofRat :
pauliContr = complexLorentzTensor.ofRat
fun
(b :
(j : Fin 3) →
Fin
(complexLorentzTensor.repDim
(![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] j))) =>
if b = fun (x : Fin 3) =>
match x with
| 0 => 0
| 1 => 0
| 2 => 0 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 0
| 1 => 1
| 2 => 1 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 1
| 1 => 0
| 2 => 1 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 1
| 1 => 1
| 2 => 0 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 2
| 1 => 0
| 2 => 1 then
{ fst := 0, snd := -1 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 2
| 1 => 1
| 2 => 0 then
{ fst := 0, snd := 1 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 3
| 1 => 0
| 2 => 0 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 3
| 1 => 1
| 2 => 1 then
{ fst := -1, snd := 0 }
else 0
theorem
PauliMatrix.pauliCo_ofRat :
pauliCo = complexLorentzTensor.ofRat
fun
(b :
(j : Fin 3) →
Fin
(complexLorentzTensor.repDim
(((Sum.elim ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.down]
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1)
j))) =>
if b = fun (x : Fin 3) =>
match x with
| 0 => 0
| 1 => 0
| 2 => 0 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 0
| 1 => 1
| 2 => 1 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 1
| 1 => 0
| 2 => 1 then
{ fst := -1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 1
| 1 => 1
| 2 => 0 then
{ fst := -1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 2
| 1 => 0
| 2 => 1 then
{ fst := 0, snd := 1 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 2
| 1 => 1
| 2 => 0 then
{ fst := 0, snd := -1 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 3
| 1 => 0
| 2 => 0 then
{ fst := -1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 3
| 1 => 1
| 2 => 1 then
{ fst := 1, snd := 0 }
else { fst := 0, snd := 0 }
theorem
PauliMatrix.pauliCoDown_ofRat :
pauliCoDown = complexLorentzTensor.ofRat
fun
(b :
(j : Fin 3) →
Fin
(complexLorentzTensor.repDim
(((Sum.elim
((Sum.elim
((Sum.elim ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.down]
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1)
![complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 2 ∘ Fin.succAbove 2)
![complexLorentzTensor.Color.downL, complexLorentzTensor.Color.downL] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 2)
j))) =>
if b = fun (x : Fin 3) =>
match x with
| 0 => 0
| 1 => 1
| 2 => 1 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 0
| 1 => 0
| 2 => 0 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 1
| 1 => 0
| 2 => 1 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 1
| 1 => 1
| 2 => 0 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 2
| 1 => 0
| 2 => 1 then
{ fst := 0, snd := -1 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 2
| 1 => 1
| 2 => 0 then
{ fst := 0, snd := 1 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 3
| 1 => 1
| 2 => 1 then
{ fst := -1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 3
| 1 => 0
| 2 => 0 then
{ fst := 1, snd := 0 }
else { fst := 0, snd := 0 }
theorem
PauliMatrix.pauliContrDown_ofRat :
pauliContrDown = complexLorentzTensor.ofRat
fun
(b :
(j : Fin 3) →
Fin
(complexLorentzTensor.repDim
(((Sum.elim
((Sum.elim
![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]
![complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 2 ∘ Fin.succAbove 2)
![complexLorentzTensor.Color.downL, complexLorentzTensor.Color.downL] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 2)
j))) =>
if b = fun (x : Fin 3) =>
match x with
| 0 => 0
| 1 => 1
| 2 => 1 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 0
| 1 => 0
| 2 => 0 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 1
| 1 => 0
| 2 => 1 then
{ fst := -1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 1
| 1 => 1
| 2 => 0 then
{ fst := -1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 2
| 1 => 0
| 2 => 1 then
{ fst := 0, snd := 1 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 2
| 1 => 1
| 2 => 0 then
{ fst := 0, snd := -1 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 3
| 1 => 1
| 2 => 1 then
{ fst := 1, snd := 0 }
else if b = fun (x : Fin 3) =>
match x with
| 0 => 3
| 1 => 0
| 2 => 0 then
{ fst := -1, snd := 0 }
else 0