The Minkowski matrix

i. Overview

The aim of this module is to define the Minkowski matrix η in d+1 dimensions, and prove properties thereof.

The Minkowski matrix is the real matrix of the form diag(1, -1, -1, -1, ...), It is related to the Minkowski metric on ℝ^(d+1).

Related to the Minkowski matrix is the notion of the dual of a matrix with respect to the Minkowski metric. This is defined as η * Λᵀ * η, where Λ is a real matrix. This will be used to help define the Lorentz group in later files.

ii. Key results

• minkowskiMatrix : The Minkowski matrix in d+1 dimensions.
• minkowskiMatrix.dual : The dual of a matrix with respect to the Minkowski metric, defined to be η * Λᵀ * η.

iii. Table of contents

• A. The Minkowski Matrix
  • A.1. Basic equalitites
  • A.2. Notation for the Minkowski matrix
  • A.3. Components of the Minkowski matrix
  • A.4. Squaring the Minkowski matrix
  • A.5. Symmetry properties of the Minkowski matrix
  • A.6. Determinant of the Minkowski matrix
  • A.7. Injective properties of multiplying diagonal components
  • A.8. Action of the Minkowski matrix on vectors
• B. The Minkowski dual
  • B.1. The dual on the identity
  • B.2. The dual swaps multiplication
  • B.3. The dual is an involution
  • B.4. The dual commutes with the transpose
  • B.5. The dual preserves the Minkowski matrix
  • B.6. The dual preserves the determinants
  • B.7. Components of the dual

iv. References

No references are given here.

A. The Minkowski Matrix

We first define the Minkowski matrix in d+1 dimensions, and prove some basic properties.

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) ℝ

A.1. Basic equalitites

We show some basic equalities for the Minkowski matrix. In particular, we show it can be expressed as a block matrix.

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

The Minkowski matrix as a block matrix.

A.2. Notation for the Minkowski matrix

We define the notation η for the Minkowski matrix, which can be used when the namespace minkowskiMatrix is opened.

def minkowskiMatrix.termη : Lean.ParserDescr

Notation for minkowskiMatrix.

Equations

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

A.3. Components of the Minkowski matrix

We prove some simple properties related to the components of the Minkowski matrix.

@[simp]

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.

@[simp]

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.

@[simp]

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

The off diagonal elements of the Minkowski matrix are zero.

theorem minkowskiMatrix.η_diag_ne_zero {d : ℕ} {μ : Fin 1 ⊕ Fin d} : minkowskiMatrix μ μ ≠ 0

A.4. Squaring the Minkowski matrix

we show that the Minkowski matrix is self-inverting, i.e. η * η = 1, as well as other properties related to squaring the Minkowski matrix.

@[simp]

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

The Minkowski matrix is self-inverting.

@[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.

@[simp]

theorem minkowskiMatrix.η_apply_sq_eq_one {d : ℕ} (μ : Fin 1 ⊕ Fin d) : minkowskiMatrix μ μ ^ 2 = 1

A.5. Symmetry properties of the Minkowski matrix

The Minkowski matrix is symmetric, due to it being diagonal.

@[simp]

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

The Minkowski matrix is symmetric.

A.6. Determinant of the Minkowski matrix

We show the determinant of the Minkowski matrix is equal to (-1)^d where d is the number of spatial dimensions.

@[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.

A.7. Injective properties of multiplying diagonal components

If x and y are reals then since η μ μ is non-zero for any μ, the equation η μ μ * x = η μ μ * y implies x = y. We prove this as a lemma. This is a useful part of the API but is not used oten.

theorem minkowskiMatrix.mul_η_diag_eq_iff {d : ℕ} {μ : Fin 1 ⊕ Fin d} {x y : ℝ} : minkowskiMatrix μ μ * x = minkowskiMatrix μ μ * y ↔ x = y

A.8. Action of the Minkowski matrix on vectors

We show properties of the action of the Minkowski matrix on vectors.

@[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.

@[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.

B. The Minkowski dual

Given a real matrix Λ, we define the dual of Λ with respect to the Minkowski metric to be η * Λᵀ * η.

The ultimate idea is that for the Minkowski inner product ⟪Λ x, y⟫ = ⟪x, dual Λ y⟫ for all vectors x and y.

An element Λ is in the Lorentz group if and only if dual Λ = Λ⁻¹. This will not be shown in this module.

This notion of a dual is not quite a homomorphism because it reverses the order of multiplication.

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 for this construction is the Minkowski dual.

Equations

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

B.1. The dual on the identity

We show that the dual of the identity matrix is the identity matrix.

@[simp]

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

The Minkowski dual of the identity is the identity.

B.2. The dual swaps multiplication

We show that the dual swaps multiplication, i.e. dual (Λ * Λ') = dual Λ' * dual Λ.

@[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).

B.3. The dual is an involution

We show that the dual is an involution, i.e. dual (dual Λ) = Λ.

@[simp]

theorem minkowskiMatrix.dual_dual {d : ℕ} : Function.Involutive dual

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

B.4. The dual commutes with the transpose

@[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.

B.5. The dual preserves the Minkowski matrix

@[simp]

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

The Minkowski dual preserves the Minkowski matrix.

B.6. The dual preserves the determinants

@[simp]

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

The Minkowski dual preserves determinants.

B.7. Components of the dual

We show a number of properties related to the components of the duals.

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.

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.