Physlib.Relativity.PauliMatrices.Basic

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 Mathlib.Analysis.Complex.Basic
public import Mathlib.LinearAlgebra.Matrix.Trace

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].

@[expose] public section

The Pauli matrices.

def pauliMatrix : Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ
  | Sum.inl 0 => 1
  | Sum.inr 0 => !![0, 1; 1, 0]
  | Sum.inr 1 => !![0, -I; I, 0]
  | Sum.inr 2 => !![1, 0; 0, -1]

@[inherit_doc pauliMatrix]
scoped[PauliMatrix] notation "σ" => pauliMatrix

The 'Pauli matrix' corresponding to the identity 1.

scoped[PauliMatrix] notation "σ0" => σ (Sum.inl 0)

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

scoped[PauliMatrix] notation "σ1" => σ (Sum.inr 0)

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

scoped[PauliMatrix] notation "σ2" => σ (Sum.inr 1)

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

scoped[PauliMatrix] notation "σ3" => σ (Sum.inr 2)

lemma pauliMatrix_inl_zero_eq_one : pauliMatrix (Sum.inl 0) = 1 := by⊢ σ (Sum.inl 0) = 1
  dsimp [pauliMatrix]All goals completed! 🐙

Matrix relations



lemma pauliMatrix_selfAdjoint (μ : Fin 1 ⊕ Fin 3) :
    (σ μ)ᴴ = σ μ := byμ:Fin 1 ⊕ Fin 3⊢ (σ μ)ᴴ = σ μ
  fin_cases μ«0»⊢ (σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)))ᴴ = σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩))«1»⊢ (σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)))ᴴ = σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩))«2»⊢ (σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)))ᴴ = σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩))«3»⊢ (σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)))ᴴ = σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩))
  all_goals
    dsimp [pauliMatrix]«3»⊢ !![1, 0; 0, -1]ᴴ = !![1, 0; 0, -1]
    rw [eta_fin_two _ᴴ«0»⊢ !![1ᴴ 0 0, 1ᴴ 0 1; 1ᴴ 1 0, 1ᴴ 1 1] = 1«3»⊢ !![!![1, 0; 0, -1]ᴴ 0 0, !![1, 0; 0, -1]ᴴ 0 1; !![1, 0; 0, -1]ᴴ 1 0, !![1, 0; 0, -1]ᴴ 1 1] = !![1, 0; 0, -1]]«2»⊢ !![!![0, -I; I, 0]ᴴ 0 0, !![0, -I; I, 0]ᴴ 0 1; !![0, -I; I, 0]ᴴ 1 0, !![0, -I; I, 0]ᴴ 1 1] = !![0, -I; I, 0]«3»⊢ !![!![1, 0; 0, -1]ᴴ 0 0, !![1, 0; 0, -1]ᴴ 0 1; !![1, 0; 0, -1]ᴴ 1 0, !![1, 0; 0, -1]ᴴ 1 1] = !![1, 0; 0, -1]«3»⊢ !![!![1, 0; 0, -1]ᴴ 0 0, !![1, 0; 0, -1]ᴴ 0 1; !![1, 0; 0, -1]ᴴ 1 0, !![1, 0; 0, -1]ᴴ 1 1] = !![1, 0; 0, -1]
    simpAll goals completed! 🐙
  ext i j«0»i:Fin 2j:Fin 2⊢ !![1, 0; 0, 1] i j = 1 i j
  fin_cases i«0».«0»j:Fin 2⊢ !![1, 0; 0, 1] ((fun i => i) ⟨0, ⋯⟩) j = 1 ((fun i => i) ⟨0, ⋯⟩) j«0».«1»j:Fin 2⊢ !![1, 0; 0, 1] ((fun i => i) ⟨1, ⋯⟩) j = 1 ((fun i => i) ⟨1, ⋯⟩) j <;>«0».«0»j:Fin 2⊢ !![1, 0; 0, 1] ((fun i => i) ⟨0, ⋯⟩) j = 1 ((fun i => i) ⟨0, ⋯⟩) j«0».«1»j:Fin 2⊢ !![1, 0; 0, 1] ((fun i => i) ⟨1, ⋯⟩) j = 1 ((fun i => i) ⟨1, ⋯⟩) j fin_cases j«0».«1».«0»⊢ !![1, 0; 0, 1] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = 1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)«0».«1».«1»⊢ !![1, 0; 0, 1] ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = 1 ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)
  all_goals
    simpAll goals completed! 🐙

Inversions

Lemmas related to the inversions of the Pauli matrices.

              @[simp]
lemma pauliMatrix_mul_self (μ : Fin 1 ⊕ Fin 3) :
    (σ μ) * (σ μ) = 1 := byμ:Fin 1 ⊕ Fin 3⊢ σ μ * σ μ = 1
  fin_cases μ«0»⊢ σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inl ((fun i => i) ⟨0, ⋯⟩)) = 1«1»⊢ σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) * σ (Sum.inr ((fun i => i) ⟨0, ⋯⟩)) = 1«2»⊢ σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) * σ (Sum.inr ((fun i => i) ⟨1, ⋯⟩)) = 1«3»⊢ σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) * σ (Sum.inr ((fun i => i) ⟨2, ⋯⟩)) = 1
  all_goals
    dsimp [pauliMatrix]«3»⊢ !![1, 0; 0, -1] * !![1, 0; 0, -1] = 1
    simp [one_fin_two]All goals completed! 🐙instance pauliMatrixInvertiable (μ : Fin 1 ⊕ Fin 3) : Invertible (σ μ) := byμ:Fin 1 ⊕ Fin 3⊢ Invertible (σ μ)
  use σ μinvOf_mul_selfμ:Fin 1 ⊕ Fin 3⊢ σ μ * σ μ = 1mul_invOf_selfμ:Fin 1 ⊕ Fin 3⊢ σ μ * σ μ = 1
  ·invOf_mul_selfμ:Fin 1 ⊕ Fin 3⊢ σ μ * σ μ = 1 simpAll goals completed! 🐙
  ·mul_invOf_selfμ:Fin 1 ⊕ Fin 3⊢ σ μ * σ μ = 1 simpAll goals completed! 🐙lemma pauliMatrix_inv (μ : Fin 1 ⊕ Fin 3) :
    ⅟ (σ μ) = σ μ := byμ:Fin 1 ⊕ Fin 3⊢ ⅟(σ μ) = σ μ rflAll goals completed! 🐙

Products

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

              @[simp] lemma σ2_mul_σ1 : σ2 * σ1 = -(σ1 * σ2) := by⊢ σ (Sum.inr 1) * σ (Sum.inr 0) = -(σ (Sum.inr 0) * σ (Sum.inr 1)) simp [pauliMatrix]All goals completed! 🐙@[simp] lemma σ3_mul_σ1 : σ3 * σ1 = -(σ1 * σ3) := by⊢ σ (Sum.inr 2) * σ (Sum.inr 0) = -(σ (Sum.inr 0) * σ (Sum.inr 2)) simp [pauliMatrix]All goals completed! 🐙@[simp] lemma σ3_mul_σ2 : σ3 * σ2 = -(σ2 * σ3) := by⊢ σ (Sum.inr 2) * σ (Sum.inr 1) = -(σ (Sum.inr 1) * σ (Sum.inr 2)) simp [pauliMatrix]All goals completed! 🐙

Traces

              @[simp] lemma trace_σ1 : Matrix.trace σ1 = 0 := by⊢ (σ (Sum.inr 0)).trace = 0 simp [pauliMatrix]All goals completed! 🐙@[simp] lemma trace_σ2 : Matrix.trace σ2 = 0 := by⊢ (σ (Sum.inr 1)).trace = 0 simp [pauliMatrix]All goals completed! 🐙@[simp] lemma trace_σ3 : Matrix.trace σ3 = 0 := by⊢ (σ (Sum.inr 2)).trace = 0 simp [pauliMatrix]All goals completed! 🐙

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

lemma σ0_σ0_trace : Matrix.trace (σ0 * σ0) = 2 := by⊢ (σ (Sum.inl 0) * σ (Sum.inl 0)).trace = 2 simpAll goals completed! 🐙

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

lemma σ0_σ1_trace : Matrix.trace (σ0 * σ1) = 0 := by⊢ (σ (Sum.inl 0) * σ (Sum.inr 0)).trace = 0 simp [pauliMatrix]All goals completed! 🐙

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

lemma σ0_σ2_trace : Matrix.trace (σ0 * σ2) = 0 := by⊢ (σ (Sum.inl 0) * σ (Sum.inr 1)).trace = 0 simp [pauliMatrix]All goals completed! 🐙

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

lemma σ0_σ3_trace : Matrix.trace (σ0 * σ3) = 0 := by⊢ (σ (Sum.inl 0) * σ (Sum.inr 2)).trace = 0 simp [pauliMatrix]All goals completed! 🐙

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

lemma σ1_σ0_trace : Matrix.trace (σ1 * σ0) = 0 := by⊢ (σ (Sum.inr 0) * σ (Sum.inl 0)).trace = 0 simp [pauliMatrix]All goals completed! 🐙

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

lemma σ1_σ1_trace : Matrix.trace (σ1 * σ1) = 2 := by⊢ (σ (Sum.inr 0) * σ (Sum.inr 0)).trace = 2 simpAll goals completed! 🐙

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

@[simp]
lemma σ1_σ2_trace : Matrix.trace (σ1 * σ2) = 0 := by⊢ (σ (Sum.inr 0) * σ (Sum.inr 1)).trace = 0
  simp [pauliMatrix]All goals completed! 🐙

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

@[simp]
lemma σ1_σ3_trace : Matrix.trace (σ1 * σ3) = 0 := by⊢ (σ (Sum.inr 0) * σ (Sum.inr 2)).trace = 0
  simp [pauliMatrix]All goals completed! 🐙

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

lemma σ2_σ0_trace : Matrix.trace (σ2 * σ0) = 0 := by⊢ (σ (Sum.inr 1) * σ (Sum.inl 0)).trace = 0 simp [pauliMatrix]All goals completed! 🐙

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

lemma σ2_σ1_trace : Matrix.trace (σ2 * σ1) = 0 := by⊢ (σ (Sum.inr 1) * σ (Sum.inr 0)).trace = 0
  simp [pauliMatrix]All goals completed! 🐙

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

lemma σ2_σ2_trace : Matrix.trace (σ2 * σ2) = 2 := by⊢ (σ (Sum.inr 1) * σ (Sum.inr 1)).trace = 2 simpAll goals completed! 🐙

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

@[simp]
lemma σ2_σ3_trace : Matrix.trace (σ2 * σ3) = 0 := by⊢ (σ (Sum.inr 1) * σ (Sum.inr 2)).trace = 0
  simp [pauliMatrix]All goals completed! 🐙

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

lemma σ3_σ0_trace : Matrix.trace (σ3 * σ0) = 0 := by⊢ (σ (Sum.inr 2) * σ (Sum.inl 0)).trace = 0 simp [pauliMatrix]All goals completed! 🐙

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

lemma σ3_σ1_trace : Matrix.trace (σ3 * σ1) = 0 := by⊢ (σ (Sum.inr 2) * σ (Sum.inr 0)).trace = 0 simpAll goals completed! 🐙

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

lemma σ3_σ2_trace : Matrix.trace (σ3 * σ2) = 0 := by⊢ (σ (Sum.inr 2) * σ (Sum.inr 1)).trace = 0 simpAll goals completed! 🐙

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

lemma σ3_σ3_trace : Matrix.trace (σ3 * σ3) = 2 := by⊢ (σ (Sum.inr 2) * σ (Sum.inr 2)).trace = 2 simpAll goals completed! 🐙

Commutation relations

Lemmas related to the commutation relations of the Pauli matrices.

              lemma σ1_σ2_commutator : σ1 * σ2 - σ2 * σ1 = (2 * I) • σ3 := by⊢ σ (Sum.inr 0) * σ (Sum.inr 1) - σ (Sum.inr 1) * σ (Sum.inr 0) = (2 * I) • σ (Sum.inr 2)
  simp [pauliMatrix]⊢ (I + I = 2 * I ∧ 0 = ![0]) ∧ -I - I = -(2 * I)
  ring_nf⊢ (True ∧ 0 = ![0]) ∧ True
  simp only [true_and, and_true]⊢ 0 = ![0]
  exact List.ofFn_inj.mp rflAll goals completed! 🐙lemma σ1_σ3_commutator : σ1 * σ3 - σ3 * σ1 = - (2 * I) • σ2 := by⊢ σ (Sum.inr 0) * σ (Sum.inr 2) - σ (Sum.inr 2) * σ (Sum.inr 0) = -(2 * I) • σ (Sum.inr 1)
  simp [pauliMatrix]⊢ -1 - 1 = 2 * I * I ∧ 1 + 1 = -(2 * I * I) ∧ 0 = ![0]
  ring_nf⊢ -2 = I ^ 2 * 2 ∧ 2 = -(I ^ 2 * 2) ∧ 0 = ![0]
  simp only [I_sq, neg_mul, one_mul, neg_neg, true_and]⊢ 0 = ![0]
  exact List.ofFn_inj.mp rflAll goals completed! 🐙lemma σ2_σ1_commutator : σ2 * σ1 - σ1 * σ2 = -(2 * I) • σ3 := by⊢ σ (Sum.inr 1) * σ (Sum.inr 0) - σ (Sum.inr 0) * σ (Sum.inr 1) = -(2 * I) • σ (Sum.inr 2)
  simp [pauliMatrix]⊢ (-I - I = -(2 * I) ∧ 0 = ![0]) ∧ I + I = 2 * I
  ring_nf⊢ (True ∧ 0 = ![0]) ∧ True
  simp only [true_and, and_true]⊢ 0 = ![0]
  exact List.ofFn_inj.mp rflAll goals completed! 🐙lemma σ2_σ3_commutator : σ2 * σ3 - σ3 * σ2 = (2 * I) • σ1 := by⊢ σ (Sum.inr 1) * σ (Sum.inr 2) - σ (Sum.inr 2) * σ (Sum.inr 1) = (2 * I) • σ (Sum.inr 0)
  simp [pauliMatrix]⊢ I + I = 2 * I ∧ 0 = ![0]
  ring_nf⊢ True ∧ 0 = ![0]
  simp only [true_and]⊢ 0 = ![0]
  exact List.ofFn_inj.mp rflAll goals completed! 🐙lemma σ3_σ1_commutator : σ3 * σ1 - σ1 * σ3 = (2 * I) • σ2 := by⊢ σ (Sum.inr 2) * σ (Sum.inr 0) - σ (Sum.inr 0) * σ (Sum.inr 2) = (2 * I) • σ (Sum.inr 1)
  simp [pauliMatrix]⊢ 1 + 1 = -(2 * I * I) ∧ -1 - 1 = 2 * I * I ∧ 0 = ![0]
  ring_nf⊢ 2 = -(I ^ 2 * 2) ∧ -2 = I ^ 2 * 2 ∧ 0 = ![0]
  simp only [I_sq, neg_mul, one_mul, neg_neg, true_and]⊢ 0 = ![0]
  exact List.ofFn_inj.mp rflAll goals completed! 🐙lemma σ3_σ2_commutator : σ3 * σ2 - σ2 * σ3 = -(2 * I) • σ1 := by⊢ σ (Sum.inr 2) * σ (Sum.inr 1) - σ (Sum.inr 1) * σ (Sum.inr 2) = -(2 * I) • σ (Sum.inr 0)
  simp [pauliMatrix]⊢ -I - I = -(2 * I) ∧ 0 = ![0]
  ring_nf⊢ True ∧ 0 = ![0]
  simp only [true_and]⊢ 0 = ![0]
  exact List.ofFn_inj.mp rflAll goals completed! 🐙