The Proper Lorentz Group

The proper Lorentz group is the subgroup of the Lorentz group with determinant 1.

We define the give a series of lemmas related to the determinant of the Lorentz group.

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

The determinant of a member of the Lorentz group is 1 or -1.

instance LorentzGroup.instTopologicalSpaceMultiplicativeZModOfNatNat : TopologicalSpace (Multiplicative (ZMod 2))

The instance of a topological space on ℤ₂ corresponding to the discrete topology.

Equations

• LorentzGroup.instTopologicalSpaceMultiplicativeZModOfNatNat = instTopologicalSpaceFin

instance LorentzGroup.instDiscreteTopologyMultiplicativeZModOfNatNat : DiscreteTopology (Multiplicative (ZMod 2))

The topological space defined by ℤ₂ is discrete.

instance LorentzGroup.instIsTopologicalGroupMultiplicativeZModOfNatNat : IsTopologicalGroup (Multiplicative (ZMod 2))

The instance of a topological group on ℤ₂ defined via the discrete topology.

def LorentzGroup.coeForℤ₂ : C(↑{-1, 1}, Multiplicative (ZMod 2))

A continuous function from ({-1, 1} : Set ℝ) to ℤ₂.

Equations

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

@[simp]

theorem LorentzGroup.coeForℤ₂_apply (x : ↑{-1, 1}) : coeForℤ₂ x = if x = ⟨1, coeForℤ₂.proof_1⟩ then 1 else Additive.toMul 1

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

The continuous map taking a Lorentz matrix to its determinant.

Equations

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

theorem LorentzGroup.detContinuous_eq_one {d : ℕ} (Λ : ↑(LorentzGroup d)) : detContinuous Λ = Additive.toMul 0 ↔ (↑Λ).det = 1

theorem LorentzGroup.detContinuous_eq_zero {d : ℕ} (Λ : ↑(LorentzGroup d)) : detContinuous Λ = Additive.toMul 1 ↔ (↑Λ).det = -1

theorem LorentzGroup.detContinuous_eq_iff_det_eq {d : ℕ} (Λ Λ' : ↑(LorentzGroup d)) : detContinuous Λ = detContinuous Λ' ↔ (↑Λ).det = (↑Λ').det

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

The representation taking a Lorentz matrix to its determinant.

Equations

• LorentzGroup.detRep = { toFun := fun (Λ : ↑(LorentzGroup d)) => LorentzGroup.detContinuous Λ, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem LorentzGroup.detRep_apply {d : ℕ} (Λ : ↑(LorentzGroup d)) : detRep Λ = detContinuous Λ

theorem LorentzGroup.detRep_continuous {d : ℕ} : Continuous ⇑detRep

The representation of the Lorentz group defined by taking the determinant detRep is continuous.

theorem LorentzGroup.det_on_connected_component {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : Λ' ∈ connectedComponent Λ) : (↑Λ).det = (↑Λ').det

Two Lorentz transformations which are in the same connected component have the same determinant.

theorem LorentzGroup.detRep_on_connected_component {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : Λ' ∈ connectedComponent Λ) : detRep Λ = detRep Λ'

Two Lorentz transformations which are in the same connected component have the same image under detRep, the determinant representation.

theorem LorentzGroup.det_of_joined {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : Joined Λ Λ') : (↑Λ).det = (↑Λ').det

Two Lorentz transformations which are joined by a path have the same determinant.

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

A Lorentz Matrix is proper if its determinant is 1.

Equations

• LorentzGroup.IsProper Λ = ((↑Λ).det = 1)

instance LorentzGroup.instDecidablePredElemMatrixSumFinOfNatNatRealIsProper {d : ℕ} : DecidablePred IsProper

The predicate IsProper is decidable.

Equations

• LorentzGroup.instDecidablePredElemMatrixSumFinOfNatNatRealIsProper Λ = (↑Λ).det.decidableEq 1

theorem LorentzGroup.IsProper_iff {d : ℕ} (Λ : ↑(LorentzGroup d)) : IsProper Λ ↔ detRep Λ = 1

A Lorentz transformation is proper if it's image under the det-representation detRep is 1.

theorem LorentzGroup.id_IsProper {d : ℕ} : IsProper 1

The identity Lorentz transformation is proper.

theorem LorentzGroup.isProper_on_connected_component {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : Λ' ∈ connectedComponent Λ) : IsProper Λ ↔ IsProper Λ'

If two Lorentz transformations are in the same connected component, and one is proper then the other is also proper.