The Lorentz Group

We define the Lorentz group.

References

• Lorentz Transformations, Rotations, and Boosts, Jaffe. https://cdn.ku.edu.tr/cdn/files/amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf

Matrices which preserves the Minkowski metric

We start studying the properties of matrices which preserve ηLin. These matrices form the Lorentz group, which we will define in the next section at lorentzGroup.

def LorentzGroup (d : ℕ) : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)

The Lorentz group is the subset of matrices for which Λ * dual Λ = 1.

Equations

• LorentzGroup d = {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ | Λ * minkowskiMatrix.dual Λ = 1}

def LorentzGroup.lorentzGroup_notation : Lean.ParserDescr

Notation for the Lorentz group.

Equations

• LorentzGroup.lorentzGroup_notation = Lean.ParserDescr.node `LorentzGroup.lorentzGroup_notation 1024 (Lean.ParserDescr.symbol "𝓛")

Membership conditions

theorem LorentzGroup.mem_iff_self_mul_dual {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : Λ ∈ LorentzGroup d ↔ Λ * minkowskiMatrix.dual Λ = 1

theorem LorentzGroup.mem_iff_dual_mul_self {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : Λ ∈ LorentzGroup d ↔ minkowskiMatrix.dual Λ * Λ = 1

theorem LorentzGroup.mem_iff_transpose {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : Λ ∈ LorentzGroup d ↔ Λ.transpose ∈ LorentzGroup d

theorem LorentzGroup.mem_mul {d : ℕ} {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} (hΛ : Λ ∈ LorentzGroup d) (hΛ' : Λ' ∈ LorentzGroup d) : Λ * Λ' ∈ LorentzGroup d

theorem LorentzGroup.one_mem {d : ℕ} : 1 ∈ LorentzGroup d

theorem LorentzGroup.dual_mem {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} (h : Λ ∈ LorentzGroup d) : minkowskiMatrix.dual Λ ∈ LorentzGroup d

The Lorentz group as a group

instance lorentzGroupIsGroup {d : ℕ} : Group ↑(LorentzGroup d)

The instance of a group on LorentzGroup d.

Equations

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

@[simp]

theorem lorentzGroupIsGroup_one_coe {d : ℕ} : ↑1 = 1

@[simp]

theorem lorentzGroupIsGroup_inv {d : ℕ} (A : ↑(LorentzGroup d)) : A⁻¹ = ⟨minkowskiMatrix.dual ↑A, ⋯⟩

@[simp]

theorem lorentzGroupIsGroup_div {d : ℕ} (a b : ↑(LorentzGroup d)) : a / b = DivInvMonoid.div' a b

@[simp]

theorem lorentzGroupIsGroup_mul_coe {d : ℕ} (A B : ↑(LorentzGroup d)) : ↑(A * B) = ↑A * ↑B

theorem inv_eq_dual {d : ℕ} (Λ : ↑(LorentzGroup d)) : ↑Λ⁻¹ = minkowskiMatrix.dual ↑Λ

instance instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup {d : ℕ} : TopologicalSpace ↑(LorentzGroup d)

LorentzGroup has the subtype topology.

Equations

• instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup = instTopologicalSpaceSubtype

theorem LorentzGroup.coe_inv {d : ℕ} {Λ : ↑(LorentzGroup d)} : ↑Λ⁻¹ = (↑Λ)⁻¹

instance LorentzGroup.instInvertibleMatrixSumFinOfNatNatRealValMemSet {d : ℕ} (M : ↑(LorentzGroup d)) : Invertible ↑M

The underlying matrix of a Lorentz transformation is invertible.

Equations

• LorentzGroup.instInvertibleMatrixSumFinOfNatNatRealValMemSet M = { invOf := (↑M)⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem LorentzGroup.subtype_inv_mul {d : ℕ} {Λ : ↑(LorentzGroup d)} : (↑Λ)⁻¹ * ↑Λ = 1

theorem LorentzGroup.subtype_mul_inv {d : ℕ} {Λ : ↑(LorentzGroup d)} : ↑Λ * (↑Λ)⁻¹ = 1

@[simp]

theorem LorentzGroup.mul_minkowskiMatrix_mul_transpose {d : ℕ} {Λ : ↑(LorentzGroup d)} : ↑Λ * minkowskiMatrix * (↑Λ).transpose = minkowskiMatrix

@[simp]

theorem LorentzGroup.transpose_mul_minkowskiMatrix_mul_self {d : ℕ} {Λ : ↑(LorentzGroup d)} : (↑Λ).transpose * minkowskiMatrix * ↑Λ = minkowskiMatrix

def LorentzGroup.transpose {d : ℕ} (Λ : ↑(LorentzGroup d)) : ↑(LorentzGroup d)

The transpose of a matrix in the Lorentz group is an element of the Lorentz group.

Equations

• LorentzGroup.transpose Λ = ⟨(↑Λ).transpose, ⋯⟩

@[simp]

theorem LorentzGroup.transpose_one {d : ℕ} : transpose 1 = 1

@[simp]

theorem LorentzGroup.transpose_mul {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} : transpose (Λ * Λ') = transpose Λ' * transpose Λ

theorem LorentzGroup.transpose_val {d : ℕ} {Λ : ↑(LorentzGroup d)} : ↑(transpose Λ) = (↑Λ).transpose

theorem LorentzGroup.transpose_inv {d : ℕ} {Λ : ↑(LorentzGroup d)} : (transpose Λ)⁻¹ = transpose Λ⁻¹

theorem LorentzGroup.comm_minkowskiMatrix {d : ℕ} {Λ : ↑(LorentzGroup d)} : ↑Λ * minkowskiMatrix = minkowskiMatrix * ↑(transpose Λ⁻¹)

theorem LorentzGroup.minkowskiMatrix_comm {d : ℕ} {Λ : ↑(LorentzGroup d)} : minkowskiMatrix * ↑Λ = ↑(transpose Λ⁻¹) * minkowskiMatrix

Lorentz group as a topological group

We now show that the Lorentz group is a topological group. We do this by showing that the natural map from the Lorentz group to GL (Fin 4) ℝ is an embedding.

def LorentzGroup.toGL {d : ℕ} : ↑(LorentzGroup d) →* GL (Fin 1 ⊕ Fin d) ℝ

The homomorphism of the Lorentz group into GL (Fin 4) ℝ.

Equations

• LorentzGroup.toGL = { toFun := fun (A : ↑(LorentzGroup d)) => { val := ↑A, inv := ↑A⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

theorem LorentzGroup.toGL_injective {d : ℕ} : Function.Injective ⇑toGL

def LorentzGroup.toProd {d : ℕ} : ↑(LorentzGroup d) →* Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ × (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)ᵐᵒᵖ

The homomorphism from the Lorentz Group into the monoid of matrices times the opposite of the monoid of matrices.

Equations

• LorentzGroup.toProd = (Units.embedProduct (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)).comp LorentzGroup.toGL

@[simp]

theorem LorentzGroup.toProd_apply {d : ℕ} (a✝ : ↑(LorentzGroup d)) : toProd a✝ = (↑(toGL a✝), (MulOpposite.op ↑(toGL a✝))⁻¹)

theorem LorentzGroup.toProd_eq_transpose_η {d : ℕ} {Λ : ↑(LorentzGroup d)} : toProd Λ = (↑Λ, MulOpposite.op (minkowskiMatrix.dual ↑Λ))

theorem LorentzGroup.toProd_injective {d : ℕ} : Function.Injective ⇑toProd

theorem LorentzGroup.toProd_continuous {d : ℕ} : Continuous ⇑toProd

theorem LorentzGroup.toProd_embedding {d : ℕ} : Topology.IsEmbedding ⇑toProd

The embedding from the Lorentz Group into the monoid of matrices times the opposite of the monoid of matrices.

theorem LorentzGroup.toGL_embedding {d : ℕ} : Topology.IsEmbedding (↑toGL).toFun

The embedding from the Lorentz Group into GL (Fin 4) ℝ.

instance LorentzGroup.instIsTopologicalGroupElemMatrixSumFinOfNatNatReal {d : ℕ} : IsTopologicalGroup ↑(LorentzGroup d)

The embedding of the Lorentz group into GL(n, ℝ) gives LorentzGroup d an instance of a topological group.

To Complex matrices

def LorentzGroup.toComplex {d : ℕ} : ↑(LorentzGroup d) →* Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℂ

The monoid homomorphisms taking the lorentz group to complex matrices.

Equations

• LorentzGroup.toComplex = { toFun := fun (Λ : ↑(LorentzGroup d)) => (↑Λ).map ⇑Complex.ofRealHom, map_one' := ⋯, map_mul' := ⋯ }

instance LorentzGroup.instInvertibleMatrixSumFinOfNatNatComplexCoeMonoidHomElemRealToComplex {d : ℕ} (M : ↑(LorentzGroup d)) : Invertible (toComplex M)

The image of a Lorentz transformation under toComplex is invertible.

Equations

• LorentzGroup.instInvertibleMatrixSumFinOfNatNatComplexCoeMonoidHomElemRealToComplex M = { invOf := LorentzGroup.toComplex M⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem LorentzGroup.toComplex_inv {d : ℕ} (Λ : ↑(LorentzGroup d)) : (toComplex Λ)⁻¹ = toComplex Λ⁻¹

@[simp]

theorem LorentzGroup.toComplex_mul_minkowskiMatrix_mul_transpose {d : ℕ} (Λ : ↑(LorentzGroup d)) : toComplex Λ * minkowskiMatrix.map ⇑Complex.ofRealHom * (toComplex Λ).transpose = minkowskiMatrix.map ⇑Complex.ofRealHom

@[simp]

theorem LorentzGroup.toComplex_transpose_mul_minkowskiMatrix_mul_self {d : ℕ} (Λ : ↑(LorentzGroup d)) : (toComplex Λ).transpose * minkowskiMatrix.map ⇑Complex.ofRealHom * toComplex Λ = minkowskiMatrix.map ⇑Complex.ofRealHom

theorem LorentzGroup.toComplex_mulVec_ofReal {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) (Λ : ↑(LorentzGroup d)) : (toComplex Λ).mulVec (⇑Complex.ofRealHom ∘ v) = ⇑Complex.ofRealHom ∘ (↑Λ).mulVec v

def LorentzGroup.parity {d : ℕ} : ↑(LorentzGroup d)

The parity transformation.

Equations

• LorentzGroup.parity = ⟨minkowskiMatrix, ⋯⟩