Pauli matrices as a tensor

The results in this file are primarily used to show that the pauli matrices in invariant under the SL(2,ℂ) action.

def PauliMatrix.asTensor : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj Lorentz.complexContr (CategoryTheory.MonoidalCategoryStruct.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.pauliBasis i)

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

The expansion of asTensor into complexContrBasis basis vectors .

theorem PauliMatrix.leftRightToMatrix_σSA_inl_0_expand : Fermion.leftRightToMatrix.symm ↑(pauliBasis (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 ↑(pauliBasis (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 ↑(pauliBasis (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 ↑(pauliBasis (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 : 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 : CategoryTheory.MonoidalCategoryStruct.tensorUnit (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Lorentz.complexContr (CategoryTheory.MonoidalCategoryStruct.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 : (CategoryTheory.ConcreteCategory.hom asConsTensor.hom) 1 = asTensor

The map 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ rightHanded corresponding to Pauli matrices, when evaluated on 1 corresponds to the tensor PauliMatrix.asTensor.