HepLean.Lorentz.PauliMatrices.AsTensor

Pauli matrices #

↑(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)

Instances For

source

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 .

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

Instances For

source

theorem PauliMatrix.asConsTensor_apply_one :

PauliMatrix.asConsTensor.hom 1 = PauliMatrix.asTensor

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