Physlib.Relativity.LorentzGroup.Basic

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.MinkowskiMatrix
public import Physlib.Meta.TODO.Basic
public import Mathlib.Analysis.Complex.Basic
public import Mathlib.Topology.Instances.Matrix
public import Mathlib.Topology.Maps.Basic
public import Mathlib.Topology.Algebra.Group.ClosedSubgroup

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

@[expose] public sectionTODO "Define the Lie group structure on the Lorentz group."

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.

Notation for the Lorentz group.

scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup

Membership conditions

              lemma mem_iff_self_mul_dual : Λ ∈ LorentzGroup d ↔ Λ * dual Λ = 1 := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ ∈ 𝓛 d ↔ Λ * dual Λ = 1
  rflAll goals completed! 🐙

lemma mem_iff_dual_mul_self : Λ ∈ LorentzGroup d ↔ dual Λ * Λ = 1 := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ ∈ 𝓛 d ↔ dual Λ * Λ = 1
  rw [mem_iff_self_mul_duald:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ * dual Λ = 1 ↔ dual Λ * Λ = 1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ * dual Λ = 1 ↔ dual Λ * Λ = 1]d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ * dual Λ = 1 ↔ dual Λ * Λ = 1
  exact _root_.mul_eq_one_commAll goals completed! 🐙

lemma mem_iff_transpose : Λ ∈ LorentzGroup d ↔ Λᵀ ∈ LorentzGroup d := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ ∈ 𝓛 d ↔ Λᵀ ∈ 𝓛 d
  refine Iff.intro (fun h ↦ ?_) (fun h ↦ ?_)refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 d⊢ Λᵀ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 d⊢ Λ ∈ 𝓛 d
  ·refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 d⊢ Λᵀ ∈ 𝓛 d have h1 := congrArg transpose ((mem_iff_dual_mul_self).mp h)refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:(dual Λ * Λ)ᵀ = 1ᵀ⊢ Λᵀ ∈ 𝓛 d
    rw [dual,refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:(η * Λᵀ * η * Λ)ᵀ = 1ᵀ⊢ Λᵀ ∈ 𝓛 drefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 d transpose_mul,refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * (η * Λᵀ * η)ᵀ = 1ᵀ⊢ Λᵀ ∈ 𝓛 drefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 d transpose_mul,refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * (ηᵀ * (η * Λᵀ)ᵀ) = 1ᵀ⊢ Λᵀ ∈ 𝓛 drefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 d transpose_mul,refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * (ηᵀ * (Λᵀᵀ * ηᵀ)) = 1ᵀ⊢ Λᵀ ∈ 𝓛 drefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 d minkowskiMatrix.eq_transpose,refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * (η * (Λᵀᵀ * η)) = 1ᵀ⊢ Λᵀ ∈ 𝓛 drefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 d
      ← mul_assoc,refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1ᵀ⊢ Λᵀ ∈ 𝓛 drefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 d transpose_onerefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 drefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 d] at h1refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ ∈ 𝓛 d
    rw [mem_iff_self_mul_dual,refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ * dual Λᵀ = 1refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ * (η * Λᵀᵀ * η) = Λᵀ * η * (Λᵀᵀ * η) ← h1,refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ * dual Λᵀ = Λᵀ * η * (Λᵀᵀ * η)refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ * (η * Λᵀᵀ * η) = Λᵀ * η * (Λᵀᵀ * η) dualrefine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ * (η * Λᵀᵀ * η) = Λᵀ * η * (Λᵀᵀ * η)refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ * (η * Λᵀᵀ * η) = Λᵀ * η * (Λᵀᵀ * η)]refine_1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 dh1:Λᵀ * η * (Λᵀᵀ * η) = 1⊢ Λᵀ * (η * Λᵀᵀ * η) = Λᵀ * η * (Λᵀᵀ * η)
    noncomm_ringAll goals completed! 🐙
  ·refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 d⊢ Λ ∈ 𝓛 d have h1 := congrArg transpose ((mem_iff_dual_mul_self).mp h)refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:(dual Λᵀ * Λᵀ)ᵀ = 1ᵀ⊢ Λ ∈ 𝓛 d
    rw [dual,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:(η * Λᵀᵀ * η * Λᵀ)ᵀ = 1ᵀ⊢ Λ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d transpose_mul,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λᵀᵀ * (η * Λᵀᵀ * η)ᵀ = 1ᵀ⊢ Λ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d transpose_mul,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λᵀᵀ * (ηᵀ * (η * Λᵀᵀ)ᵀ) = 1ᵀ⊢ Λ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d transpose_mul,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λᵀᵀ * (ηᵀ * (Λᵀᵀᵀ * ηᵀ)) = 1ᵀ⊢ Λ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d minkowskiMatrix.eq_transpose,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λᵀᵀ * (η * (Λᵀᵀᵀ * η)) = 1ᵀ⊢ Λ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d
      ← mul_assoc,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λᵀᵀ * η * (Λᵀᵀᵀ * η) = 1ᵀ⊢ Λ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d transpose_one,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λᵀᵀ * η * (Λᵀᵀᵀ * η) = 1⊢ Λ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d transpose_transposerefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 drefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d] at h1refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ ∈ 𝓛 d
    rw [mem_iff_self_mul_dual,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ * dual Λ = 1refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ * (η * Λᵀ * η) = Λ * η * (Λᵀ * η) ← h1,refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ * dual Λ = Λ * η * (Λᵀ * η)refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ * (η * Λᵀ * η) = Λ * η * (Λᵀ * η) dualrefine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ * (η * Λᵀ * η) = Λ * η * (Λᵀ * η)refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ * (η * Λᵀ * η) = Λ * η * (Λᵀ * η)]refine_2d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ ∈ 𝓛 dh1:Λ * η * (Λᵀ * η) = 1⊢ Λ * (η * Λᵀ * η) = Λ * η * (Λᵀ * η)
    noncomm_ringAll goals completed! 🐙

lemma mem_iff_neg_mem : Λ ∈ LorentzGroup d ↔ -Λ ∈ LorentzGroup d := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ ∈ 𝓛 d ↔ -Λ ∈ 𝓛 d
  rw [mem_iff_self_mul_dual,d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ * dual Λ = 1 ↔ -Λ ∈ 𝓛 dd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ * dual Λ = 1 ↔ -Λ * dual (-Λ) = 1 mem_iff_self_mul_duald:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ * dual Λ = 1 ↔ -Λ * dual (-Λ) = 1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ * dual Λ = 1 ↔ -Λ * dual (-Λ) = 1]d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ * dual Λ = 1 ↔ -Λ * dual (-Λ) = 1
  simp [dual]All goals completed! 🐙

lemma mem_mul (hΛ : Λ ∈ LorentzGroup d) (hΛ' : Λ' ∈ LorentzGroup d) : Λ * Λ' ∈ LorentzGroup d := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ Λ * Λ' ∈ 𝓛 d
  rw [mem_iff_dual_mul_self,d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual (Λ * Λ') * (Λ * Λ') = 1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * dual Λ * (Λ * Λ') = 1 dual_muld:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * dual Λ * (Λ * Λ') = 1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * dual Λ * (Λ * Λ') = 1]d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * dual Λ * (Λ * Λ') = 1
  trans dual Λ' * (dual Λ * Λ) * Λ'd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * dual Λ * (Λ * Λ') = dual Λ' * (dual Λ * Λ) * Λ'd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * (dual Λ * Λ) * Λ' = 1
  ·d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * dual Λ * (Λ * Λ') = dual Λ' * (dual Λ * Λ) * Λ' noncomm_ringAll goals completed! 🐙
  ·d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * (dual Λ * Λ) * Λ' = 1 rw [(mem_iff_dual_mul_self).mp hΛd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * 1 * Λ' = 1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * 1 * Λ' = 1]d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝΛ':Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝhΛ:Λ ∈ 𝓛 dhΛ':Λ' ∈ 𝓛 d⊢ dual Λ' * 1 * Λ' = 1
    simp [(mem_iff_dual_mul_self).mp hΛ']All goals completed! 🐙

lemma one_mem : 1 ∈ LorentzGroup d := byd:ℕ⊢ 1 ∈ 𝓛 d
  rw [mem_iff_dual_mul_selfd:ℕ⊢ dual 1 * 1 = 1d:ℕ⊢ dual 1 * 1 = 1]d:ℕ⊢ dual 1 * 1 = 1
  simpAll goals completed! 🐙

lemma dual_mem (h : Λ ∈ LorentzGroup d) : dual Λ ∈ LorentzGroup d := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 d⊢ dual Λ ∈ 𝓛 d
  rw [mem_iff_dual_mul_self,d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 d⊢ dual (dual Λ) * dual Λ = 1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 d⊢ Λ * dual Λ = 1 dual_duald:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 d⊢ Λ * dual Λ = 1d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 d⊢ Λ * dual Λ = 1]d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λ ∈ 𝓛 d⊢ Λ * dual Λ = 1
  exact mem_iff_self_mul_dual.mp hAll goals completed! 🐙

A matrix Λ is in the Lorentz group if and only if it satisfies Λᵀ * η * Λ = η.


lemma mem_iff_transpose_mul_minkowskiMatrix_mul_self
    (Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
    Λ ∈ LorentzGroup d ↔ Λᵀ * η * Λ = η := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λ ∈ 𝓛 d ↔ Λᵀ * η * Λ = η
  rw [mem_iff_dual_mul_selfd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ dual Λ * Λ = 1 ↔ Λᵀ * η * Λ = ηd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ dual Λ * Λ = 1 ↔ Λᵀ * η * Λ = η]d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ dual Λ * Λ = 1 ↔ Λᵀ * η * Λ = η
  rw [duald:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ η * Λᵀ * η * Λ = 1 ↔ Λᵀ * η * Λ = ηd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ η * Λᵀ * η * Λ = 1 ↔ Λᵀ * η * Λ = η]d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ η * Λᵀ * η * Λ = 1 ↔ Λᵀ * η * Λ = η
  constructormpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ η * Λᵀ * η * Λ = 1 → Λᵀ * η * Λ = ηmprd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λᵀ * η * Λ = η → η * Λᵀ * η * Λ = 1
  ·mpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ η * Λᵀ * η * Λ = 1 → Λᵀ * η * Λ = η intro hmpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1⊢ Λᵀ * η * Λ = η
    have h' : η * ((η * Λᵀ * η) * Λ) = η * 1 := congr_arg (η * ·) hmpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1h':η * (η * Λᵀ * η * Λ) = η * 1⊢ Λᵀ * η * Λ = η
    rw [mul_onempd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1h':η * (η * Λᵀ * η * Λ) = η⊢ Λᵀ * η * Λ = ηmpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1h':η * (η * Λᵀ * η * Λ) = η⊢ Λᵀ * η * Λ = η] at h'mpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1h':η * (η * Λᵀ * η * Λ) = η⊢ Λᵀ * η * Λ = η
    simp_rw [mpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1h':η * (η * Λᵀ * η * Λ) = η⊢ Λᵀ * η * Λ = η← mul_assoc,mpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1h':η * η * Λᵀ * η * Λ = η⊢ Λᵀ * η * Λ = η sq,mpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1h':1 * Λᵀ * η * Λ = η⊢ Λᵀ * η * Λ = η one_mulmpd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:η * Λᵀ * η * Λ = 1h':Λᵀ * η * Λ = η⊢ Λᵀ * η * Λ = η] at h'
    exact h'All goals completed! 🐙
  ·mprd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ⊢ Λᵀ * η * Λ = η → η * Λᵀ * η * Λ = 1 intro hmprd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ * η * Λ = η⊢ η * Λᵀ * η * Λ = 1
    calc
      (η * Λᵀ * η) * Λ = η * (Λᵀ * η * Λ) := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ * η * Λ = η⊢ η * Λᵀ * η * Λ = η * (Λᵀ * η * Λ) simp_rw [d:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ * η * Λ = η⊢ η * Λᵀ * η * Λ = η * (Λᵀ * η * Λ)mul_assocAll goals completed! 🐙]
      _ = η * η := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ * η * Λ = η⊢ η * (Λᵀ * η * Λ) = η * η rw [hd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ * η * Λ = η⊢ η * η = η * ηAll goals completed! 🐙]All goals completed! 🐙
      _ = 1 := byd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ * η * Λ = η⊢ η * η = 1 rw [minkowskiMatrix.sqd:ℕΛ:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝh:Λᵀ * η * Λ = η⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙

The Lorentz group as a group

The instance of a group on LorentzGroup d.

@[simps! mul_coe one_coe div]
instance lorentzGroupIsGroup : Group (LorentzGroup d) where
  mul A B := ⟨A.1 * B.1, LorentzGroup.mem_mul A.2 B.2⟩
  mul_assoc A B C := Subtype.ext (Matrix.mul_assoc A.1 B.1 C.1)
  one := ⟨1, LorentzGroup.one_mem⟩
  one_mul A := Subtype.ext (Matrix.one_mul A.1)
  mul_one A := Subtype.ext (Matrix.mul_one A.1)
  inv A := ⟨minkowskiMatrix.dual A.1, LorentzGroup.dual_mem A.2⟩
  inv_mul_cancel A := Subtype.ext (LorentzGroup.mem_iff_dual_mul_self.mp A.2)

LorentzGroup has the subtype topology.

instance : TopologicalSpace (LorentzGroup d) := instTopologicalSpaceSubtype

Lorentz group as a closed subset of matrices

lemma continuous_self_mul_dual {d : ℕ} :
    Continuous (fun Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ => Λ * dual Λ) := byd:ℕ⊢ Continuous fun Λ => Λ * dual Λ
  unfold duald:ℕ⊢ Continuous fun Λ => Λ * (η * Λᵀ * η)
  fun_propAll goals completed! 🐙

The Lorentz group is closed in the ambient matrix space.


lemma isClosed (d : ℕ) :
    IsClosed (LorentzGroup d : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)) := byd:ℕ⊢ IsClosed (𝓛 d)
  rw [LorentzGroupd:ℕ⊢ IsClosed {Λ | Λ * dual Λ = 1}d:ℕ⊢ IsClosed {Λ | Λ * dual Λ = 1}]d:ℕ⊢ IsClosed {Λ | Λ * dual Λ = 1}
  exact isClosed_singleton.preimage continuous_self_mul_dualAll goals completed! 🐙

The coercion from the Lorentz group to its ambient matrix space is a closed embedding.

lemma isClosedEmbedding_val {d : ℕ} :
    Topology.IsClosedEmbedding
      (Subtype.val : LorentzGroup d → Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :=
  (isClosed d).isClosedEmbedding_subtypeVal

Inverses

lemma inv_eq_dual (Λ : LorentzGroup d) :
    (Λ⁻¹ : LorentzGroup d) = ⟨minkowskiMatrix.dual Λ.1, LorentzGroup.dual_mem Λ.2⟩ := byd:ℕΛ:↑(𝓛 d)⊢ Λ⁻¹ = ⟨dual ↑Λ, ⋯⟩
  rflAll goals completed! 🐙

lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= (inv_eq_left_inv (mem_iff_dual_mul_self.mp Λ.2)).symm

The underlying matrix of a Lorentz transformation is invertible.


instance (M : LorentzGroup d) : Invertible M.1 where
  invOf := M⁻¹
  invOf_mul_self := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ (↑M)⁻¹ * ↑M = 1
    rw [← coe_invd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ ↑M⁻¹ * ↑M = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ ↑M⁻¹ * ↑M = 1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ ↑M⁻¹ * ↑M = 1
    exact (mem_iff_dual_mul_self.mp M.2)All goals completed! 🐙
  mul_invOf_self := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ ↑M * (↑M)⁻¹ = 1
    rw [← coe_invd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ ↑M * ↑M⁻¹ = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ ↑M * ↑M⁻¹ = 1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ ↑M * ↑M⁻¹ = 1
    exact (mem_iff_self_mul_dual.mp M.2)All goals completed! 🐙

              lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := inv_mul_of_invertible _lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := mul_inv_of_invertible _

@[simp]
lemma mul_minkowskiMatrix_mul_transpose :
    (Subtype.val Λ) * minkowskiMatrix * (Subtype.val Λ).transpose = minkowskiMatrix := byd:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η * (↑Λ)ᵀ = η
  have h2 := Λ.propd:ℕΛ:↑(𝓛 d)h2:↑Λ ∈ 𝓛 d⊢ ↑Λ * η * (↑Λ)ᵀ = η
  rw [LorentzGroup.mem_iff_self_mul_duald:ℕΛ:↑(𝓛 d)h2:↑Λ * dual ↑Λ = 1⊢ ↑Λ * η * (↑Λ)ᵀ = ηd:ℕΛ:↑(𝓛 d)h2:↑Λ * dual ↑Λ = 1⊢ ↑Λ * η * (↑Λ)ᵀ = η] at h2d:ℕΛ:↑(𝓛 d)h2:↑Λ * dual ↑Λ = 1⊢ ↑Λ * η * (↑Λ)ᵀ = η
  simp only [dual] at h2d:ℕΛ:↑(𝓛 d)h2:↑Λ * (η * (↑Λ)ᵀ * η) = 1⊢ ↑Λ * η * (↑Λ)ᵀ = η
  refine (right_inv_eq_left_inv minkowskiMatrix.sq ?_).symmd:ℕΛ:↑(𝓛 d)h2:↑Λ * (η * (↑Λ)ᵀ * η) = 1⊢ ↑Λ * η * (↑Λ)ᵀ * η = 1
  rw [← h2d:ℕΛ:↑(𝓛 d)h2:↑Λ * (η * (↑Λ)ᵀ * η) = 1⊢ ↑Λ * η * (↑Λ)ᵀ * η = ↑Λ * (η * (↑Λ)ᵀ * η)d:ℕΛ:↑(𝓛 d)h2:↑Λ * (η * (↑Λ)ᵀ * η) = 1⊢ ↑Λ * η * (↑Λ)ᵀ * η = ↑Λ * (η * (↑Λ)ᵀ * η)]d:ℕΛ:↑(𝓛 d)h2:↑Λ * (η * (↑Λ)ᵀ * η) = 1⊢ ↑Λ * η * (↑Λ)ᵀ * η = ↑Λ * (η * (↑Λ)ᵀ * η)
  noncomm_ringAll goals completed! 🐙

@[simp]
lemma transpose_mul_minkowskiMatrix_mul_self :
    (Subtype.val Λ).transpose * minkowskiMatrix * (Subtype.val Λ) = minkowskiMatrix := byd:ℕΛ:↑(𝓛 d)⊢ (↑Λ)ᵀ * η * ↑Λ = η
  have h2 := Λ.propd:ℕΛ:↑(𝓛 d)h2:↑Λ ∈ 𝓛 d⊢ (↑Λ)ᵀ * η * ↑Λ = η
  rw [LorentzGroup.mem_iff_dual_mul_selfd:ℕΛ:↑(𝓛 d)h2:dual ↑Λ * ↑Λ = 1⊢ (↑Λ)ᵀ * η * ↑Λ = ηd:ℕΛ:↑(𝓛 d)h2:dual ↑Λ * ↑Λ = 1⊢ (↑Λ)ᵀ * η * ↑Λ = η] at h2d:ℕΛ:↑(𝓛 d)h2:dual ↑Λ * ↑Λ = 1⊢ (↑Λ)ᵀ * η * ↑Λ = η
  simp only [dual] at h2d:ℕΛ:↑(𝓛 d)h2:η * (↑Λ)ᵀ * η * ↑Λ = 1⊢ (↑Λ)ᵀ * η * ↑Λ = η
  refine right_inv_eq_left_inv ?_ minkowskiMatrix.sqd:ℕΛ:↑(𝓛 d)h2:η * (↑Λ)ᵀ * η * ↑Λ = 1⊢ η * ((↑Λ)ᵀ * η * ↑Λ) = 1
  rw [← h2d:ℕΛ:↑(𝓛 d)h2:η * (↑Λ)ᵀ * η * ↑Λ = 1⊢ η * ((↑Λ)ᵀ * η * ↑Λ) = η * (↑Λ)ᵀ * η * ↑Λd:ℕΛ:↑(𝓛 d)h2:η * (↑Λ)ᵀ * η * ↑Λ = 1⊢ η * ((↑Λ)ᵀ * η * ↑Λ) = η * (↑Λ)ᵀ * η * ↑Λ]d:ℕΛ:↑(𝓛 d)h2:η * (↑Λ)ᵀ * η * ↑Λ = 1⊢ η * ((↑Λ)ᵀ * η * ↑Λ) = η * (↑Λ)ᵀ * η * ↑Λ
  noncomm_ringAll goals completed! 🐙

Transpose of a Lorentz transformation

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

def transpose (Λ : LorentzGroup d) : LorentzGroup d :=
  ⟨Λ.1ᵀ, mem_iff_transpose.mp Λ.2⟩

              @[simp]
lemma transpose_one : @transpose d 1 = 1 := Subtype.ext Matrix.transpose_one@[simp]
lemma transpose_mul : transpose (Λ * Λ') = transpose Λ' * transpose Λ :=
  Subtype.ext (Matrix.transpose_mul Λ.1 Λ'.1)lemma transpose_val : (transpose Λ).1 = Λ.1ᵀ := rfl

lemma transpose_inv : (transpose Λ)⁻¹ = transpose Λ⁻¹ := byd:ℕΛ:↑(𝓛 d)⊢ (transpose Λ)⁻¹ = transpose Λ⁻¹
  refine Subtype.ext ?_d:ℕΛ:↑(𝓛 d)⊢ ↑(transpose Λ)⁻¹ = ↑(transpose Λ⁻¹)
  rw [transpose_val,d:ℕΛ:↑(𝓛 d)⊢ ↑(transpose Λ)⁻¹ = (↑Λ⁻¹)ᵀAll goals completed! 🐙 coe_inv,d:ℕΛ:↑(𝓛 d)⊢ (↑(transpose Λ))⁻¹ = (↑Λ⁻¹)ᵀAll goals completed! 🐙 transpose_val,d:ℕΛ:↑(𝓛 d)⊢ (↑Λ)ᵀ⁻¹ = (↑Λ⁻¹)ᵀAll goals completed! 🐙 coe_inv,d:ℕΛ:↑(𝓛 d)⊢ (↑Λ)ᵀ⁻¹ = (↑Λ)⁻¹ᵀAll goals completed! 🐙 Matrix.transpose_nonsing_invd:ℕΛ:↑(𝓛 d)⊢ (↑Λ)ᵀ⁻¹ = (↑Λ)ᵀ⁻¹All goals completed! 🐙]All goals completed! 🐙

lemma comm_minkowskiMatrix : Λ.1 * minkowskiMatrix = minkowskiMatrix * (transpose Λ⁻¹).1 := byd:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η = η * ↑(transpose Λ⁻¹)
  conv_rhs => rw [← @mul_minkowskiMatrix_mul_transpose d Λ]d:ℕΛ:↑(𝓛 d)| ↑Λ * η * (↑Λ)ᵀ * ↑(transpose Λ⁻¹)
  rw [← transpose_inv,d:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η = ↑Λ * η * (↑Λ)ᵀ * ↑(transpose Λ)⁻¹d:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η = ↑Λ * η * (↑Λ)ᵀ * (↑Λ)ᵀ⁻¹ coe_inv,d:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η = ↑Λ * η * (↑Λ)ᵀ * (↑(transpose Λ))⁻¹d:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η = ↑Λ * η * (↑Λ)ᵀ * (↑Λ)ᵀ⁻¹ transpose_vald:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η = ↑Λ * η * (↑Λ)ᵀ * (↑Λ)ᵀ⁻¹d:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η = ↑Λ * η * (↑Λ)ᵀ * (↑Λ)ᵀ⁻¹]d:ℕΛ:↑(𝓛 d)⊢ ↑Λ * η = ↑Λ * η * (↑Λ)ᵀ * (↑Λ)ᵀ⁻¹
  exact Eq.symm (mul_inv_cancel_right_of_invertible _ _)All goals completed! 🐙

lemma minkowskiMatrix_comm : minkowskiMatrix * Λ.1 = (transpose Λ⁻¹).1 * minkowskiMatrix := byd:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = ↑(transpose Λ⁻¹) * η
  conv_rhs => rw [← @transpose_mul_minkowskiMatrix_mul_self d Λ]d:ℕΛ:↑(𝓛 d)| ↑(transpose Λ⁻¹) * ((↑Λ)ᵀ * η * ↑Λ)
  rw [← transpose_inv,d:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = ↑(transpose Λ)⁻¹ * ((↑Λ)ᵀ * η * ↑Λ)d:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * ((↑Λ)ᵀ * η * ↑Λ) coe_inv,d:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑(transpose Λ))⁻¹ * ((↑Λ)ᵀ * η * ↑Λ)d:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * ((↑Λ)ᵀ * η * ↑Λ) transpose_vald:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * ((↑Λ)ᵀ * η * ↑Λ)d:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * ((↑Λ)ᵀ * η * ↑Λ)]d:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * ((↑Λ)ᵀ * η * ↑Λ)
  rw [← mul_assoc,d:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * ((↑Λ)ᵀ * η) * ↑Λd:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λ ← mul_assocd:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λd:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λ]d:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λ
  have h1 : ((Λ.1)ᵀ⁻¹ * (Λ.1)ᵀ) = 1 := byd:ℕΛ:↑(𝓛 d)⊢ η * ↑Λ = ↑(transpose Λ⁻¹) * ηd:ℕΛ:↑(𝓛 d)h1:(↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ = 1⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λ
    rw [← transpose_vald:ℕΛ:↑(𝓛 d)⊢ (↑(transpose Λ))⁻¹ * ↑(transpose Λ) = 1d:ℕΛ:↑(𝓛 d)⊢ (↑(transpose Λ))⁻¹ * ↑(transpose Λ) = 1d:ℕΛ:↑(𝓛 d)h1:(↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ = 1⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λ]d:ℕΛ:↑(𝓛 d)⊢ (↑(transpose Λ))⁻¹ * ↑(transpose Λ) = 1d:ℕΛ:↑(𝓛 d)h1:(↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ = 1⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λ
    simp only [subtype_inv_mul]d:ℕΛ:↑(𝓛 d)h1:(↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ = 1⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λd:ℕΛ:↑(𝓛 d)h1:(↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ = 1⊢ η * ↑Λ = (↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ * η * ↑Λ
  rw [h1d:ℕΛ:↑(𝓛 d)h1:(↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ = 1⊢ η * ↑Λ = 1 * η * ↑Λd:ℕΛ:↑(𝓛 d)h1:(↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ = 1⊢ η * ↑Λ = 1 * η * ↑Λ]d:ℕΛ:↑(𝓛 d)h1:(↑Λ)ᵀ⁻¹ * (↑Λ)ᵀ = 1⊢ η * ↑Λ = 1 * η * ↑Λ
  simpAll goals completed! 🐙

Negation of a Lorentz transformation

The negation of a Lorentz transform.

instance : Neg (LorentzGroup d) where
  neg Λ := ⟨-Λ.1, mem_iff_neg_mem.mp Λ.2⟩

@[simp]
lemma coe_neg : (-Λ).1 = -Λ.1 := rfl

lemma inv_neg : (-Λ)⁻¹ = -Λ⁻¹ := byd:ℕΛ:↑(𝓛 d)⊢ (-Λ)⁻¹ = -Λ⁻¹
  refine Subtype.ext ?_d:ℕΛ:↑(𝓛 d)⊢ ↑(-Λ)⁻¹ = ↑(-Λ⁻¹)
  simp [inv_eq_dual, dual]All goals completed! 🐙

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.

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

def toGL : LorentzGroup d →* GL (Fin 1 ⊕ Fin d) ℝ where
  toFun A := ⟨A.1, (A⁻¹).1, _root_.mul_eq_one_comm.mpr $ mem_iff_dual_mul_self.mp A.2,
    mem_iff_dual_mul_self.mp A.2⟩
  map_one' :=
    (GeneralLinearGroup.ext_iff _ 1).mpr fun _ => congrFun rfl
  map_mul' _ _ :=
    (GeneralLinearGroup.ext_iff _ _).mpr fun _ => congrFun rfl



lemma toGL_injective : Function.Injective (@toGL d) := byd:ℕ⊢ Function.Injective ⇑toGL
  refine fun A B h => Subtype.ext ?_d:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:toGL A = toGL B⊢ ↑A = ↑B
  rw [@Units.ext_iffd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:↑(toGL A) = ↑(toGL B)⊢ ↑A = ↑Bd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:↑(toGL A) = ↑(toGL B)⊢ ↑A = ↑B] at hd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:↑(toGL A) = ↑(toGL B)⊢ ↑A = ↑B
  exact hAll goals completed! 🐙

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

@[simps!]
def toProd : LorentzGroup d →* (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) ×
    (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)ᵐᵒᵖ :=
  MonoidHom.comp (Units.embedProduct _) toGL

              lemma toProd_eq_transpose_η : toProd Λ = (Λ.1, MulOpposite.op $ minkowskiMatrix.dual Λ.1) := rfl

lemma toProd_injective : Function.Injective (@toProd d) := byd:ℕ⊢ Function.Injective ⇑toProd
  intro A B hd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:toProd A = toProd B⊢ A = B
  rw [toProd_eq_transpose_η,d:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:(↑A, MulOpposite.op (dual ↑A)) = toProd B⊢ A = Bd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:(↑A, MulOpposite.op (dual ↑A)) = (↑B, MulOpposite.op (dual ↑B))⊢ A = B toProd_eq_transpose_ηd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:(↑A, MulOpposite.op (dual ↑A)) = (↑B, MulOpposite.op (dual ↑B))⊢ A = Bd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:(↑A, MulOpposite.op (dual ↑A)) = (↑B, MulOpposite.op (dual ↑B))⊢ A = B] at hd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:(↑A, MulOpposite.op (dual ↑A)) = (↑B, MulOpposite.op (dual ↑B))⊢ A = B
  rw [Prod.mk_injd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:↑A = ↑B ∧ MulOpposite.op (dual ↑A) = MulOpposite.op (dual ↑B)⊢ A = Bd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:↑A = ↑B ∧ MulOpposite.op (dual ↑A) = MulOpposite.op (dual ↑B)⊢ A = B] at hd:ℕA:↑(𝓛 d)B:↑(𝓛 d)h:↑A = ↑B ∧ MulOpposite.op (dual ↑A) = MulOpposite.op (dual ↑B)⊢ A = B
  exact Subtype.ext h.1All goals completed! 🐙lemma toProd_continuous : Continuous (@toProd d) := byd:ℕ⊢ Continuous ⇑toProd
  refine continuous_prodMk.mpr ⟨continuous_iff_le_induced.mpr fun U a ↦ a,
    MulOpposite.continuous_op.comp' ((continuous_const.matrix_mul (continuous_iff_le_induced.mpr
      fun U a => a).matrix_transpose).matrix_mul continuous_const)⟩All goals completed! 🐙

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

lemma toProd_embedding : IsEmbedding (@toProd d) where
  injective := toProd_injective
  eq_induced :=
    (isInducing_iff ⇑toProd).mp (IsInducing.of_comp toProd_continuous continuous_fst
      ((isInducing_iff (Prod.fst ∘ ⇑toProd)).mpr rfl))

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


lemma toGL_embedding : IsEmbedding (@toGL d).toFun where
  injective := toGL_injective
  eq_induced := byd:ℕ⊢ instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup =
  TopologicalSpace.induced (↑toGL).toFun Units.instTopologicalSpaceUnits
    refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) fun _ ↦ ?_).symmd:ℕx✝:Set { x // x ∈ 𝓛 d }⊢ IsOpen[TopologicalSpace.induced (↑toGL).toFun Units.instTopologicalSpaceUnits] x✝ ↔ IsOpen x✝
    rw [TopologicalSpace.ext_iff.mp toProd_embedding.eq_induced _,d:ℕx✝:Set { x // x ∈ 𝓛 d }⊢ IsOpen[TopologicalSpace.induced (↑toGL).toFun Units.instTopologicalSpaceUnits] x✝ ↔
  IsOpen[TopologicalSpace.induced (⇑toProd) instTopologicalSpaceProd] x✝d:ℕx✝:Set { x // x ∈ 𝓛 d }⊢ (∃ t, IsOpen t ∧ (↑toGL).toFun ⁻¹' t = x✝) ↔ ∃ t, IsOpen t ∧ ⇑toProd ⁻¹' t = x✝ isOpen_induced_iff,d:ℕx✝:Set { x // x ∈ 𝓛 d }⊢ (∃ t, IsOpen t ∧ (↑toGL).toFun ⁻¹' t = x✝) ↔ IsOpen[TopologicalSpace.induced (⇑toProd) instTopologicalSpaceProd] x✝d:ℕx✝:Set { x // x ∈ 𝓛 d }⊢ (∃ t, IsOpen t ∧ (↑toGL).toFun ⁻¹' t = x✝) ↔ ∃ t, IsOpen t ∧ ⇑toProd ⁻¹' t = x✝
      isOpen_induced_iffd:ℕx✝:Set { x // x ∈ 𝓛 d }⊢ (∃ t, IsOpen t ∧ (↑toGL).toFun ⁻¹' t = x✝) ↔ ∃ t, IsOpen t ∧ ⇑toProd ⁻¹' t = x✝d:ℕx✝:Set { x // x ∈ 𝓛 d }⊢ (∃ t, IsOpen t ∧ (↑toGL).toFun ⁻¹' t = x✝) ↔ ∃ t, IsOpen t ∧ ⇑toProd ⁻¹' t = x✝]d:ℕx✝:Set { x // x ∈ 𝓛 d }⊢ (∃ t, IsOpen t ∧ (↑toGL).toFun ⁻¹' t = x✝) ↔ ∃ t, IsOpen t ∧ ⇑toProd ⁻¹' t = x✝
    exact exists_exists_and_eq_andAll goals completed! 🐙

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

instance : IsTopologicalGroup (LorentzGroup d) :=
  IsInducing.topologicalGroup toGL toGL_embedding.toIsInducing

Lorentz group as a closed subgroup of the general linear group

Following the plan sketched by PrParadoxy and Joseph Tooby-Smith in physlib issue #833, we realise LorentzGroup d as a closed subgroup of GL (Fin 1 ⊕ Fin d) ℝ. This promotes the closed embedding into the ambient matrix space (isClosedEmbedding_val) to the level of the general linear group, and is the structural prerequisite for a Lie group structure on the Lorentz group.

The remaining step of that plan, endowing LorentzGroup d with a Lie group structure as a closed subgroup of the Lie group GL (Fin 1 ⊕ Fin d) ℝ and thereby deriving its Lie algebra, needs the closed subgroup theorem (Cartan's theorem: a closed subgroup of a Lie group is an embedded Lie subgroup). That theorem is not yet available in Mathlib: there is no LieSubgroup, and no ChartedSpace/IsManifold instance is produced from a closed embedding (only IsOpenEmbedding.singletonChartedSpace, for open embeddings). The Lie group instance and the Lorentz algebra therefore remain open; see the TODO at the top of this file.

The range of toGL, as a set in GL (Fin 1 ⊕ Fin d) ℝ, is exactly the preimage of the Lorentz group under the coercion GL (Fin 1 ⊕ Fin d) ℝ → Matrix _ _ ℝ: an element of the general linear group lies in the image precisely when its underlying matrix is a Lorentz transformation.

lemma range_toGL :
    Set.range (@toGL d).toFun =
      Units.val ⁻¹' (LorentzGroup d : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)) := byd:ℕ⊢ Set.range (↑toGL).toFun = Units.val ⁻¹' 𝓛 d
  ext xd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ x ∈ Set.range (↑toGL).toFun ↔ x ∈ Units.val ⁻¹' 𝓛 d
  constructormpd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ x ∈ Set.range (↑toGL).toFun → x ∈ Units.val ⁻¹' 𝓛 dmprd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ x ∈ Units.val ⁻¹' 𝓛 d → x ∈ Set.range (↑toGL).toFun
  ·mpd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ x ∈ Set.range (↑toGL).toFun → x ∈ Units.val ⁻¹' 𝓛 d rintro ⟨A, rfl⟩mpd:ℕA:↑(𝓛 d)⊢ (↑toGL).toFun A ∈ Units.val ⁻¹' 𝓛 d
    exact A.2All goals completed! 🐙
  ·mprd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ x ∈ Units.val ⁻¹' 𝓛 d → x ∈ Set.range (↑toGL).toFun intro hxmprd:ℕx:GL (Fin 1 ⊕ Fin d) ℝhx:x ∈ Units.val ⁻¹' 𝓛 d⊢ x ∈ Set.range (↑toGL).toFun
    exact ⟨⟨x.val, hx⟩, Units.ext rfl⟩All goals completed! 🐙

The homomorphism toGL is a closed embedding of the Lorentz group into GL (Fin 1 ⊕ Fin d) ℝ. This strengthens toGL_embedding: the image is closed because it is the preimage, under the continuous coercion GL (Fin 1 ⊕ Fin d) ℝ → Matrix _ _ ℝ, of the closed set LorentzGroup d (LorentzGroup.isClosed).


lemma toGL_isClosedEmbedding : Topology.IsClosedEmbedding (@toGL d).toFun where
  toIsEmbedding := toGL_embedding
  isClosed_range := byd:ℕ⊢ IsClosed (Set.range (↑toGL).toFun)
    rw [range_toGLd:ℕ⊢ IsClosed (Units.val ⁻¹' 𝓛 d)d:ℕ⊢ IsClosed (Units.val ⁻¹' 𝓛 d)]d:ℕ⊢ IsClosed (Units.val ⁻¹' 𝓛 d)
    exact (isClosed d).preimage Units.continuous_valAll goals completed! 🐙

The Lorentz group realised as a subgroup of GL (Fin 1 ⊕ Fin d) ℝ, namely the range of the embedding toGL.

def toGLSubgroup (d : ℕ) : Subgroup (GL (Fin 1 ⊕ Fin d) ℝ) := (@toGL d).range

@[simp]
lemma mem_toGLSubgroup {x : GL (Fin 1 ⊕ Fin d) ℝ} :
    x ∈ toGLSubgroup d ↔
      (x : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) ∈ LorentzGroup d := byd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ x ∈ toGLSubgroup d ↔ ↑x ∈ 𝓛 d
  constructormpd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ x ∈ toGLSubgroup d → ↑x ∈ 𝓛 dmprd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ ↑x ∈ 𝓛 d → x ∈ toGLSubgroup d
  ·mpd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ x ∈ toGLSubgroup d → ↑x ∈ 𝓛 d rintro ⟨A, rfl⟩mpd:ℕA:↑(𝓛 d)⊢ ↑(toGL A) ∈ 𝓛 d
    exact A.2All goals completed! 🐙
  ·mprd:ℕx:GL (Fin 1 ⊕ Fin d) ℝ⊢ ↑x ∈ 𝓛 d → x ∈ toGLSubgroup d intro hxmprd:ℕx:GL (Fin 1 ⊕ Fin d) ℝhx:↑x ∈ 𝓛 d⊢ x ∈ toGLSubgroup d
    exact ⟨⟨x.val, hx⟩, Units.ext rfl⟩All goals completed! 🐙

lemma coe_toGLSubgroup :
    (toGLSubgroup d : Set (GL (Fin 1 ⊕ Fin d) ℝ)) =
      Units.val ⁻¹' (LorentzGroup d : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)) :=
  range_toGL

The Lorentz group realised as a closed subgroup of GL (Fin 1 ⊕ Fin d) ℝ. The closedness is exactly the content of toGL_isClosedEmbedding, and is the hypothesis that the (not-yet-formalised) closed subgroup theorem would consume to produce a Lie group structure.


def toClosedSubgroup (d : ℕ) : ClosedSubgroup (GL (Fin 1 ⊕ Fin d) ℝ) where
  toSubgroup := toGLSubgroup d
  isClosed' := byd✝:ℕΛ:↑(𝓛 d✝)Λ':↑(𝓛 d✝)d:ℕ⊢ IsClosed (toGLSubgroup d).carrier
    rw [show (toGLSubgroup d).carrier =
        Units.val ⁻¹' (LorentzGroup d : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)) from
      coe_toGLSubgroupd✝:ℕΛ:↑(𝓛 d✝)Λ':↑(𝓛 d✝)d:ℕ⊢ IsClosed (Units.val ⁻¹' 𝓛 d)d✝:ℕΛ:↑(𝓛 d✝)Λ':↑(𝓛 d✝)d:ℕ⊢ IsClosed (Units.val ⁻¹' 𝓛 d)]d✝:ℕΛ:↑(𝓛 d✝)Λ':↑(𝓛 d✝)d:ℕ⊢ IsClosed (Units.val ⁻¹' 𝓛 d)
    exact (isClosed d).preimage Units.continuous_valAll goals completed! 🐙

To Complex matrices

The monoid homomorphisms taking the lorentz group to complex matrices.

def toComplex : LorentzGroup d →* Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℂ where
  toFun Λ := Λ.1.map ofRealHom
  map_one' := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)⊢ (↑1).map ⇑ofRealHom = 1
    ext i jd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (↑1).map (⇑ofRealHom) i j = 1 i j
    simp only [lorentzGroupIsGroup_one_coe, map_apply, ofRealHom_eq_coe]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ↑(1 i j) = 1 i j
    simp only [Matrix.one_apply]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ↑(if i = j then 1 else 0) = if i = j then 1 else 0
    split_ifsposd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dh✝:i = j⊢ ↑1 = 1negd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dh✝:¬i = j⊢ ↑0 = 0
    ·posd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dh✝:i = j⊢ ↑1 = 1 rflAll goals completed! 🐙
    ·negd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin dh✝:¬i = j⊢ ↑0 = 0 rflAll goals completed! 🐙
  map_mul' Λ Λ' := byd:ℕΛ✝:↑(𝓛 d)Λ'✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)⊢ (↑(Λ * Λ')).map ⇑ofRealHom = (↑Λ).map ⇑ofRealHom * (↑Λ').map ⇑ofRealHom
    ext i jd:ℕΛ✝:↑(𝓛 d)Λ'✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (↑(Λ * Λ')).map (⇑ofRealHom) i j = ((↑Λ).map ⇑ofRealHom * (↑Λ').map ⇑ofRealHom) i j
    simp only [lorentzGroupIsGroup_mul_coe, map_apply, ofRealHom_eq_coe]d:ℕΛ✝:↑(𝓛 d)Λ'✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ↑((↑Λ * ↑Λ') i j) = ((↑Λ).map ⇑ofRealHom * (↑Λ').map ⇑ofRealHom) i j
    simp only [← Matrix.map_mul]d:ℕΛ✝:↑(𝓛 d)Λ'✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ↑((↑Λ * ↑Λ') i j) = (↑Λ * ↑Λ').map (⇑ofRealHom) i j
    rflAll goals completed! 🐙

The image of a Lorentz transformation under toComplex is invertible.


instance (M : LorentzGroup d) : Invertible (toComplex M) where
  invOf := toComplex M⁻¹
  invOf_mul_self := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex M⁻¹ * toComplex M = 1
    rw [← toComplex.map_mul,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex (M⁻¹ * M) = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex 1 = 1 Group.inv_mul_canceld:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex 1 = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex 1 = 1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex 1 = 1
    simpAll goals completed! 🐙
  mul_invOf_self := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex M * toComplex M⁻¹ = 1
    rw [← toComplex.map_muld:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex (M * M⁻¹) = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex (M * M⁻¹) = 1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex (M * M⁻¹) = 1
    rw [@mul_inv_canceld:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex 1 = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex 1 = 1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)M:↑(𝓛 d)⊢ toComplex 1 = 1
    simpAll goals completed! 🐙

              

lemma toComplex_inv (Λ : LorentzGroup d) : (toComplex Λ)⁻¹ = toComplex Λ⁻¹ := byd:ℕΛ:↑(𝓛 d)⊢ (toComplex Λ)⁻¹ = toComplex Λ⁻¹
  refine inv_eq_right_inv ?hhd:ℕΛ:↑(𝓛 d)⊢ toComplex Λ * toComplex Λ⁻¹ = 1
  rw [← toComplex.map_mul,hd:ℕΛ:↑(𝓛 d)⊢ toComplex (Λ * Λ⁻¹) = 1hd:ℕΛ:↑(𝓛 d)⊢ toComplex 1 = 1 mul_inv_cancelhd:ℕΛ:↑(𝓛 d)⊢ toComplex 1 = 1hd:ℕΛ:↑(𝓛 d)⊢ toComplex 1 = 1]hd:ℕΛ:↑(𝓛 d)⊢ toComplex 1 = 1
  simpAll goals completed! 🐙

@[simp]
lemma toComplex_mul_minkowskiMatrix_mul_transpose (Λ : LorentzGroup d) :
    toComplex Λ * minkowskiMatrix.map ofRealHom * (toComplex Λ)ᵀ =
    minkowskiMatrix.map ofRealHom := byd:ℕΛ:↑(𝓛 d)⊢ toComplex Λ * η.map ⇑ofRealHom * (toComplex Λ)ᵀ = η.map ⇑ofRealHom
  simp only [toComplex, MonoidHom.coe_mk, OneHom.coe_mk]d:ℕΛ:↑(𝓛 d)⊢ (↑Λ).map ⇑ofRealHom * η.map ⇑ofRealHom * ((↑Λ).map ⇑ofRealHom)ᵀ = η.map ⇑ofRealHom
  have h1 : ((Λ.1).map ⇑ofRealHom)ᵀ = (Λ.1ᵀ).map ofRealHom := rfld:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ).map ⇑ofRealHom * η.map ⇑ofRealHom * ((↑Λ).map ⇑ofRealHom)ᵀ = η.map ⇑ofRealHom
  rw [h1d:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ).map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ)ᵀ.map ⇑ofRealHom = η.map ⇑ofRealHomd:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ).map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ)ᵀ.map ⇑ofRealHom = η.map ⇑ofRealHom]d:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ).map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ)ᵀ.map ⇑ofRealHom = η.map ⇑ofRealHom
  trans (Λ.1 * minkowskiMatrix * Λ.1ᵀ).map ofRealHomd:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ).map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ)ᵀ.map ⇑ofRealHom = (↑Λ * η * (↑Λ)ᵀ).map ⇑ofRealHomd:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ * η * (↑Λ)ᵀ).map ⇑ofRealHom = η.map ⇑ofRealHom
  ·d:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ).map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ)ᵀ.map ⇑ofRealHom = (↑Λ * η * (↑Λ)ᵀ).map ⇑ofRealHom simp only [Matrix.map_mul]All goals completed! 🐙
  simp only [mul_minkowskiMatrix_mul_transpose]All goals completed! 🐙

@[simp]
lemma toComplex_transpose_mul_minkowskiMatrix_mul_self (Λ : LorentzGroup d) :
    (toComplex Λ)ᵀ * minkowskiMatrix.map ofRealHom * toComplex Λ =
    minkowskiMatrix.map ofRealHom := byd:ℕΛ:↑(𝓛 d)⊢ (toComplex Λ)ᵀ * η.map ⇑ofRealHom * toComplex Λ = η.map ⇑ofRealHom
  simp only [toComplex, MonoidHom.coe_mk, OneHom.coe_mk]d:ℕΛ:↑(𝓛 d)⊢ ((↑Λ).map ⇑ofRealHom)ᵀ * η.map ⇑ofRealHom * (↑Λ).map ⇑ofRealHom = η.map ⇑ofRealHom
  have h1 : ((Λ.1).map ofRealHom)ᵀ = (Λ.1ᵀ).map ofRealHom := rfld:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ ((↑Λ).map ⇑ofRealHom)ᵀ * η.map ⇑ofRealHom * (↑Λ).map ⇑ofRealHom = η.map ⇑ofRealHom
  rw [h1d:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ)ᵀ.map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ).map ⇑ofRealHom = η.map ⇑ofRealHomd:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ)ᵀ.map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ).map ⇑ofRealHom = η.map ⇑ofRealHom]d:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ)ᵀ.map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ).map ⇑ofRealHom = η.map ⇑ofRealHom
  trans (Λ.1ᵀ * minkowskiMatrix * Λ.1).map ofRealHomd:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ)ᵀ.map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ).map ⇑ofRealHom = ((↑Λ)ᵀ * η * ↑Λ).map ⇑ofRealHomd:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ ((↑Λ)ᵀ * η * ↑Λ).map ⇑ofRealHom = η.map ⇑ofRealHom
  ·d:ℕΛ:↑(𝓛 d)h1:((↑Λ).map ⇑ofRealHom)ᵀ = (↑Λ)ᵀ.map ⇑ofRealHom⊢ (↑Λ)ᵀ.map ⇑ofRealHom * η.map ⇑ofRealHom * (↑Λ).map ⇑ofRealHom = ((↑Λ)ᵀ * η * ↑Λ).map ⇑ofRealHom simp only [Matrix.map_mul]All goals completed! 🐙
  simp only [transpose_mul_minkowskiMatrix_mul_self]All goals completed! 🐙

lemma toComplex_mulVec_ofReal (v : Fin 1 ⊕ Fin d → ℝ) (Λ : LorentzGroup d) :
    toComplex Λ *ᵥ (ofRealHom ∘ v) = ofRealHom ∘ (Λ *ᵥ v) := byd:ℕv:Fin 1 ⊕ Fin d → ℝΛ:↑(𝓛 d)⊢ toComplex Λ *ᵥ ⇑ofRealHom ∘ v = ⇑ofRealHom ∘ (↑Λ *ᵥ v)
  simp only [toComplex, MonoidHom.coe_mk, OneHom.coe_mk]d:ℕv:Fin 1 ⊕ Fin d → ℝΛ:↑(𝓛 d)⊢ (↑Λ).map ⇑ofRealHom *ᵥ ⇑ofRealHom ∘ v = ⇑ofRealHom ∘ (↑Λ *ᵥ v)
  funext id:ℕv:Fin 1 ⊕ Fin d → ℝΛ:↑(𝓛 d)i:Fin 1 ⊕ Fin d⊢ ((↑Λ).map ⇑ofRealHom *ᵥ ⇑ofRealHom ∘ v) i = (⇑ofRealHom ∘ (↑Λ *ᵥ v)) i
  rw [← RingHom.map_mulVecd:ℕv:Fin 1 ⊕ Fin d → ℝΛ:↑(𝓛 d)i:Fin 1 ⊕ Fin d⊢ ofRealHom ((↑Λ *ᵥ v) i) = (⇑ofRealHom ∘ (↑Λ *ᵥ v)) id:ℕv:Fin 1 ⊕ Fin d → ℝΛ:↑(𝓛 d)i:Fin 1 ⊕ Fin d⊢ ofRealHom ((↑Λ *ᵥ v) i) = (⇑ofRealHom ∘ (↑Λ *ᵥ v)) i]d:ℕv:Fin 1 ⊕ Fin d → ℝΛ:↑(𝓛 d)i:Fin 1 ⊕ Fin d⊢ ofRealHom ((↑Λ *ᵥ v) i) = (⇑ofRealHom ∘ (↑Λ *ᵥ v)) i
  rflAll goals completed! 🐙

The parity transformation.


def parity : LorentzGroup d := ⟨minkowskiMatrix, byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)⊢ η ∈ 𝓛 d
  rw [mem_iff_dual_mul_selfd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)⊢ dual η * η = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)⊢ dual η * η = 1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)⊢ dual η * η = 1
  simp only [dual_eta, minkowskiMatrix.sq]All goals completed! 🐙⟩

Equality conditions

lemma eq_of_mulVec_eq {Λ Λ' : LorentzGroup d}
    (h : ∀ (x : Fin 1 ⊕ Fin d → ℝ), Λ.1 *ᵥ x = Λ'.1 *ᵥ x) : Λ = Λ' := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:∀ (x : Fin 1 ⊕ Fin d → ℝ), ↑Λ *ᵥ x = ↑Λ' *ᵥ x⊢ Λ = Λ'
  apply Subtype.extd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:∀ (x : Fin 1 ⊕ Fin d → ℝ), ↑Λ *ᵥ x = ↑Λ' *ᵥ x⊢ ↑Λ = ↑Λ'
  exact ext_of_mulVec_single fun i => h (Pi.single i 1)All goals completed! 🐙