PhysLean Documentation

PhysLean.Relativity.PauliMatrices.SelfAdjoint

Interaction of Pauli matrices with self-adjoint matrices #

source
theorem PauliMatrix.trace_pauliMatrix_mul_selfAdjoint_re (μ : Fin 1 ⊕ Fin 3) (A : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) :
↑(pauliMatrix μ * ↑A).trace.re = (pauliMatrix μ * ↑A).trace

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

source
theorem PauliMatrix.selfAdjoint_ext_complex {A B : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))} (h0 : (pauliMatrix (Sum.inl 0) * ↑A).trace = (pauliMatrix (Sum.inl 0) * ↑B).trace) (h1 : (pauliMatrix (Sum.inr 0) * ↑A).trace = (pauliMatrix (Sum.inr 0) * ↑B).trace) (h2 : (pauliMatrix (Sum.inr 1) * ↑A).trace = (pauliMatrix (Sum.inr 1) * ↑B).trace) (h3 : (pauliMatrix (Sum.inr 2) * ↑A).trace = (pauliMatrix (Sum.inr 2) * ↑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.

source
theorem PauliMatrix.selfAdjoint_ext {A B : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))} (h0 : (pauliMatrix (Sum.inl 0) * ↑A).trace.re = (pauliMatrix (Sum.inl 0) * ↑B).trace.re) (h1 : (pauliMatrix (Sum.inr 0) * ↑A).trace.re = (pauliMatrix (Sum.inr 0) * ↑B).trace.re) (h2 : (pauliMatrix (Sum.inr 1) * ↑A).trace.re = (pauliMatrix (Sum.inr 1) * ↑B).trace.re) (h3 : (pauliMatrix (Sum.inr 2) * ↑A).trace.re = (pauliMatrix (Sum.inr 2) * ↑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.

source
def PauliMatrix.pauliSelfAdjoint (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
Instances For
    source
    theorem PauliMatrix.pauliSelfAdjoint_linearly_independent :
    LinearIndependent ℝ pauliSelfAdjoint

    The Pauli matrices are linearly independent.

    source
    theorem PauliMatrix.pauliSelfAdjoint_span :
    ⊤ ≤ Submodule.span ℝ (Set.range pauliSelfAdjoint)

    The Pauli matrices span all self-adjoint matrices.

    source
    def PauliMatrix.pauliBasis :
    Module.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
    Instances For
      source
      def PauliMatrix.pauliSelfAdjoint' (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
      Instances For
        source
        theorem PauliMatrix.pauliSelfAdjoint'_linearly_independent :
        LinearIndependent ℝ pauliSelfAdjoint'

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

        source
        theorem PauliMatrix.pauliSelfAdjoint'_span :
        ⊤ ≤ Submodule.span ℝ (Set.range pauliSelfAdjoint')

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

        source
        def PauliMatrix.pauliBasis' :
        Module.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
        Instances For
          source
          theorem PauliMatrix.pauliBasis'_decomp (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) :
          M = (1 / 2 * (pauliMatrix (Sum.inl 0) * ↑M).trace.re) • pauliBasis' (Sum.inl 0) + (-1 / 2 * (pauliMatrix (Sum.inr 0) * ↑M).trace.re) • pauliBasis' (Sum.inr 0) + (-1 / 2 * (pauliMatrix (Sum.inr 1) * ↑M).trace.re) • pauliBasis' (Sum.inr 1) + (-1 / 2 * (pauliMatrix (Sum.inr 2) * ↑M).trace.re) • pauliBasis' (Sum.inr 2)

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

          source
          @[simp]
          theorem PauliMatrix.pauliBasis'_repr_inl_0 (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) :
          ↑((pauliBasis'.repr M) (Sum.inl 0)) = 1 / 2 * (pauliMatrix (Sum.inl 0) * ↑M).trace

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

          source
          @[simp]
          theorem PauliMatrix.pauliBasis'_repr_inr_0 (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) :
          ↑((pauliBasis'.repr M) (Sum.inr 0)) = -1 / 2 * (pauliMatrix (Sum.inr 0) * ↑M).trace

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

          source
          @[simp]
          theorem PauliMatrix.pauliBasis'_repr_inr_1 (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) :
          ↑((pauliBasis'.repr M) (Sum.inr 1)) = -1 / 2 * (pauliMatrix (Sum.inr 1) * ↑M).trace

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

          source
          @[simp]
          theorem PauliMatrix.pauliBasis'_repr_inr_2 (M : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) :
          ↑((pauliBasis'.repr M) (Sum.inr 2)) = -1 / 2 * (pauliMatrix (Sum.inr 2) * ↑M).trace

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

          source
          theorem PauliMatrix.pauliBasis_minkowskiMetric_pauliBasis' (i : Fin 1 ⊕ Fin 3) :
          pauliBasis i = minkowskiMatrix i i • pauliBasis' i

          The relationship between the basis pauliBasis of contravariant Pauli-matrices and the basis pauliBasis' of covariant Pauli matrices is by multiplication by the Minkowski matrix.