Pauli matrices as complex Lorentz tensors

Definitions.

def PauliMatrix.pauliContr : ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR])).V

The Pauli matrices as the complex Lorentz tensor σ^μ^α^{dot β}.

Equations

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

def PauliMatrix.«termσ^^^» : Lean.ParserDescr

The Pauli matrices as the complex Lorentz tensor σ^μ^α^{dot β}.

Equations

• PauliMatrix.«termσ^^^» = Lean.ParserDescr.node `PauliMatrix.«termσ^^^» 1024 (Lean.ParserDescr.symbol "σ^^^")

def PauliMatrix.pauliCo : ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ((Sum.elim ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.down] ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1))).V

The Pauli matrices as the complex Lorentz tensor σ_μ^α^{dot β}.

Equations

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

def PauliMatrix.«termσ_^^» : Lean.ParserDescr

The Pauli matrices as the complex Lorentz tensor σ_μ^α^{dot β}.

Equations

• PauliMatrix.«termσ_^^» = Lean.ParserDescr.node `PauliMatrix.«termσ_^^» 1024 (Lean.ParserDescr.symbol "σ_^^")

def PauliMatrix.pauliCoDown : ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ((Sum.elim ((Sum.elim ((Sum.elim ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.down] ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1) ![complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 2 ∘ Fin.succAbove 2) ![complexLorentzTensor.Color.downL, complexLorentzTensor.Color.downL] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 2))).V

The Pauli matrices as the complex Lorentz tensor σ_μ_{dot β}_α.

Equations

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

def PauliMatrix.termσ___ : Lean.ParserDescr

The Pauli matrices as the complex Lorentz tensor σ_μ_{dot β}_α.

Equations

• PauliMatrix.termσ___ = Lean.ParserDescr.node `PauliMatrix.termσ___ 1024 (Lean.ParserDescr.symbol "σ___")

def PauliMatrix.pauliContrDown : ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ((Sum.elim ((Sum.elim ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] ![complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 2 ∘ Fin.succAbove 2) ![complexLorentzTensor.Color.downL, complexLorentzTensor.Color.downL] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 2))).V

The Pauli matrices as the complex Lorentz tensor σ^μ_{dot β}_α.

Equations

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

def PauliMatrix.«termσ^__» : Lean.ParserDescr

The Pauli matrices as the complex Lorentz tensor σ^μ_{dot β}_α.

Equations

• PauliMatrix.«termσ^__» = Lean.ParserDescr.node `PauliMatrix.«termσ^__» 1024 (Lean.ParserDescr.symbol "σ^__")

Tensor nodes.

theorem PauliMatrix.tensorNode_pauliContr : (TensorTree.tensorNode pauliContr).tensor = (TensorTree.constThreeNodeE complexLorentzTensor complexLorentzTensor.Color.up complexLorentzTensor.Color.upL complexLorentzTensor.Color.upR asConsTensor).tensor

The definitional tensor node relation for pauliContr.

theorem PauliMatrix.tensorNode_pauliCo : (TensorTree.tensorNode pauliCo).tensor = (TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode complexLorentzTensor.coMetric).prod (TensorTree.tensorNode pauliContr))).tensor

The definitional tensor node relation for pauliCo.

theorem PauliMatrix.tensorNode_pauliCoDown : (TensorTree.tensorNode pauliCoDown).tensor = (TensorTree.contr 1 2 ⋯ ((TensorTree.contr 2 2 ⋯ ((TensorTree.tensorNode pauliCo).prod (TensorTree.tensorNode complexLorentzTensor.altRightMetric))).prod (TensorTree.tensorNode complexLorentzTensor.altLeftMetric))).tensor

The definitional tensor node relation for pauliCoDown.

theorem PauliMatrix.tensorNode_pauliContrDown : (TensorTree.tensorNode pauliContrDown).tensor = (TensorTree.contr 1 2 ⋯ ((TensorTree.contr 2 2 ⋯ ((TensorTree.tensorNode pauliContr).prod (TensorTree.tensorNode complexLorentzTensor.altRightMetric))).prod (TensorTree.tensorNode complexLorentzTensor.altLeftMetric))).tensor

The definitional tensor node relation for pauliContrDown.

Group actions

theorem PauliMatrix.action_pauliContr (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode pauliContr)).tensor = (TensorTree.tensorNode pauliContr).tensor

The tensor pauliContr is invariant under the action of SL(2,ℂ).

theorem PauliMatrix.action_pauliCo (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode pauliCo)).tensor = (TensorTree.tensorNode pauliCo).tensor

The tensor pauliCo is invariant under the action of SL(2,ℂ).

theorem PauliMatrix.action_pauliCoDown (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode pauliCoDown)).tensor = (TensorTree.tensorNode pauliCoDown).tensor

The tensor pauliCoDown is invariant under the action of SL(2,ℂ).

theorem PauliMatrix.action_pauliContrDown (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (TensorTree.action g (TensorTree.tensorNode pauliContrDown)).tensor = (TensorTree.tensorNode pauliContrDown).tensor

The tensor pauliContrDown is invariant under the action of SL(2,ℂ).