PhysLean Documentation

PhysLean.Relativity.Lorentz.MinkowskiMatrix

The Minkowski matrix #

The definition of the Minkowski Matrix #

source
def minkowskiMatrix {d : ℕ} :
Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ

The d.succ-dimensional real matrix of the form diag(1, -1, -1, -1, ...).

Equations
Instances For
    source
    def minkowskiMatrix.termη :
    Lean.ParserDescr

    Notation for minkowskiMatrix.

    Equations
    Instances For
      source
      @[simp]
      theorem minkowskiMatrix.sq {d : ℕ} :
      minkowskiMatrix * minkowskiMatrix = 1

      The Minkowski matrix is self-inverting.

      source
      @[simp]
      theorem minkowskiMatrix.eq_transpose {d : ℕ} :
      minkowskiMatrix.transpose = minkowskiMatrix

      The Minkowski matrix is symmetric.

      source
      @[simp]
      theorem minkowskiMatrix.det_eq_neg_one_pow_d {d : ℕ} :
      minkowskiMatrix.det = (-1) ^ d

      The determinant of the Minkowski matrix is equal to -1 to the power of the number of spatial dimensions.

      source
      @[simp]
      theorem minkowskiMatrix.η_apply_mul_η_apply_diag {d : ℕ} (μ : Fin 1 ⊕ Fin d) :
      minkowskiMatrix μ μ * minkowskiMatrix μ μ = 1

      Multiplying any element on the diagonal of the Minkowski matrix by itself gives 1.

      source
      theorem minkowskiMatrix.as_block {d : ℕ} :
      minkowskiMatrix = Matrix.fromBlocks 1 0 0 (-1)

      The Minkowski matrix as a block matrix.

      source
      @[simp]
      theorem minkowskiMatrix.off_diag_zero {d : ℕ} {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) :
      minkowskiMatrix μ ν = 0

      The off diagonal elements of the Minkowski matrix are zero.

      source
      theorem minkowskiMatrix.inl_0_inl_0 {d : ℕ} :
      minkowskiMatrix (Sum.inl 0) (Sum.inl 0) = 1

      The time-time component of the Minkowski matrix is 1.

      source
      theorem minkowskiMatrix.inr_i_inr_i {d : ℕ} (i : Fin d) :
      minkowskiMatrix (Sum.inr i) (Sum.inr i) = -1

      The space diagonal components of the Minkowski matrix are -1.

      source
      @[simp]
      theorem minkowskiMatrix.mulVec_inl_0 {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
      minkowskiMatrix.mulVec v (Sum.inl 0) = v (Sum.inl 0)

      The time components of a vector acted on by the Minkowski matrix remains unchanged.

      source
      @[simp]
      theorem minkowskiMatrix.mulVec_inr_i {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) (i : Fin d) :
      minkowskiMatrix.mulVec v (Sum.inr i) = -v (Sum.inr i)

      The space components of a vector acted on by the Minkowski matrix swaps sign.

      source
      def minkowskiMatrix.dual {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
      Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ

      The dual of a matrix with respect to the Minkowski metric. A suitable name fo this construction is the Minkowski dual.

      Equations
      Instances For
        source
        @[simp]
        theorem minkowskiMatrix.dual_id {d : ℕ} :
        dual 1 = 1

        The Minkowski dual of the identity is the identity.

        source
        @[simp]
        theorem minkowskiMatrix.dual_mul {d : ℕ} (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
        dual (Λ * Λ') = dual Λ' * dual Λ

        The Minkowski dual swaps multiplications (acts contravariantly).

        source
        @[simp]
        theorem minkowskiMatrix.dual_dual {d : ℕ} :
        Function.Involutive dual

        The Minkowski dual is involutive (i.e. dual (dual Λ)) = Λ).

        source
        @[simp]
        theorem minkowskiMatrix.dual_eta {d : ℕ} :
        dual minkowskiMatrix = minkowskiMatrix

        The Minkowski dual preserves the Minkowski matrix.

        source
        @[simp]
        theorem minkowskiMatrix.dual_transpose {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
        dual Λ.transpose = (dual Λ).transpose

        The Minkowski dual commutes with the transpose.

        source
        @[simp]
        theorem minkowskiMatrix.det_dual {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
        (dual Λ).det = Λ.det

        The Minkowski dual preserves determinants.

        source
        theorem minkowskiMatrix.dual_apply {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (μ ν : Fin 1 ⊕ Fin d) :
        dual Λ μ ν = minkowskiMatrix μ μ * Λ ν μ * minkowskiMatrix ν ν

        Expansion of the components of the Minkowski dual in terms of the components of the original matrix.

        source
        theorem minkowskiMatrix.dual_apply_minkowskiMatrix {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (μ ν : Fin 1 ⊕ Fin d) :
        dual Λ μ ν * minkowskiMatrix ν ν = minkowskiMatrix μ μ * Λ ν μ

        The components of the Minkowski dual of a matrix multiplied by the Minkowski matrix in terms of the original matrix.