Pauli matrices

def PauliMatrix.asTensor : ↑(CategoryTheory.MonoidalCategory.tensorObj Lorentz.complexContr (CategoryTheory.MonoidalCategory.tensorObj Fermion.leftHanded Fermion.rightHanded)).V

The tensor σ^μ^a^{dot a} based on the Pauli-matrices as an element of complexContr ⊗ leftHanded ⊗ rightHanded.

Equations

• PauliMatrix.asTensor = ∑ i : Fin 1 ⊕ Fin 3, Lorentz.complexContrBasis i ⊗ₜ[ℂ] Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA i)

theorem PauliMatrix.asTensor_expand_complexContrBasis : PauliMatrix.asTensor = Lorentz.complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA (Sum.inl 0)) + Lorentz.complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA (Sum.inr 0)) + Lorentz.complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA (Sum.inr 1)) + Lorentz.complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA (Sum.inr 2))

The expansion of asTensor into complexContrBasis basis vectors .

theorem PauliMatrix.leftRightToMatrix_σSA_inl_0_expand : Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA (Sum.inl 0)) = Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 0 + Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 1

The expansion of the pauli matrix σ₀ in terms of a basis of tensor product vectors.

theorem PauliMatrix.leftRightToMatrix_σSA_inr_0_expand : Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA (Sum.inr 0)) = Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 1 + Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 0

The expansion of the pauli matrix σ₁ in terms of a basis of tensor product vectors.

theorem PauliMatrix.leftRightToMatrix_σSA_inr_1_expand : Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA (Sum.inr 1)) = -(Complex.I • Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 1) + Complex.I • Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 0

The expansion of the pauli matrix σ₂ in terms of a basis of tensor product vectors.

theorem PauliMatrix.leftRightToMatrix_σSA_inr_2_expand : Fermion.leftRightToMatrix.symm ↑(PauliMatrix.σSA (Sum.inr 2)) = Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 0 - Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 1

The expansion of the pauli matrix σ₃ in terms of a basis of tensor product vectors.

theorem PauliMatrix.asTensor_expand : PauliMatrix.asTensor = Lorentz.complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 0 + Lorentz.complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 1 + Lorentz.complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 1 + Lorentz.complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 0 - Complex.I • Lorentz.complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 1 + Complex.I • Lorentz.complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 0 + Lorentz.complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] Fermion.leftBasis 0 ⊗ₜ[ℂ] Fermion.rightBasis 0 - Lorentz.complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] Fermion.leftBasis 1 ⊗ₜ[ℂ] Fermion.rightBasis 1

The expansion of asTensor into complexContrBasis basis of tensor product vectors.

def PauliMatrix.asConsTensor : 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategory.tensorObj Lorentz.complexContr (CategoryTheory.MonoidalCategory.tensorObj Fermion.leftHanded Fermion.rightHanded)

The tensor σ^μ^a^{dot a} based on the Pauli-matrices as a morphism, 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ rightHanded manifesting the invariance under the SL(2,ℂ) action.

Equations

• One or more equations did not get rendered due to their size.

theorem PauliMatrix.asConsTensor_apply_one : PauliMatrix.asConsTensor.hom 1 = PauliMatrix.asTensor