Physlib.Relativity.LorentzGroup.Restricted.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.Meta.Informal.SemiFormal
public import Physlib.Relativity.LorentzGroup.Orthochronous.Basic

The Restricted Lorentz Group

This file is currently a stub.

@[expose] public section

The restricted Lorentz group comprises the proper and orthochronous elements of the Lorentz group.


def restricted (d : ℕ) : Subgroup (LorentzGroup d) where
  carrier := { Λ : LorentzGroup d | IsProper Λ ∧ IsOrthochronous Λ }
  one_mem' := ⟨
    byd:ℕ⊢ IsProper 1 rw [IsProperd:ℕ⊢ (↑1).det = 1d:ℕ⊢ (↑1).det = 1]d:ℕ⊢ (↑1).det = 1; exact det_oneAll goals completed! 🐙,
    byd:ℕ⊢ IsOrthochronous 1 rw [IsOrthochronousd:ℕ⊢ 0 ≤ ↑1 (Sum.inl 0) (Sum.inl 0)d:ℕ⊢ 0 ≤ ↑1 (Sum.inl 0) (Sum.inl 0)]d:ℕ⊢ 0 ≤ ↑1 (Sum.inl 0) (Sum.inl 0); exact zero_le_oneAll goals completed! 🐙⟩
  mul_mem' := byd:ℕ⊢ ∀ {a b : ↑(𝓛 d)},
  a ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} →
    b ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} → a * b ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}
    rintro Λ₁ Λ₂ ⟨Λ₁_proper, Λ₁_ortho⟩ ⟨Λ₂_proper, Λ₂_ortho⟩d:ℕΛ₁:↑(𝓛 d)Λ₂:↑(𝓛 d)Λ₁_proper:IsProper Λ₁Λ₁_ortho:IsOrthochronous Λ₁Λ₂_proper:IsProper Λ₂Λ₂_ortho:IsOrthochronous Λ₂⊢ Λ₁ * Λ₂ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}
    exact ⟨
      byd:ℕΛ₁:↑(𝓛 d)Λ₂:↑(𝓛 d)Λ₁_proper:IsProper Λ₁Λ₁_ortho:IsOrthochronous Λ₁Λ₂_proper:IsProper Λ₂Λ₂_ortho:IsOrthochronous Λ₂⊢ IsProper (Λ₁ * Λ₂) exact isProper_mul Λ₁_proper Λ₂_properAll goals completed! 🐙,
      byd:ℕΛ₁:↑(𝓛 d)Λ₂:↑(𝓛 d)Λ₁_proper:IsProper Λ₁Λ₁_ortho:IsOrthochronous Λ₁Λ₂_proper:IsProper Λ₂Λ₂_ortho:IsOrthochronous Λ₂⊢ IsOrthochronous (Λ₁ * Λ₂) exact isOrthochronous_mul Λ₁_ortho Λ₂_orthoAll goals completed! 🐙⟩
  inv_mem' := byd:ℕ⊢ ∀ {x : ↑(𝓛 d)}, x ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} → x⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}
    rintro Λ ⟨Λ_proper, Λ_ortho⟩d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λ⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}

    have h_η₀₀ : @minkowskiMatrix d (Sum.inl 0) (Sum.inl 0) = 1 := byd:ℕ⊢ ∀ {x : ↑(𝓛 d)}, x ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} → x⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} rfld:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}
    have h_dual : (dual Λ.1) (Sum.inl 0) (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inl 0) := byd:ℕ⊢ ∀ {x : ↑(𝓛 d)}, x ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} → x⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}
      rw [dual_apply,d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1⊢ η (Sum.inl 0) (Sum.inl 0) * ↑Λ (Sum.inl 0) (Sum.inl 0) * η (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} h_η₀₀,d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1⊢ 1 * ↑Λ (Sum.inl 0) (Sum.inl 0) * 1 = ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} one_mul,d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) * 1 = ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ} mul_oned:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}]d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ Λ⁻¹ ∈ {Λ | IsProper Λ ∧ IsOrthochronous Λ}

    exact ⟨
      byd:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ IsProper Λ⁻¹ rw [IsProper,d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ (↑Λ⁻¹).det = 1All goals completed! 🐙 inv_eq_dual,d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ (↑⟨dual ↑Λ, ⋯⟩).det = 1All goals completed! 🐙 det_dual,d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ (↑Λ).det = 1All goals completed! 🐙 Λ_properd:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙,
      byd:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ IsOrthochronous Λ⁻¹ simp [IsOrthochronous, inv_eq_dual, h_dual]d:ℕΛ:↑(𝓛 d)Λ_proper:IsProper ΛΛ_ortho:IsOrthochronous Λh_η₀₀:η (Sum.inl 0) (Sum.inl 0) = 1h_dual:dual (↑Λ) (Sum.inl 0) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0); exact Λ_orthoAll goals completed! 🐙⟩

lemma isOrthochronous_of_restricted {d : ℕ} (Λ : restricted d) :
    IsOrthochronous Λ.1 := Λ.2.2

The restricted Lorentz group is a normal subgroup of the Lorentz group.


lemma restricted_normal_subgroup {d : ℕ} : (restricted d).Normal := byd:ℕ⊢ (restricted d).Normal
  have h_proper {Λ P : LorentzGroup d} (hP : IsProper P) : IsProper (Λ * P * Λ⁻¹) := by
    rw [isProper_iffd:ℕΛ:↑(𝓛 d)P:↑(𝓛 d)hP:detRep P = 1⊢ detRep (Λ * P * Λ⁻¹) = 1d:ℕΛ:↑(𝓛 d)P:↑(𝓛 d)hP:detRep P = 1⊢ detRep (Λ * P * Λ⁻¹) = 1d:ℕh_proper:∀ {Λ P : ↑(𝓛 d)}, IsProper P → IsProper (Λ * P * Λ⁻¹)⊢ (restricted d).Normal] at hP ⊢d:ℕΛ:↑(𝓛 d)P:↑(𝓛 d)hP:detRep P = 1⊢ detRep (Λ * P * Λ⁻¹) = 1d:ℕh_proper:∀ {Λ P : ↑(𝓛 d)}, IsProper P → IsProper (Λ * P * Λ⁻¹)⊢ (restricted d).Normal
    simp only [map_mul, map_inv, hP, mul_one, mul_inv_cancel]d:ℕh_proper:∀ {Λ P : ↑(𝓛 d)}, IsProper P → IsProper (Λ * P * Λ⁻¹)⊢ (restricted d).Normald:ℕh_proper:∀ {Λ P : ↑(𝓛 d)}, IsProper P → IsProper (Λ * P * Λ⁻¹)⊢ (restricted d).Normal
  have h_ortho {Λ O : LorentzGroup d} (hO : IsOrthochronous O) : IsOrthochronous (Λ * O * Λ⁻¹) := by
    simp [isOrthochronous_mul_iff, isOrthochronous_inv_iff, hO]d:ℕh_proper:∀ {Λ P : ↑(𝓛 d)}, IsProper P → IsProper (Λ * P * Λ⁻¹)h_ortho:∀ {Λ O : ↑(𝓛 d)}, IsOrthochronous O → IsOrthochronous (Λ * O * Λ⁻¹)⊢ (restricted d).Normald:ℕh_proper:∀ {Λ P : ↑(𝓛 d)}, IsProper P → IsProper (Λ * P * Λ⁻¹)h_ortho:∀ {Λ O : ↑(𝓛 d)}, IsOrthochronous O → IsOrthochronous (Λ * O * Λ⁻¹)⊢ (restricted d).Normal
  exact ⟨fun R hR Λ => ⟨h_proper hR.1, h_ortho hR.2⟩⟩All goals completed! 🐙

The restricted Lorentz group is connected.

semiformal_result "FXNL5" restricted_isConnected {d : ℕ} :
  IsConnected (restricted d : Set (LorentzGroup d))

Given the hypothesis that the restricted Lorentz group is connected, the proof that the restricted lorentz group is equal to the connected component of the identity.

lemma restricted_eq_identity_component_of_isConnected {d : ℕ}
    (h1 : IsConnected (restricted d : Set (LorentzGroup d))) :
    (restricted d) = connectedComponent (1 : LorentzGroup d) := byd:ℕh1:IsConnected ↑(restricted d)⊢ ↑(restricted d) = connectedComponent 1
  exact Set.Subset.antisymm (IsConnected.subset_connectedComponent h1 (restricted d).one_mem)
    fun x h => ⟨(isProper_on_connected_component h).mp isProper_id,
      (isOrthochronous_on_connected_component h).mp id_isOrthochronous⟩All goals completed! 🐙