Pauli matrices

The pauli matrices are defined ultimately through

• pauliMatrix which is a map Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ. The notation σ can be used as short hand.

A tensorial structure is put on Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ to allow the use of index notation. We then define the following notation:

• σ^^^ is the tensorial version of the Pauli matrices, which is a complex Lorentz tensor of type ℂT[.up, .upL, .upR].

and the following abbreviations:

• σ_^^ is the Pauli matrices as a complex Lorentz tensor of type ℂT[.down, .upL, .upR].
• σ___ is the Pauli matrices as a complex Lorentz tensor of type ℂT[.down, .downR, .downL].
• σ^__ is the Pauli matrices as a complex Lorentz tensor of type ℂT[.up, .downR, .downL].

def PauliMatrix.pauliMatrix : Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ

The Pauli matrices.

Equations

• PauliMatrix.pauliMatrix (Sum.inl 0) = 1
• PauliMatrix.pauliMatrix (Sum.inr 0) = !![0, 1; 1, 0]
• PauliMatrix.pauliMatrix (Sum.inr 1) = !![0, -Complex.I; Complex.I, 0]
• PauliMatrix.pauliMatrix (Sum.inr 2) = !![1, 0; 0, -1]

def PauliMatrix.termσ : Lean.ParserDescr

The Pauli matrices.

Equations

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

def PauliMatrix.termσ0 : Lean.ParserDescr

The 'Pauli matrix' corresponding to the identity 1.

Equations

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

def PauliMatrix.termσ1 : Lean.ParserDescr

The Pauli matrix corresponding to the matrix !![0, 1; 1, 0].

Equations

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

def PauliMatrix.termσ2 : Lean.ParserDescr

The Pauli matrix corresponding to the matrix !![0, -I; I, 0].

Equations

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

def PauliMatrix.termσ3 : Lean.ParserDescr

The Pauli matrix corresponding to the matrix !![1, 0; 0, -1].

Equations

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

theorem PauliMatrix.pauliMatrix_inl_zero_eq_one : pauliMatrix (Sum.inl 0) = 1

Matrix relations

theorem PauliMatrix.pauliMatrix_selfAdjoint (μ : Fin 1 ⊕ Fin 3) : (pauliMatrix μ).conjTranspose = pauliMatrix μ

Inversions

Lemmas related to the inversions of the Pauli matrices.

@[simp]

theorem PauliMatrix.pauliMatrix_mul_self (μ : Fin 1 ⊕ Fin 3) : pauliMatrix μ * pauliMatrix μ = 1

instance PauliMatrix.pauliMatrixInvertiable (μ : Fin 1 ⊕ Fin 3) : Invertible (pauliMatrix μ)

Equations

• PauliMatrix.pauliMatrixInvertiable μ = { invOf := PauliMatrix.pauliMatrix μ, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem PauliMatrix.pauliMatrix_inv (μ : Fin 1 ⊕ Fin 3) : ⅟(pauliMatrix μ) = pauliMatrix μ

Products

These lemmas try to put the terms in numerical order. We skip σ0 since it's just 1 anyway.

@[simp]

theorem PauliMatrix.σ2_mul_σ1 : pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 0) = -(pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 1))

@[simp]

theorem PauliMatrix.σ3_mul_σ1 : pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 0) = -(pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 2))

@[simp]

theorem PauliMatrix.σ3_mul_σ2 : pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 1) = -(pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 2))

Traces

@[simp]

theorem PauliMatrix.trace_σ1 : (pauliMatrix (Sum.inr 0)).trace = 0

@[simp]

theorem PauliMatrix.trace_σ2 : (pauliMatrix (Sum.inr 1)).trace = 0

@[simp]

theorem PauliMatrix.trace_σ3 : (pauliMatrix (Sum.inr 2)).trace = 0

theorem PauliMatrix.σ0_σ0_trace : (pauliMatrix (Sum.inl 0) * pauliMatrix (Sum.inl 0)).trace = 2

The trace of σ0 multiplied by σ0 is equal to 2.

theorem PauliMatrix.σ0_σ1_trace : (pauliMatrix (Sum.inl 0) * pauliMatrix (Sum.inr 0)).trace = 0

The trace of σ0 multiplied by σ1 is equal to 0.

theorem PauliMatrix.σ0_σ2_trace : (pauliMatrix (Sum.inl 0) * pauliMatrix (Sum.inr 1)).trace = 0

The trace of σ0 multiplied by σ2 is equal to 0.

theorem PauliMatrix.σ0_σ3_trace : (pauliMatrix (Sum.inl 0) * pauliMatrix (Sum.inr 2)).trace = 0

The trace of σ0 multiplied by σ3 is equal to 0.

theorem PauliMatrix.σ1_σ0_trace : (pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inl 0)).trace = 0

The trace of σ1 multiplied by σ0 is equal to 0.

theorem PauliMatrix.σ1_σ1_trace : (pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 0)).trace = 2

The trace of σ1 multiplied by σ1 is equal to 2.

@[simp]

theorem PauliMatrix.σ1_σ2_trace : (pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 1)).trace = 0

The trace of σ1 multiplied by σ2 is equal to 0.

@[simp]

theorem PauliMatrix.σ1_σ3_trace : (pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 2)).trace = 0

The trace of σ1 multiplied by σ3 is equal to 0.

theorem PauliMatrix.σ2_σ0_trace : (pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inl 0)).trace = 0

The trace of σ2 multiplied by σ0 is equal to 0.

theorem PauliMatrix.σ2_σ1_trace : (pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 0)).trace = 0

The trace of σ2 multiplied by σ1 is equal to 0.

theorem PauliMatrix.σ2_σ2_trace : (pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 1)).trace = 2

The trace of σ2 multiplied by σ2 is equal to 2.

@[simp]

theorem PauliMatrix.σ2_σ3_trace : (pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 2)).trace = 0

The trace of σ2 multiplied by σ3 is equal to 0.

theorem PauliMatrix.σ3_σ0_trace : (pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inl 0)).trace = 0

The trace of σ3 multiplied by σ0 is equal to 0.

theorem PauliMatrix.σ3_σ1_trace : (pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 0)).trace = 0

The trace of σ3 multiplied by σ1 is equal to 0.

theorem PauliMatrix.σ3_σ2_trace : (pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 1)).trace = 0

The trace of σ3 multiplied by σ2 is equal to 0.

theorem PauliMatrix.σ3_σ3_trace : (pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 2)).trace = 2

The trace of σ3 multiplied by σ3 is equal to 2.

Commutation relations

Lemmas related to the commutation relations of the Pauli matrices.

theorem PauliMatrix.σ1_σ2_commutator : pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 1) - pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 0) = (2 * Complex.I) • pauliMatrix (Sum.inr 2)

theorem PauliMatrix.σ1_σ3_commutator : pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 2) - pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 0) = -(2 * Complex.I) • pauliMatrix (Sum.inr 1)

theorem PauliMatrix.σ2_σ1_commutator : pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 0) - pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 1) = -(2 * Complex.I) • pauliMatrix (Sum.inr 2)

theorem PauliMatrix.σ2_σ3_commutator : pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 2) - pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 1) = (2 * Complex.I) • pauliMatrix (Sum.inr 0)

theorem PauliMatrix.σ3_σ1_commutator : pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 0) - pauliMatrix (Sum.inr 0) * pauliMatrix (Sum.inr 2) = (2 * Complex.I) • pauliMatrix (Sum.inr 1)

theorem PauliMatrix.σ3_σ2_commutator : pauliMatrix (Sum.inr 2) * pauliMatrix (Sum.inr 1) - pauliMatrix (Sum.inr 1) * pauliMatrix (Sum.inr 2) = -(2 * Complex.I) • pauliMatrix (Sum.inr 0)