Pauli matrices as a tensor

Tersorial structure

The tensorial structure on the type Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ and properties thereof.

def PauliMatrix.indexEquiv : TensorSpecies.Tensor.ComponentIdx ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] ≃ (Fin 1 ⊕ Fin 3) × Fin 2 × Fin 2

The equivalence between the type of indices of a [.up, .upL, .upR] tensor and (Fin 1 ⊕ Fin 3) × Fin 2 × Fin 2.

Equations

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

instance PauliMatrix.tensorial : complexLorentzTensor.Tensorial ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] (Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ)

Equations

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

theorem PauliMatrix.toTensor_symm_apply (p : complexLorentzTensor.Tensor ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) : TensorSpecies.Tensorial.toTensor.symm p = (Equiv.piCongrRight fun (x : Fin 1 ⊕ Fin 3) => Equiv.curry (Fin 2) (Fin 2) ℂ) ((Equiv.curry (Fin 1 ⊕ Fin 3) (Fin 2 × Fin 2) ℂ) ((Equiv.piCongrLeft' (fun (a : TensorSpecies.Tensor.ComponentIdx ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) => ℂ) indexEquiv) (Finsupp.equivFunOnFinite ((TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]).repr p))))

theorem PauliMatrix.toTensor_symm_basis (b : (x : Fin (Nat.succ 0).succ.succ) → Fin (complexLorentzTensor.repDim (![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] x))) : TensorSpecies.Tensorial.toTensor.symm ((TensorSpecies.Tensor.basis ![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR]) b) = fun (μ : Fin 1 ⊕ Fin 3) (α : Fin (complexLorentzTensor.repDim (![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] 1))) (β : Fin (complexLorentzTensor.repDim (![complexLorentzTensor.Color.up, complexLorentzTensor.Color.upL, complexLorentzTensor.Color.upR] 2))) => if b 0 = finSumFinEquiv μ ∧ b 1 = α ∧ b 2 = β then 1 else 0

Pauli matrices as a tensor

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

The Pauli matarices as a tensor toTensor pauliMatrix in ℂT[.up, .upL, .upR].

Equations

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

theorem PauliMatrix.toTensor_basis_expand : TensorSpecies.Tensorial.toTensor pauliMatrix = ((((((((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.toTensor_eq_asConsTensor : TensorSpecies.Tensorial.toTensor pauliMatrix = TensorSpecies.Tensor.fromConstTriple asConsTensor

theorem PauliMatrix.toTensor_eq_ofRat : TensorSpecies.Tensorial.toTensor pauliMatrix = 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

@[simp]

theorem PauliMatrix.smul_eq_self (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) : Λ • pauliMatrix = pauliMatrix

@[simp]

theorem PauliMatrix.toTensor_smul_eq_self (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) : Λ • TensorSpecies.Tensorial.toTensor pauliMatrix = TensorSpecies.Tensorial.toTensor pauliMatrix

Variations of the pauli tensor

@[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.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.smul_pauliCo (g : Matrix.SpecialLinearGroup (Fin 2) ℂ) : g • pauliCo = pauliCo

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

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

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

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

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