1. Physlib
  2. Relativity
  3. PauliMatrices
  4. AsTensor
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Relativity.Fermions.Weyl.Two public import Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic

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.

@[expose] public section

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

def asTensor : (ContrℂModule ⊗[ℂ] (LeftHandedWeyl ⊗[ℂ] RightHandedWeyl)) := ∑ i, complexContrBasis i ⊗ₜ leftRightToMatrix.symm (pauliBasis i)

The expansion of asTensor into complexContrBasis basis vectors .

lemma asTensor_expand_complexContrBasis : asTensor = complexContrBasis (Sum.inl 0) ⊗ₜ leftRightToMatrix.symm (pauliBasis (Sum.inl 0)) + complexContrBasis (Sum.inr 0) ⊗ₜ leftRightToMatrix.symm (pauliBasis (Sum.inr 0)) + complexContrBasis (Sum.inr 1) ⊗ₜ leftRightToMatrix.symm (pauliBasis (Sum.inr 1)) + complexContrBasis (Sum.inr 2) ⊗ₜ leftRightToMatrix.symm (pauliBasis (Sum.inr 2)) := ⊢ asTensor = complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis (Sum.inl 0)) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis (Sum.inr 0)) + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis (Sum.inr 1)) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis (Sum.inr 2)) All goals completed! 🐙

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

⊢ ∑ i, ∑ j, ↑(pauliBasis (Sum.inl 0)) i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j = LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 All goals completed! 🐙

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

⊢ ∑ i, ∑ j, ↑(pauliBasis (Sum.inr 0)) i j • LeftHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j = LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 All goals completed! 🐙

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

lemma leftRightToMatrix_σSA_inr_1_expand : leftRightToMatrix.symm (pauliBasis (Sum.inr 1)) = -(I • LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + I • LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 := ⊢ leftRightToMatrix.symm ↑(pauliBasis (Sum.inr 1)) = -(I • LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + I • LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 ⊢ -I • LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 = -(I • LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) All goals completed! 🐙

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

set_option backward.isDefEq.respectTransparency false inlemma leftRightToMatrix_σSA_inr_2_expand : leftRightToMatrix.symm (pauliBasis (Sum.inr 2)) = LeftHandedWeyl.basis 0 ⊗ₜ RightHandedWeyl.basis 0 - LeftHandedWeyl.basis 1 ⊗ₜ RightHandedWeyl.basis 1 := ⊢ leftRightToMatrix.symm ↑(pauliBasis (Sum.inr 2)) = LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 - LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 ⊢ LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 + -1 • LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 = LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 - LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 All goals completed! 🐙

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

⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 + LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] (-(I • LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + I • LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 - LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) = complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) + complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) - I • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + I • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) ⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) + complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0)) + (-(I • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1)) + I • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0)) + (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1)) = complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) + complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) - I • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) + I • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) All goals completed! 🐙

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.

set_option backward.isDefEq.respectTransparency false inM:SL(2, ℂ)x:ℂi:Fin 1 ⊕ Fin 3x✝:i ∈ Finset.univ⊢ 1 i i • complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis i) = complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis i)M:SL(2, ℂ)x:ℂi:Fin 1 ⊕ Fin 3x✝¹:i ∈ Finset.univb:Fin 1 ⊕ Fin 3x✝:b ∈ Finset.univhb:b ≠ i⊢ 1 i b • complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis b) = 0M:SL(2, ℂ)x:ℂi:Fin 1 ⊕ Fin 3x✝:i ∈ Finset.univhb:i ∉ Finset.univ⊢ 1 i i • complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis i) = 0 M:SL(2, ℂ)x:ℂi:Fin 1 ⊕ Fin 3x✝:i ∈ Finset.univ⊢ 1 i i • complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis i) = complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis i) All goals completed! 🐙 M:SL(2, ℂ)x:ℂi:Fin 1 ⊕ Fin 3x✝¹:i ∈ Finset.univb:Fin 1 ⊕ Fin 3x✝:b ∈ Finset.univhb:b ≠ i⊢ 1 i b • complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis b) = 0 M:SL(2, ℂ)x:ℂi:Fin 1 ⊕ Fin 3x✝¹:i ∈ Finset.univb:Fin 1 ⊕ Fin 3x✝:b ∈ Finset.univhb:b ≠ i⊢ 0 • complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis b) = 0 All goals completed! 🐙 M:SL(2, ℂ)x:ℂi:Fin 1 ⊕ Fin 3x✝:i ∈ Finset.univhb:i ∉ Finset.univ⊢ 1 i i • complexContrBasis i ⊗ₜ[ℂ] leftRightToMatrix.symm ↑(pauliBasis i) = 0 All goals completed! 🐙

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

lemma asConsTensor_apply_one : asConsTensor (1 : ℂ) = asTensor := ⊢ asConsTensor 1 = asTensor ⊢ 1 • asTensor = asTensor All goals completed! 🐙