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.LorentzGroup.Proper
public import Physlib.Relativity.LorentzGroup.ToVector
public import Physlib.Relativity.Tensors.RealTensor.Velocity.BasicThe Orthochronous Lorentz Group
We define the give a series of lemmas related to the orthochronous property of lorentz matrices.
@[expose] public sectionTODO "Prove topological properties of the Orthochronous Lorentz Group."
A Lorentz transformation is orthochronous if its 0 0 element is non-negative.
def IsOrthochronous : Prop := 0 ≤ Λ.1 (Sum.inl 0) (Sum.inl 0)
A Lorentz transformation is orthochronous if and only if its first column is
future pointing.
lemma isOrthochronous_iff_toVector_timeComponet_nonneg :
IsOrthochronous Λ ↔ 0 ≤ (toVector Λ).timeComponent := d:ℕΛ:↑(𝓛 d)⊢ IsOrthochronous Λ ↔ 0 ≤ (toVector Λ).timeComponent
All goals completed! 🐙A Lorentz transformation is orthochronous if and only if its transpose is orthochronous.
lemma isOrthochronous_iff_transpose :
IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := d:ℕΛ:↑(𝓛 d)⊢ IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) All goals completed! 🐙@[simp]
lemma isOrthochronous_inv_iff {Λ : LorentzGroup d} :
IsOrthochronous Λ⁻¹ ↔ IsOrthochronous Λ := d:ℕΛ:↑(𝓛 d)⊢ IsOrthochronous Λ⁻¹ ↔ IsOrthochronous Λ
All goals completed! 🐙
A Lorentz transformation is orthochronous if and only if its 0 0 element is greater
or equal to one.
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ IsOrthochronous Λ ↔ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) ↔ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) → 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) → 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) → 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) → 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) d:ℕΛ:↑(𝓛 d)h:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)h:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) d:ℕΛ:↑(𝓛 d)h:0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)h:0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)h:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)d:ℕΛ:↑(𝓛 d)h:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) All goals completed! 🐙
The Lorentz.Velocity from Lorentz.toVector of a orthochronous lorentz
transformation.
d:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)h:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ toVector Λ ∈ Lorentz.Velocity d
d:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)h:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 < ↑Λ (Sum.inl 0) (Sum.inl 0)
All goals completed! 🐙⟩
A Lorentz transformation is not orthochronous if and only if its 0 0 element is less than
or equal to minus one.
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ¬IsOrthochronous Λ ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 → ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 → ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 → ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 → ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:↑Λ (Sum.inl 0) (Sum.inl 0) < 0⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) < 0h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) < 0h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 All goals completed! 🐙d:ℕΛ:↑(𝓛 d)⊢ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0) ↔ ↑(-Λ) (Sum.inl 0) (Sum.inl 0) ≤ -1
All goals completed! 🐙lemma neg_isOrthochronous_iff_not {Λ : LorentzGroup d} :
IsOrthochronous (- Λ) ↔ ¬ IsOrthochronous Λ := d:ℕΛ:↑(𝓛 d)⊢ IsOrthochronous (-Λ) ↔ ¬IsOrthochronous Λ
conv_rhs => d:ℕΛ:↑(𝓛 d)| ¬¬IsOrthochronous (-Λ)
All goals completed! 🐙
A Lorentz transformation is not orthochronous if and only if its 0 0 element is
non-positive.
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ¬IsOrthochronous Λ ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0
d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 → ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0 → ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 → ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0 → ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:↑Λ (Sum.inl 0) (Sum.inl 0) < 0⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0d:ℕΛ:↑(𝓛 d)h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1 ∨ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) < 0h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) < 0h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0h1:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0d:ℕΛ:↑(𝓛 d)h:↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0h1:1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) < 0 All goals completed! 🐙d:ℕΛ:↑(𝓛 d)⊢ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0 ↔ (toVector Λ).timeComponent ≤ 0
All goals completed! 🐙The identity Lorentz transformation is orthochronous.
lemma id_isOrthochronous : @IsOrthochronous d 1 := d:ℕ⊢ IsOrthochronous 1
All goals completed! 🐙
The continuous map taking a Lorentz transformation to its 0 0 element.
def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => Λ.1 (Sum.inl 0) (Sum.inl 0),
Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩
An auxiliary function used in the definition of orthchroMapReal.
This function takes all elements of ℝ less than -1 to -1,
all elements of R greater than 1 to 1 and preserves all other elements.
def stepFunction : ℝ → ℝ := fun t =>
if t ≤ -1 then -1 else
if 1 ≤ t then 1 else t
The stepFunction is continuous.
a:ℝha:a = 1⊢ 1 = id a
All goals completed! 🐙
The continuous map from lorentzGroup to ℝ wh
taking Orthochronous elements to 1 and non-orthochronous to -1.
def orthchroMapReal : C(LorentzGroup d, ℝ) := ContinuousMap.comp
⟨stepFunction, stepFunction_continuous⟩ timeCompCont
A Lorentz transformation which is orthochronous maps under orthchroMapReal to 1.
All goals completed! 🐙
A Lorentz transformation which is not-orthochronous maps under orthchroMapReal to - 1.
All goals completed! 🐙
Every Lorentz transformation maps under orthchroMapReal to either 1 or -1.
lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup d) :
orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 := d:ℕΛ:↑(𝓛 d)⊢ orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1
d:ℕΛ:↑(𝓛 d)h:IsOrthochronous Λ⊢ orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1d:ℕΛ:↑(𝓛 d)h:¬IsOrthochronous Λ⊢ orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1
d:ℕΛ:↑(𝓛 d)h:IsOrthochronous Λ⊢ orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 All goals completed! 🐙
d:ℕΛ:↑(𝓛 d)h:¬IsOrthochronous Λ⊢ orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 All goals completed! 🐙local notation "ℤ₂" => Multiplicative (ZMod 2)
A continuous map from lorentzGroup to ℤ₂ whose kernel are the Orthochronous elements.
def orthchroMap : C(LorentzGroup d, ℤ₂) :=
ContinuousMap.comp coeForℤ₂ {
toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
continuous_toFun := Continuous.subtype_mk (ContinuousMap.continuous orthchroMapReal) _}
A Lorentz transformation which is orthochronous maps under orthchroMap to 1
in ℤ₂ (the identity element).
lemma orthchroMap_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ) :
orthchroMap Λ = 1 := d:ℕΛ:↑(𝓛 d)h:IsOrthochronous Λ⊢ orthchroMap Λ = 1
All goals completed! 🐙
A Lorentz transformation which is not-orthochronous maps under orthchroMap to
the non-identity element of ℤ₂.
d:ℕΛ:↑(𝓛 d)h:¬IsOrthochronous Λ⊢ Additive.toMul 1 = Additive.toMul 1
All goals completed! 🐙The product of two orthochronous Lorentz transformations is orthochronous.
d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsOrthochronous Λh':IsOrthochronous Λ'⊢ 0 ≤ (minkowskiProduct (toVector Λ⁻¹)) (toVector Λ')
d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsOrthochronous Λh':IsOrthochronous Λ'⊢ 0 ≤ (minkowskiProduct ↑(orthochronoustoVelocity ⋯)) ↑(orthochronoustoVelocity h')
All goals completed! 🐙d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'hnn:-Λ * -Λ' = Λ * Λ'⊢ IsOrthochronous (-Λ * -Λ')
d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'hnn:-Λ * -Λ' = Λ * Λ'⊢ IsOrthochronous (-Λ)d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'hnn:-Λ * -Λ' = Λ * Λ'⊢ IsOrthochronous (-Λ') d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'hnn:-Λ * -Λ' = Λ * Λ'⊢ IsOrthochronous (-Λ)d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'hnn:-Λ * -Λ' = Λ * Λ'⊢ IsOrthochronous (-Λ') rwa [d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'hnn:-Λ * -Λ' = Λ * Λ'⊢ ¬IsOrthochronous Λd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'hnn:-Λ * -Λ' = Λ * Λ'⊢ ¬IsOrthochronous Λ'
The homomorphism from LorentzGroup to ℤ₂.
def orthchroRep : LorentzGroup d →* ℤ₂ where
toFun := orthchroMap
map_one' := orthchroMap_IsOrthochronous (d:ℕΛ:↑(𝓛 d)⊢ IsOrthochronous 1 All goals completed! 🐙)
map_mul' Λ Λ' := d:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ'
d:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsOrthochronous Λ⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ'd:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λ⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ' d:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsOrthochronous Λ⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ'd:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λ⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ' d:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':IsOrthochronous Λ'⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ'd:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ' d:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsOrthochronous Λh':IsOrthochronous Λ'⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ'd:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsOrthochronous Λh':¬IsOrthochronous Λ'⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ'd:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':IsOrthochronous Λ'⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ'd:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'⊢ orthchroMap (Λ * Λ') = orthchroMap Λ * orthchroMap Λ'
d:ℕΛ✝:↑(𝓛 d)Λ:↑(𝓛 d)Λ':↑(𝓛 d)h:¬IsOrthochronous Λh':¬IsOrthochronous Λ'⊢ 1 = Additive.toMul 1 * Additive.toMul 1
All goals completed! 🐙
The orthochronous Lorentz transformations form the kernel of the homomorphism from
LorentzGroup to ℤ₂.
set_option backward.isDefEq.respectTransparency false ind:ℕΛ:↑(𝓛 d)h:orthchroRep Λ = Additive.toMul 1⊢ ¬Additive.toMul 1 = 1
All goals completed! 🐙
The homomorphism from LorentzGroup to ℤ₂ assigns the same value to any Lorentz
transformation and its inverse.
d:ℕΛ:↑(𝓛 d)⊢ orthchroRep Λ = (orthchroRep Λ)⁻¹
d:ℕΛ:↑(𝓛 d)x:ℤ₂⊢ x = x⁻¹
d:ℕΛ:↑(𝓛 d)⊢ ∀ (x : ℤ₂), x = x⁻¹
All goals completed! 🐙
Two Lorentz transformations are both orthochronous or both not orthochronous if they are mapped
to the same element via the homomorphism from LorentzGroup to ℤ₂.
All goals completed! 🐙Two Lorentz transformations which are in the same connected component are either both orthochronous or both not orthochronous.
d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)s:Set ↑(𝓛 d)hs:s ∈ {s | IsPreconnected s ∧ Λ ∈ s}hΛ':Λ' ∈ sf:C(↑s, ℤ₂) := ContinuousMap.restrict s orthchroMapthis:PreconnectedSpace ↑sh_eq:orthchroMap Λ = orthchroMap Λ'⊢ IsOrthochronous Λ ↔ IsOrthochronous Λ'
All goals completed! 🐙