Contraction of indices of Pauli matrix. #
The main result of this file is pauliMatrix_contract_pauliMatrix which states that
η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}.
The current way this result is proved is by using tensor tree manipulations. There is likely a more direct path to this result.
The statement that σᵥᵃᵇ σᵛᵃ'ᵇ' = 2 εᵃᵃ' εᵇᵇ'.
theorem
PauliMatrix.pauliCoDown_trace_pauliCo :
(TensorSpecies.Tensor.contrT 2 1 3 ⋯)
((TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT pauliCoDown) pauliCo)) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) (2 • complexLorentzTensor.coMetric)
theorem
PauliMatrix.pauliCo_trace_pauliCoDown :
(TensorSpecies.Tensor.contrT 2 1 3 ⋯)
((TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT pauliCo) pauliCoDown)) = (TensorSpecies.Tensor.permT ![0, 1] ⋯) (2 • complexLorentzTensor.coMetric)
theorem
PauliMatrix.pauliContr_mul_pauliContrDown_add :
(TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT pauliContr) pauliContrDown) + (TensorSpecies.Tensor.permT ![2, 1, 0, 3] ⋯)
((TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT pauliContr) pauliContrDown)) = (TensorSpecies.Tensor.permT ![0, 2, 1, 3] ⋯)
(2 • (TensorSpecies.Tensor.prodT complexLorentzTensor.contrMetric) complexLorentzTensor.leftAltLeftUnit)
theorem
PauliMatrix.auliContrDown_pauliContr_mul_add :
(TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT pauliContrDown) pauliContr) + (TensorSpecies.Tensor.permT ![2, 1, 0, 3] ⋯)
((TensorSpecies.Tensor.contrT 4 2 4 ⋯) ((TensorSpecies.Tensor.prodT pauliContrDown) pauliContr)) = (TensorSpecies.Tensor.permT ![0, 2, 1, 3] ⋯)
(2 • (TensorSpecies.Tensor.prodT complexLorentzTensor.contrMetric) complexLorentzTensor.altRightRightUnit)