Pauli matrices

The Pauli matrices are an invariant complex Lorentz tensor with three indices, two fermionic and one bosonic.

Definitions.

@[reducible, inline]

abbrev PauliMatrix.pauliContr : complexLorentzTensor.Tensor ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]

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

Equations

• PauliMatrix.pauliContr = TensorSpecies.Tensor.fromConstTriple PauliMatrix.asConsTensor

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 "σ^^^")

@[reducible, inline]

abbrev PauliMatrix.pauliCo : complexLorentzTensor.Tensor ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]

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 "σ_^^")

@[reducible, inline]

abbrev PauliMatrix.pauliCoDown : complexLorentzTensor.Tensor ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downL]

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 "σ___")

@[reducible, inline]

abbrev PauliMatrix.pauliContrDown : complexLorentzTensor.Tensor ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downL]

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 "σ^__")

Different forms

theorem PauliMatrix.pauliContr_eq_fromConstTriple : pauliContr = TensorSpecies.Tensor.fromConstTriple asConsTensor

theorem PauliMatrix.pauliContr_eq_fromTripleT : pauliContr = TensorSpecies.Tensor.fromTripleT asTensor

theorem PauliMatrix.pauliContr_eq_basis : pauliContr = ((((((((TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => 0 | 1 => 0 | 2 => 0) + (TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => 0 | 1 => 1 | 2 => 1) + (TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => 1 | 1 => 0 | 2 => 1) + (TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => 1 | 1 => 1 | 2 => 0) - Complex.I • (TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => 2 | 1 => 0 | 2 => 1) + Complex.I • (TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => 2 | 1 => 1 | 2 => 0) + (TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => 3 | 1 => 0 | 2 => 0) - (TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => 3 | 1 => 1 | 2 => 1

theorem PauliMatrix.pauliContr_eq_ofRat : pauliContr = complexLorentzTensor.ofRat fun (b : TensorSpecies.Tensor.ComponentIdx ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) => if b 0 = 0 ∧ b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = 1 ∧ b 1 ≠ b 2 then { fst := 1, snd := 0 } else if b 0 = 2 ∧ b 1 = 0 ∧ b 2 = 1 then { fst := 0, snd := -1 } else if b 0 = 2 ∧ b 1 = 1 ∧ b 2 = 0 then { fst := 0, snd := 1 } else if b 0 = 3 ∧ b 1 = 0 ∧ b 2 = 0 then { fst := 1, snd := 0 } else if b 0 = 3 ∧ b 1 = 3 ∧ b 2 = 3 then { fst := -1, snd := 0 } else 0

theorem PauliMatrix.pauliCo_eq_ofRat : pauliCo = complexLorentzTensor.ofRat fun (b : TensorSpecies.Tensor.ComponentIdx ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) => if b 0 = 0 ∧ b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = 1 ∧ b 1 ≠ b 2 then { fst := -1, snd := 0 } else if b 0 = 2 ∧ b 1 = 0 ∧ b 2 = 1 then { fst := 0, snd := 1 } else if b 0 = 2 ∧ b 1 = 1 ∧ b 2 = 0 then { fst := 0, snd := -1 } else if b 0 = 3 ∧ b 1 = 0 ∧ b 2 = 0 then { fst := -1, snd := 0 } else if b 0 = 3 ∧ b 1 = 1 ∧ b 2 = 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }

theorem PauliMatrix.pauliCoDown_eq_ofRat : pauliCoDown = complexLorentzTensor.ofRat fun (b : TensorSpecies.Tensor.ComponentIdx ![complexLorentzTensor.Color.down, complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downL]) => if b 0 = 0 ∧ b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = 1 ∧ b 1 ≠ b 2 then { fst := 1, snd := 0 } else if b 0 = 2 ∧ b 1 = 0 ∧ b 2 = 1 then { fst := 0, snd := -1 } else if b 0 = 2 ∧ b 1 = 1 ∧ b 2 = 0 then { fst := 0, snd := 1 } else if b 0 = 3 ∧ b 1 = 1 ∧ b 2 = 1 then { fst := -1, snd := 0 } else if b 0 = 3 ∧ b 1 = 0 ∧ b 2 = 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }

theorem PauliMatrix.pauliContrDown_ofRat : pauliContrDown = complexLorentzTensor.ofRat fun (b : TensorSpecies.Tensor.ComponentIdx ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.downR, complexLorentzTensor.Color.downL]) => if b 0 = 0 ∧ b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = 1 ∧ b 1 ≠ b 2 then { fst := -1, snd := 0 } else if b 0 = 2 ∧ b 1 = 0 ∧ b 2 = 1 then { fst := 0, snd := 1 } else if b 0 = 2 ∧ b 1 = 1 ∧ b 2 = 0 then { fst := 0, snd := -1 } else if b 0 = 3 ∧ b 1 = 1 ∧ b 2 = 1 then { fst := 1, snd := 0 } else if b 0 = 3 ∧ b 1 = 0 ∧ b 2 = 0 then { fst := -1, snd := 0 } else 0

Group actions

theorem PauliMatrix.actionT_pauliContr (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • pauliContr = pauliContr

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

theorem PauliMatrix.actionT_pauliCo (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • pauliCo = pauliCo

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

theorem PauliMatrix.actionT_pauliCoDown (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • pauliCoDown = pauliCoDown

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

theorem PauliMatrix.actionT_pauliContrDown (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • pauliContrDown = pauliContrDown

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