Interaction of Pauli matrices with self-adjoint matrices

theorem PauliMatrix.selfAdjoint_trace_σ0_real (A : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑(σ0 * ↑A).trace.re = (σ0 * ↑A).trace

The trace of σ0 multiplied by a self-adjoint 2×2 matrix is real.

theorem PauliMatrix.selfAdjoint_trace_σ1_real (A : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑(σ1 * ↑A).trace.re = (σ1 * ↑A).trace

The trace of σ1 multiplied by a self-adjoint 2×2 matrix is real.

theorem PauliMatrix.selfAdjoint_trace_σ2_real (A : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑(σ2 * ↑A).trace.re = (σ2 * ↑A).trace

The trace of σ2 multiplied by a self-adjoint 2×2 matrix is real.

theorem PauliMatrix.selfAdjoint_trace_σ3_real (A : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑(σ3 * ↑A).trace.re = (σ3 * ↑A).trace

The trace of σ3 multiplied by a self-adjoint 2×2 matrix is real.

theorem PauliMatrix.selfAdjoint_ext_complex {A B : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))} (h0 : (σ0 * ↑A).trace = (σ0 * ↑B).trace) (h1 : (σ1 * ↑A).trace = (σ1 * ↑B).trace) (h2 : (σ2 * ↑A).trace = (σ2 * ↑B).trace) (h3 : (σ3 * ↑A).trace = (σ3 * ↑B).trace) : A = B

Two 2×2 self-adjoint matrices are equal if the (complex) traces of each matrix multiplied by each of the Pauli-matrices are equal.

theorem PauliMatrix.selfAdjoint_ext {A B : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))} (h0 : (σ0 * ↑A).trace.re = (σ0 * ↑B).trace.re) (h1 : (σ1 * ↑A).trace.re = (σ1 * ↑B).trace.re) (h2 : (σ2 * ↑A).trace.re = (σ2 * ↑B).trace.re) (h3 : (σ3 * ↑A).trace.re = (σ3 * ↑B).trace.re) : A = B

Two 2×2 self-adjoint matrices are equal if the real traces of each matrix multiplied by each of the Pauli-matrices are equal.

def PauliMatrix.σSA' (i : Fin 1 ⊕ Fin 3) : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))

An auxiliary function which on i : Fin 1 ⊕ Fin 3 returns the corresponding Pauli-matrix as a self-adjoint matrix.

Equations

• PauliMatrix.σSA' (Sum.inl 0) = ⟨PauliMatrix.σ0, PauliMatrix.σ0_selfAdjoint⟩
• PauliMatrix.σSA' (Sum.inr 0) = ⟨PauliMatrix.σ1, PauliMatrix.σ1_selfAdjoint⟩
• PauliMatrix.σSA' (Sum.inr 1) = ⟨PauliMatrix.σ2, PauliMatrix.σ2_selfAdjoint⟩
• PauliMatrix.σSA' (Sum.inr 2) = ⟨PauliMatrix.σ3, PauliMatrix.σ3_selfAdjoint⟩

theorem PauliMatrix.σSA_linearly_independent : LinearIndependent ℝ σSA'

The Pauli matrices are linearly independent.

theorem PauliMatrix.σSA_span : ⊤ ≤ Submodule.span ℝ (Set.range σSA')

The Pauli matrices span all self-adjoint matrices.

def PauliMatrix.σSA : Basis (Fin 1 ⊕ Fin 3) ℝ ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))

The basis of selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) formed by Pauli matrices.

Equations

• PauliMatrix.σSA = Basis.mk PauliMatrix.σSA_linearly_independent PauliMatrix.σSA_span

def PauliMatrix.σSAL' (i : Fin 1 ⊕ Fin 3) : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))

An auxiliary function which on i : Fin 1 ⊕ Fin 3 returns the corresponding Pauli-matrix as a self-adjoint matrix with a minus sign for Sum.inr _.

Equations

• PauliMatrix.σSAL' (Sum.inl 0) = ⟨PauliMatrix.σ0, PauliMatrix.σ0_selfAdjoint⟩
• PauliMatrix.σSAL' (Sum.inr 0) = ⟨-PauliMatrix.σ1, PauliMatrix.σSAL'.proof_1⟩
• PauliMatrix.σSAL' (Sum.inr 1) = ⟨-PauliMatrix.σ2, PauliMatrix.σSAL'.proof_2⟩
• PauliMatrix.σSAL' (Sum.inr 2) = ⟨-PauliMatrix.σ3, PauliMatrix.σSAL'.proof_3⟩

theorem PauliMatrix.σSAL_linearly_independent : LinearIndependent ℝ σSAL'

The Pauli matrices where σi are negated are linearly independent.

theorem PauliMatrix.σSAL_span : ⊤ ≤ Submodule.span ℝ (Set.range σSAL')

The Pauli matrices where σi are negated span all Self-adjoint matrices.

def PauliMatrix.σSAL : Basis (Fin 1 ⊕ Fin 3) ℝ ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))

The basis of selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) formed by Pauli matrices where the 1, 2, 3 pauli matrices are negated. These can be thought of as the covariant Pauli-matrices.

Equations

• PauliMatrix.σSAL = Basis.mk PauliMatrix.σSAL_linearly_independent PauliMatrix.σSAL_span

theorem PauliMatrix.σSAL_decomp (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : M = (1 / 2 * (σ0 * ↑M).trace.re) • σSAL (Sum.inl 0) + (-1 / 2 * (σ1 * ↑M).trace.re) • σSAL (Sum.inr 0) + (-1 / 2 * (σ2 * ↑M).trace.re) • σSAL (Sum.inr 1) + (-1 / 2 * (σ3 * ↑M).trace.re) • σSAL (Sum.inr 2)

The decomposition of a self-adjoint matrix into the Pauli matrices (where σi are negated).

@[simp]

theorem PauliMatrix.σSAL_repr_inl_0 (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑((σSAL.repr M) (Sum.inl 0)) = 1 / 2 * (σ0 * ↑M).trace

The component of a self-adjoint matrix in the direction σ0 under the basis formed by the covariant Pauli matrices.

@[simp]

theorem PauliMatrix.σSAL_repr_inr_0 (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑((σSAL.repr M) (Sum.inr 0)) = -1 / 2 * (σ1 * ↑M).trace

The component of a self-adjoint matrix in the direction -σ1 under the basis formed by the covariant Pauli matrices.

@[simp]

theorem PauliMatrix.σSAL_repr_inr_1 (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑((σSAL.repr M) (Sum.inr 1)) = -1 / 2 * (σ2 * ↑M).trace

The component of a self-adjoint matrix in the direction -σ2 under the basis formed by the covariant Pauli matrices.

@[simp]

theorem PauliMatrix.σSAL_repr_inr_2 (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑((σSAL.repr M) (Sum.inr 2)) = -1 / 2 * (σ3 * ↑M).trace

The component of a self-adjoint matrix in the direction -σ3 under the basis formed by the covariant Pauli matrices.

theorem PauliMatrix.σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) : σSA i = minkowskiMatrix i i • σSAL i

The relationship between the basis σSA of contravariant Pauli-matrices and the basis σSAL of covariant Pauli matrices is by multiplication by the Minkowski matrix.