The Orthochronous Lorentz Group

We define the give a series of lemmas related to the orthochronous property of lorentz matrices.

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

A Lorentz transformation is orthochronous if its 0 0 element is non-negative.

Equations

• LorentzGroup.IsOrthochronous Λ = (0 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0))

theorem LorentzGroup.IsOrthochronous_iff_futurePointing {d : ℕ} (Λ : ↑(LorentzGroup d)) : IsOrthochronous Λ ↔ toNormOne Λ ∈ Lorentz.Contr.NormOne.FuturePointing d

A Lorentz transformation is orthochronous if and only if its first column is future pointing.

theorem LorentzGroup.IsOrthochronous_iff_transpose {d : ℕ} (Λ : ↑(LorentzGroup d)) : IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ)

A Lorentz transformation is orthochronous if and only if its transpose is orthochronous.

theorem LorentzGroup.IsOrthochronous_iff_ge_one {d : ℕ} (Λ : ↑(LorentzGroup d)) : IsOrthochronous Λ ↔ 1 ≤ ↑Λ (Sum.inl 0) (Sum.inl 0)

A Lorentz transformation is orthochronous if and only if its 0 0 element is greater or equal to one.

theorem LorentzGroup.not_orthochronous_iff_le_neg_one {d : ℕ} (Λ : ↑(LorentzGroup d)) : ¬IsOrthochronous Λ ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ -1

A Lorentz transformation is not orthochronous if and only if its 0 0 element is less than or equal to minus one.

theorem LorentzGroup.not_orthochronous_iff_le_zero {d : ℕ} (Λ : ↑(LorentzGroup d)) : ¬IsOrthochronous Λ ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) ≤ 0

A Lorentz transformation is not orthochronous if and only if its 0 0 element is non-positive.

def LorentzGroup.timeCompCont {d : ℕ} : C(↑(LorentzGroup d), ℝ)

The continuous map taking a Lorentz transformation to its 0 0 element.

Equations

• LorentzGroup.timeCompCont = { toFun := fun (Λ : ↑(LorentzGroup d)) => ↑Λ (Sum.inl 0) (Sum.inl 0), continuous_toFun := ⋯ }

def LorentzGroup.stepFunction : ℝ → ℝ

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.

Equations

• LorentzGroup.stepFunction t = if t ≤ -1 then -1 else if 1 ≤ t then 1 else t

theorem LorentzGroup.stepFunction_continuous : Continuous stepFunction

The stepFunction is continuous.

def LorentzGroup.orthchroMapReal {d : ℕ} : C(↑(LorentzGroup d), ℝ)

The continuous map from lorentzGroup to ℝ wh taking Orthochronous elements to 1 and non-orthochronous to -1.

Equations

• LorentzGroup.orthchroMapReal = { toFun := LorentzGroup.stepFunction, continuous_toFun := LorentzGroup.stepFunction_continuous }.comp LorentzGroup.timeCompCont

theorem LorentzGroup.orthchroMapReal_on_IsOrthochronous {d : ℕ} {Λ : ↑(LorentzGroup d)} (h : IsOrthochronous Λ) : orthchroMapReal Λ = 1

A Lorentz transformation which is orthochronous maps under orthchroMapReal to 1.

theorem LorentzGroup.orthchroMapReal_on_not_IsOrthochronous {d : ℕ} {Λ : ↑(LorentzGroup d)} (h : ¬IsOrthochronous Λ) : orthchroMapReal Λ = -1

A Lorentz transformation which is not-orthochronous maps under orthchroMapReal to - 1.

theorem LorentzGroup.orthchroMapReal_minus_one_or_one {d : ℕ} (Λ : ↑(LorentzGroup d)) : orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1

Every Lorentz transformation maps under orthchroMapReal to either 1 or -1.

def LorentzGroup.orthchroMap {d : ℕ} : C(↑(LorentzGroup d), Multiplicative (ZMod 2))

A continuous map from lorentzGroup to ℤ₂ whose kernel are the Orthochronous elements.

Equations

• LorentzGroup.orthchroMap = LorentzGroup.coeForℤ₂.comp { toFun := fun (Λ : ↑(LorentzGroup d)) => ⟨LorentzGroup.orthchroMapReal Λ, ⋯⟩, continuous_toFun := ⋯ }

theorem LorentzGroup.orthchroMap_IsOrthochronous {d : ℕ} {Λ : ↑(LorentzGroup d)} (h : IsOrthochronous Λ) : orthchroMap Λ = 1

A Lorentz transformation which is orthochronous maps under orthchroMap to 1 in ℤ₂ (the identity element).

theorem LorentzGroup.orthchroMap_not_IsOrthochronous {d : ℕ} {Λ : ↑(LorentzGroup d)} (h : ¬IsOrthochronous Λ) : orthchroMap Λ = Additive.toMul 1

A Lorentz transformation which is not-orthochronous maps under orthchroMap to the non-identity element of ℤ₂.

theorem LorentzGroup.mul_othchron_of_othchron_othchron {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : IsOrthochronous Λ) (h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ')

The product of two orthochronous Lorentz transformations is orthochronous.

theorem LorentzGroup.mul_othchron_of_not_othchron_not_othchron {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : ¬IsOrthochronous Λ) (h' : ¬IsOrthochronous Λ') : IsOrthochronous (Λ * Λ')

The product of two non-orthochronous Lorentz transformations is orthochronous.

theorem LorentzGroup.mul_not_othchron_of_othchron_not_othchron {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : IsOrthochronous Λ) (h' : ¬IsOrthochronous Λ') : ¬IsOrthochronous (Λ * Λ')

The product of an orthochronous Lorentz transformations with a non-orthochronous Lorentz transformation is not orthochronous.

theorem LorentzGroup.mul_not_othchron_of_not_othchron_othchron {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : ¬IsOrthochronous Λ) (h' : IsOrthochronous Λ') : ¬IsOrthochronous (Λ * Λ')

The product of a non-orthochronous Lorentz transformations with an orthochronous Lorentz transformation is not orthochronous.

def LorentzGroup.orthchroRep {d : ℕ} : ↑(LorentzGroup d) →* Multiplicative (ZMod 2)

The homomorphism from LorentzGroup to ℤ₂ whose kernel are the Orthochronous elements.

Equations

• LorentzGroup.orthchroRep = { toFun := ⇑LorentzGroup.orthchroMap, map_one' := ⋯, map_mul' := ⋯ }