The Minkowski Metric

This file introduces the Minkowski metric on spacetime in the mainly-minus signature.

We define the Minkowski metric as a bilinear map on the vector space of Lorentz vectors in d dimensions.

The definition of the Minkowski Matrix

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

• minkowskiMatrix = LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin d) ℝ

def minkowskiMatrix.termη : Lean.ParserDescr

Notation for minkowskiMatrix.

Equations

• minkowskiMatrix.termη = Lean.ParserDescr.node `minkowskiMatrix.termη 1024 (Lean.ParserDescr.symbol "η")

@[simp]

theorem minkowskiMatrix.sq {d : ℕ} : minkowskiMatrix * minkowskiMatrix = 1

@[simp]

theorem minkowskiMatrix.eq_transpose {d : ℕ} : minkowskiMatrix.transpose = minkowskiMatrix

@[simp]

theorem minkowskiMatrix.det_eq_neg_one_pow_d {d : ℕ} : minkowskiMatrix.det = (-1) ^ d

@[simp]

theorem minkowskiMatrix.η_apply_mul_η_apply_diag {d : ℕ} (μ : Fin 1 ⊕ Fin d) : minkowskiMatrix μ μ * minkowskiMatrix μ μ = 1

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

@[simp]

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

The definition of the Minkowski Metric

@[simp]

theorem minkowskiLinearForm_apply {d : ℕ} (v : LorentzVector d) (w : LorentzVector d) : (minkowskiLinearForm v) w = Matrix.dotProduct v (minkowskiMatrix.mulVec w)

def minkowskiLinearForm {d : ℕ} (v : LorentzVector d) : LorentzVector d →ₗ[ℝ] ℝ

Given a Lorentz vector v we define the the linear map w ↦ v * η * w.

Equations

• minkowskiLinearForm v = { toFun := fun (w : LorentzVector d) => Matrix.dotProduct v (minkowskiMatrix.mulVec w), map_add' := ⋯, map_smul' := ⋯ }

def minkowskiMetric {d : ℕ} : LorentzVector d →ₗ[ℝ] LorentzVector d →ₗ[ℝ] ℝ

The Minkowski metric as a bilinear map.

Equations

• minkowskiMetric = { toFun := fun (v : LorentzVector d) => minkowskiLinearForm v, map_add' := ⋯, map_smul' := ⋯ }

def minkowskiMetric.«term⟪_,_⟫ₘ» : Lean.ParserDescr

Notation for minkowskiMetric.

Equations

• One or more equations did not get rendered due to their size.

Equalitites involving the Minkowski metric

theorem minkowskiMetric.as_sum {d : ℕ} (v : LorentzVector d) (w : LorentzVector d) : (minkowskiMetric v) w = v.time * w.time - ∑ i : Fin d, v.space i * w.space i

The Minkowski metric expressed as a sum.

theorem minkowskiMetric.as_sum_self {d : ℕ} (v : LorentzVector d) : (minkowskiMetric v) v = v.time ^ 2 - ‖v.space‖ ^ 2

The Minkowski metric expressed as a sum for a single vector.

theorem minkowskiMetric.eq_time_minus_inner_prod {d : ℕ} (v : LorentzVector d) (w : LorentzVector d) : (minkowskiMetric v) w = v.time * w.time - ⟪v.space, w.space⟫_ℝ

theorem minkowskiMetric.self_eq_time_minus_norm {d : ℕ} (v : LorentzVector d) : (minkowskiMetric v) v = v.time ^ 2 - ‖v.space‖ ^ 2

theorem minkowskiMetric.symm {d : ℕ} (v : LorentzVector d) (w : LorentzVector d) : (minkowskiMetric v) w = (minkowskiMetric w) v

The Minkowski metric is symmetric in its arguments..

theorem minkowskiMetric.time_sq_eq_metric_add_space {d : ℕ} (v : LorentzVector d) : v.time ^ 2 = (minkowskiMetric v) v + ‖v.space‖ ^ 2

Minkowski metric and space reflections

theorem minkowskiMetric.right_spaceReflection {d : ℕ} (v : LorentzVector d) (w : LorentzVector d) : (minkowskiMetric v) w.spaceReflection = v.time * w.time + ⟪v.space, w.space⟫_ℝ

theorem minkowskiMetric.self_spaceReflection_eq_zero_iff {d : ℕ} (v : LorentzVector d) : (minkowskiMetric v) v.spaceReflection = 0 ↔ v = 0

Non degeneracy of the Minkowski metric

theorem minkowskiMetric.nondegenerate {d : ℕ} (v : LorentzVector d) : (∀ (w : LorentzVector d), (minkowskiMetric w) v = 0) ↔ v = 0

The metric tensor is non-degenerate.

Inequalities involving the Minkowski metric

theorem minkowskiMetric.leq_time_sq {d : ℕ} (v : LorentzVector d) : (minkowskiMetric v) v ≤ v.time ^ 2

theorem minkowskiMetric.ge_abs_inner_product {d : ℕ} (v : LorentzVector d) (w : LorentzVector d) : v.time * w.time - ‖⟪v.space, w.space⟫_ℝ‖ ≤ (minkowskiMetric v) w

theorem minkowskiMetric.ge_sub_norm {d : ℕ} (v : LorentzVector d) (w : LorentzVector d) : v.time * w.time - ‖v.space‖ * ‖w.space‖ ≤ (minkowskiMetric v) w

The Minkowski metric and matrices

def minkowskiMetric.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.

Equations

• minkowskiMetric.dual Λ = minkowskiMatrix * Λ.transpose * minkowskiMatrix

@[simp]

theorem minkowskiMetric.dual_id {d : ℕ} : minkowskiMetric.dual 1 = 1

@[simp]

theorem minkowskiMetric.dual_mul {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : minkowskiMetric.dual (Λ * Λ') = minkowskiMetric.dual Λ' * minkowskiMetric.dual Λ

@[simp]

theorem minkowskiMetric.dual_dual {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : minkowskiMetric.dual (minkowskiMetric.dual Λ) = Λ

@[simp]

theorem minkowskiMetric.dual_eta {d : ℕ} : minkowskiMetric.dual minkowskiMatrix = minkowskiMatrix

@[simp]

theorem minkowskiMetric.dual_transpose {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : minkowskiMetric.dual Λ.transpose = (minkowskiMetric.dual Λ).transpose

@[simp]

theorem minkowskiMetric.det_dual {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : (minkowskiMetric.dual Λ).det = Λ.det

@[simp]

theorem minkowskiMetric.dual_mulVec_right {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) {x : LorentzVector d} {y : Fin 1 ⊕ Fin d → ℝ} : (minkowskiMetric x) ((minkowskiMetric.dual Λ).mulVec y) = (minkowskiMetric (Λ.mulVec x)) y

@[simp]

theorem minkowskiMetric.dual_mulVec_left {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) {x : Fin 1 ⊕ Fin d → ℝ} {y : LorentzVector d} : (minkowskiMetric ((minkowskiMetric.dual Λ).mulVec x)) y = (minkowskiMetric x) (Λ.mulVec y)

theorem minkowskiMetric.matrix_apply_eq_iff_sub {d : ℕ} (v : LorentzVector d) (w : LorentzVector d) (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : (minkowskiMetric v) (Λ.mulVec w) = (minkowskiMetric v) (Λ'.mulVec w) ↔ (minkowskiMetric v) ((Λ - Λ').mulVec w) = 0

theorem minkowskiMetric.matrix_eq_iff_eq_forall' {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : (∀ (v : Fin 1 ⊕ Fin d → ℝ), Λ.mulVec v = Λ'.mulVec v) ↔ ∀ (w : Fin 1 ⊕ Fin d → ℝ) (v : LorentzVector d), (minkowskiMetric v) (Λ.mulVec w) = (minkowskiMetric v) (Λ'.mulVec w)

theorem minkowskiMetric.matrix_eq_iff_eq_forall {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : Λ = Λ' ↔ ∀ (w : Fin 1 ⊕ Fin d → ℝ) (v : LorentzVector d), (minkowskiMetric v) (Λ.mulVec w) = (minkowskiMetric v) (Λ'.mulVec w)

theorem minkowskiMetric.matrix_eq_id_iff {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) : Λ = 1 ↔ ∀ (w : Fin 1 ⊕ Fin d → ℝ) (v : LorentzVector d), (minkowskiMetric v) (Λ.mulVec w) = (minkowskiMetric v) w

The Minkowski metric and the standard basis

@[simp]

theorem minkowskiMetric.basis_left {d : ℕ} (v : LorentzVector d) (μ : Fin 1 ⊕ Fin d) : (minkowskiMetric (LorentzVector.stdBasis μ)) v = minkowskiMatrix μ μ * v μ

theorem minkowskiMetric.on_timeVec {d : ℕ} : (minkowskiMetric LorentzVector.timeVec) LorentzVector.timeVec = 1

theorem minkowskiMetric.on_basis_mulVec {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (μ : Fin 1 ⊕ Fin d) (ν : Fin 1 ⊕ Fin d) : (minkowskiMetric (LorentzVector.stdBasis μ)) (Λ.mulVec (LorentzVector.stdBasis ν)) = minkowskiMatrix μ μ * Λ μ ν

theorem minkowskiMetric.on_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) (ν : Fin 1 ⊕ Fin d) : (minkowskiMetric (LorentzVector.stdBasis μ)) (LorentzVector.stdBasis ν) = minkowskiMatrix μ ν

theorem minkowskiMetric.matrix_apply_stdBasis {d : ℕ} (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (ν : Fin 1 ⊕ Fin d) (μ : Fin 1 ⊕ Fin d) : Λ ν μ = minkowskiMatrix ν ν * (minkowskiMetric (LorentzVector.stdBasis ν)) (Λ.mulVec (LorentzVector.stdBasis μ))