Physlib.Relativity.LorentzGroup.Proper

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.Basic
public import Mathlib.Topology.Connected.PathConnected
public import Mathlib.Tactic.Cases

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.

@[expose] public section

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

lemma det_eq_one_or_neg_one (Λ : 𝓛 d) : Λ.1.det = 1 ∨ Λ.1.det = -1 := byd:ℕΛ:↑(𝓛 d)⊢ (↑Λ).det = 1 ∨ (↑Λ).det = -1
  refine mul_self_eq_one_iff.mp ?_d:ℕΛ:↑(𝓛 d)⊢ (↑Λ).det * (↑Λ).det = 1
  simpa only [det_mul, det_dual, det_one] using congrArg det ((mem_iff_self_mul_dual).mp Λ.2)All goals completed! 🐙

The group ℤ₂.

local notation "ℤ₂" => Multiplicative (ZMod 2)

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

instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin

The topological space defined by ℤ₂ is discrete.

instance : DiscreteTopology ℤ₂ := byd:ℕ⊢ DiscreteTopology ℤ₂
  exact discreteTopology_iff_forall_isOpen.mpr fun _ => trivialAll goals completed! 🐙

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

instance : IsTopologicalGroup ℤ₂ := IsTopologicalGroup.mk

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

@[simps!]
def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where
  toFun x := if x = ⟨1, Set.mem_insert_of_mem (-1) rfl⟩
    then Additive.toMul 0 else Additive.toMul (1 : ZMod 2)
  continuous_toFun := continuous_of_discreteTopology

The continuous map taking a Lorentz matrix to its determinant.

def detContinuous : C(𝓛 d, ℤ₂) :=
  ContinuousMap.comp coeForℤ₂ {
    toFun := fun Λ => ⟨Λ.1.det, Or.symm (LorentzGroup.det_eq_one_or_neg_one _)⟩,
    continuous_toFun := byd:ℕ⊢ Continuous fun Λ => ⟨(↑Λ).det, ⋯⟩
      refine Continuous.subtype_mk ?_ _d:ℕ⊢ Continuous fun Λ => (↑Λ).det
      exact Continuous.matrix_det $
        Continuous.comp' (continuous_iff_le_induced.mpr fun U a => a) continuous_id'All goals completed! 🐙
      }

              lemma detContinuous_eq_one (Λ : LorentzGroup d) :
    detContinuous Λ = Additive.toMul 0 ↔ Λ.1.det = 1 := byd:ℕΛ:↑(𝓛 d)⊢ detContinuous Λ = Additive.toMul 0 ↔ (↑Λ).det = 1
  simp only [detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk, coeForℤ₂_apply,
    Subtype.mk.injEq]d:ℕΛ:↑(𝓛 d)⊢ (if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 0 ↔ (↑Λ).det = 1
  simp only [toMul_zero, ite_eq_left_iff, toMul_eq_one]d:ℕΛ:↑(𝓛 d)⊢ ¬(↑Λ).det = 1 → 1 = 0 ↔ (↑Λ).det = 1
  refine Iff.intro (fun h => ?_) (fun h => ?_)refine_1d:ℕΛ:↑(𝓛 d)h:¬(↑Λ).det = 1 → 1 = 0⊢ (↑Λ).det = 1refine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = 1⊢ ¬(↑Λ).det = 1 → 1 = 0
  ·refine_1d:ℕΛ:↑(𝓛 d)h:¬(↑Λ).det = 1 → 1 = 0⊢ (↑Λ).det = 1 by_contra hnrefine_1d:ℕΛ:↑(𝓛 d)h:¬(↑Λ).det = 1 → 1 = 0hn:¬(↑Λ).det = 1⊢ False
    have h' := h hnrefine_1d:ℕΛ:↑(𝓛 d)h:¬(↑Λ).det = 1 → 1 = 0hn:¬(↑Λ).det = 1h':1 = 0⊢ False
    change (1 : Fin 2) = (0 : Fin 2) at h'refine_1d:ℕΛ:↑(𝓛 d)h:¬(↑Λ).det = 1 → 1 = 0hn:¬(↑Λ).det = 1h':1 = 0⊢ False
    simp only [Fin.isValue, one_ne_zero] at h'All goals completed! 🐙
  ·refine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = 1⊢ ¬(↑Λ).det = 1 → 1 = 0 intro h'refine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = 1h':¬(↑Λ).det = 1⊢ 1 = 0
    exact False.elim (h' h)All goals completed! 🐙

lemma detContinuous_eq_zero (Λ : LorentzGroup d) :
    detContinuous Λ = Additive.toMul (1 : ZMod 2) ↔ Λ.1.det = - 1 := byd:ℕΛ:↑(𝓛 d)⊢ detContinuous Λ = Additive.toMul 1 ↔ (↑Λ).det = -1
  simp only [detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk, coeForℤ₂_apply,
    Subtype.mk.injEq, Nat.reduceAdd]d:ℕΛ:↑(𝓛 d)⊢ (if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1 ↔ (↑Λ).det = -1
  refine Iff.intro (fun h => ?_) (fun h => ?_)refine_1d:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1⊢ (↑Λ).det = -1refine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ (if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1
  ·refine_1d:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1⊢ (↑Λ).det = -1 by_contra hnrefine_1d:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ False
    rw [if_posrefine_1d:ℕΛ:↑(𝓛 d)h:1 = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ Falserefine_1.hcd:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ (↑Λ).det = 1refine_1d:ℕΛ:↑(𝓛 d)h:1 = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ Falserefine_1.hcd:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ (↑Λ).det = 1] at hrefine_1d:ℕΛ:↑(𝓛 d)h:1 = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ Falserefine_1.hcd:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ (↑Λ).det = 1
    ·refine_1d:ℕΛ:↑(𝓛 d)h:1 = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ False change (0 : Fin 2) = (1 : Fin 2) at hrefine_1d:ℕΛ:↑(𝓛 d)hn:¬(↑Λ).det = -1h:0 = 1⊢ False
      simp only [Fin.isValue, zero_ne_one] at hAll goals completed! 🐙
    ·refine_1.hcd:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1⊢ (↑Λ).det = 1 cases' det_eq_one_or_neg_one Λ with h2 h2refine_1.hc.inld:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1h2:(↑Λ).det = 1⊢ (↑Λ).det = 1refine_1.hc.inrd:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1h2:(↑Λ).det = -1⊢ (↑Λ).det = 1
      ·refine_1.hc.inld:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1h2:(↑Λ).det = 1⊢ (↑Λ).det = 1 simp_all only [ite_true]All goals completed! 🐙
      ·refine_1.hc.inrd:ℕΛ:↑(𝓛 d)h:(if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1hn:¬(↑Λ).det = -1h2:(↑Λ).det = -1⊢ (↑Λ).det = 1 simp_all only [not_true_eq_false]All goals completed! 🐙
  ·refine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ (if (↑Λ).det = 1 then 1 else Additive.toMul 1) = Additive.toMul 1 rw [if_negrefine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ Additive.toMul 1 = Additive.toMul 1refine_2.hncd:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ ¬(↑Λ).det = 1refine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ Additive.toMul 1 = Additive.toMul 1refine_2.hncd:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ ¬(↑Λ).det = 1]refine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ Additive.toMul 1 = Additive.toMul 1refine_2.hncd:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ ¬(↑Λ).det = 1
    ·refine_2d:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ Additive.toMul 1 = Additive.toMul 1 rflAll goals completed! 🐙
    ·refine_2.hncd:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1⊢ ¬(↑Λ).det = 1 cases' det_eq_one_or_neg_one Λ with h2 h2refine_2.hnc.inld:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1h2:(↑Λ).det = 1⊢ ¬(↑Λ).det = 1refine_2.hnc.inrd:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1h2:(↑Λ).det = -1⊢ ¬(↑Λ).det = 1
      ·refine_2.hnc.inld:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1h2:(↑Λ).det = 1⊢ ¬(↑Λ).det = 1 rw [hrefine_2.hnc.inld:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1h2:(↑Λ).det = 1⊢ ¬-1 = 1refine_2.hnc.inld:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1h2:(↑Λ).det = 1⊢ ¬-1 = 1]refine_2.hnc.inld:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1h2:(↑Λ).det = 1⊢ ¬-1 = 1
        linarithAll goals completed! 🐙
      ·refine_2.hnc.inrd:ℕΛ:↑(𝓛 d)h:(↑Λ).det = -1h2:(↑Λ).det = -1⊢ ¬(↑Λ).det = 1 linarithAll goals completed! 🐙

lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
    detContinuous Λ = detContinuous Λ' ↔ Λ.1.det = Λ'.1.det := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)⊢ detContinuous Λ = detContinuous Λ' ↔ (↑Λ).det = (↑Λ').det
  match det_eq_one_or_neg_one Λ, det_eq_one_or_neg_one Λ' with
  | .inl h1, .inl h2 =>d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ detContinuous Λ = detContinuous Λ' ↔ (↑Λ).det = (↑Λ').det
    rw [h1,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ detContinuous Λ = detContinuous Λ' ↔ 1 = (↑Λ').detd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ Additive.toMul 0 = Additive.toMul 0 ↔ 1 = 1 h2,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ detContinuous Λ = detContinuous Λ' ↔ 1 = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ Additive.toMul 0 = Additive.toMul 0 ↔ 1 = 1 (detContinuous_eq_one Λ).mpr h1,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ Additive.toMul 0 = detContinuous Λ' ↔ 1 = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ Additive.toMul 0 = Additive.toMul 0 ↔ 1 = 1 (detContinuous_eq_one Λ').mpr h2d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ Additive.toMul 0 = Additive.toMul 0 ↔ 1 = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ Additive.toMul 0 = Additive.toMul 0 ↔ 1 = 1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = 1⊢ Additive.toMul 0 = Additive.toMul 0 ↔ 1 = 1
    simp only [toMul_zero]All goals completed! 🐙
  | .inr h1, .inr h2 =>d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ detContinuous Λ = detContinuous Λ' ↔ (↑Λ).det = (↑Λ').det
    rw [h1,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ detContinuous Λ = detContinuous Λ' ↔ -1 = (↑Λ').detd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ Additive.toMul 1 = Additive.toMul 1 ↔ -1 = -1 h2,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ detContinuous Λ = detContinuous Λ' ↔ -1 = -1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ Additive.toMul 1 = Additive.toMul 1 ↔ -1 = -1 (detContinuous_eq_zero Λ).mpr h1,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ Additive.toMul 1 = detContinuous Λ' ↔ -1 = -1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ Additive.toMul 1 = Additive.toMul 1 ↔ -1 = -1 (detContinuous_eq_zero Λ').mpr h2d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ Additive.toMul 1 = Additive.toMul 1 ↔ -1 = -1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ Additive.toMul 1 = Additive.toMul 1 ↔ -1 = -1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = -1⊢ Additive.toMul 1 = Additive.toMul 1 ↔ -1 = -1
    simp only [Nat.reduceAdd]All goals completed! 🐙
  | .inl h1, .inr h2 =>d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ detContinuous Λ = detContinuous Λ' ↔ (↑Λ).det = (↑Λ').det
    rw [h1,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ detContinuous Λ = detContinuous Λ' ↔ 1 = (↑Λ').detd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ Additive.toMul 0 = Additive.toMul 1 ↔ 1 = -1 h2,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ detContinuous Λ = detContinuous Λ' ↔ 1 = -1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ Additive.toMul 0 = Additive.toMul 1 ↔ 1 = -1 (detContinuous_eq_one Λ).mpr h1,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ Additive.toMul 0 = detContinuous Λ' ↔ 1 = -1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ Additive.toMul 0 = Additive.toMul 1 ↔ 1 = -1 (detContinuous_eq_zero Λ').mpr h2d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ Additive.toMul 0 = Additive.toMul 1 ↔ 1 = -1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ Additive.toMul 0 = Additive.toMul 1 ↔ 1 = -1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ Additive.toMul 0 = Additive.toMul 1 ↔ 1 = -1
    change (0 : Fin 2) = (1 : Fin 2) ↔ _d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ 0 = 1 ↔ 1 = -1
    simp only [zero_ne_one, false_iff]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = 1h2:(↑Λ').det = -1⊢ ¬1 = -1
    linarithAll goals completed! 🐙
  | .inr h1, .inl h2 =>d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ detContinuous Λ = detContinuous Λ' ↔ (↑Λ).det = (↑Λ').det
    rw [h1,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ detContinuous Λ = detContinuous Λ' ↔ -1 = (↑Λ').detd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ Additive.toMul 1 = Additive.toMul 0 ↔ -1 = 1 h2,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ detContinuous Λ = detContinuous Λ' ↔ -1 = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ Additive.toMul 1 = Additive.toMul 0 ↔ -1 = 1 (detContinuous_eq_zero Λ).mpr h1,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ Additive.toMul 1 = detContinuous Λ' ↔ -1 = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ Additive.toMul 1 = Additive.toMul 0 ↔ -1 = 1 (detContinuous_eq_one Λ').mpr h2d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ Additive.toMul 1 = Additive.toMul 0 ↔ -1 = 1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ Additive.toMul 1 = Additive.toMul 0 ↔ -1 = 1]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ Additive.toMul 1 = Additive.toMul 0 ↔ -1 = 1
    change (1 : Fin 2) = (0 : Fin 2) ↔ _d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ 1 = 0 ↔ -1 = 1
    simp only [one_ne_zero, false_iff]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h1:(↑Λ).det = -1h2:(↑Λ').det = 1⊢ ¬-1 = 1
    linarithAll goals completed! 🐙

The representation taking a Lorentz matrix to its determinant.


@[simps!]
def detRep : 𝓛 d →* ℤ₂ where
  toFun Λ := detContinuous Λ
  map_one' := byd:ℕ⊢ detContinuous 1 = 1
    simp only [detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
      lorentzGroupIsGroup_one_coe, det_one, coeForℤ₂_apply, ↓reduceIte]All goals completed! 🐙
  map_mul' Λ1 Λ2 := byd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)⊢ detContinuous (Λ1 * Λ2) = detContinuous Λ1 * detContinuous Λ2
    cases' det_eq_one_or_neg_one Λ1 with h1 h1inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1⊢ detContinuous (Λ1 * Λ2) = detContinuous Λ1 * detContinuous Λ2inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1⊢ detContinuous (Λ1 * Λ2) = detContinuous Λ1 * detContinuous Λ2
    ·inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1⊢ detContinuous (Λ1 * Λ2) = detContinuous Λ1 * detContinuous Λ2 rw [(detContinuous_eq_one Λ1).mpr h1inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * detContinuous Λ2inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * detContinuous Λ2]inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * detContinuous Λ2
      cases' det_eq_one_or_neg_one Λ2 with h2 h2inl.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * detContinuous Λ2inl.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * detContinuous Λ2
      ·inl.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * detContinuous Λ2 rw [(detContinuous_eq_one Λ2).mpr h2inl.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * Additive.toMul 0inl.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * Additive.toMul 0]inl.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * Additive.toMul 0
        apply (detContinuous_eq_one _).mprinl.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = 1⊢ (↑(Λ1 * Λ2)).det = 1
        simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_one]All goals completed! 🐙
      ·inl.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * detContinuous Λ2 rw [(detContinuous_eq_zero Λ2).mpr h2inl.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * Additive.toMul 1inl.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * Additive.toMul 1]inl.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 0 * Additive.toMul 1
        apply (detContinuous_eq_zero _).mprinl.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = 1h2:(↑Λ2).det = -1⊢ (↑(Λ1 * Λ2)).det = -1
        simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_neg, mul_one]All goals completed! 🐙
    ·inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1⊢ detContinuous (Λ1 * Λ2) = detContinuous Λ1 * detContinuous Λ2 rw [(detContinuous_eq_zero Λ1).mpr h1inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * detContinuous Λ2inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * detContinuous Λ2]inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * detContinuous Λ2
      cases' det_eq_one_or_neg_one Λ2 with h2 h2inr.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * detContinuous Λ2inr.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * detContinuous Λ2
      ·inr.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * detContinuous Λ2 rw [(detContinuous_eq_one Λ2).mpr h2inr.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * Additive.toMul 0inr.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * Additive.toMul 0]inr.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = 1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * Additive.toMul 0
        apply (detContinuous_eq_zero _).mprinr.inld:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = 1⊢ (↑(Λ1 * Λ2)).det = -1
        simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_one]All goals completed! 🐙
      ·inr.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * detContinuous Λ2 rw [(detContinuous_eq_zero Λ2).mpr h2inr.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * Additive.toMul 1inr.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * Additive.toMul 1]inr.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = -1⊢ detContinuous (Λ1 * Λ2) = Additive.toMul 1 * Additive.toMul 1
        apply (detContinuous_eq_one _).mprinr.inrd:ℕΛ1:↑(𝓛 d)Λ2:↑(𝓛 d)h1:(↑Λ1).det = -1h2:(↑Λ2).det = -1⊢ (↑(Λ1 * Λ2)).det = 1
        simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_neg, mul_one, neg_neg]All goals completed! 🐙

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

lemma detRep_continuous : Continuous (@detRep d) := detContinuous.2

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

lemma det_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
    Λ.1.det = Λ'.1.det := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:Λ' ∈ connectedComponent Λ⊢ (↑Λ).det = (↑Λ').det
  obtain ⟨s, hs, hΛ'⟩ := hd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)s:Set ↑(𝓛 d)hs:s ∈ {s | IsPreconnected s ∧ Λ ∈ s}hΛ':Λ' ∈ s⊢ (↑Λ).det = (↑Λ').det
  let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s detContinuousd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)s:Set ↑(𝓛 d)hs:s ∈ {s | IsPreconnected s ∧ Λ ∈ s}hΛ':Λ' ∈ sf:C(↑s, ℤ₂) := ContinuousMap.restrict s detContinuous⊢ (↑Λ).det = (↑Λ').det
  haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)s:Set ↑(𝓛 d)hs:s ∈ {s | IsPreconnected s ∧ Λ ∈ s}hΛ':Λ' ∈ sf:C(↑s, ℤ₂) := ContinuousMap.restrict s detContinuousthis:PreconnectedSpace ↑s⊢ (↑Λ).det = (↑Λ').det
  simpa [f, detContinuous_eq_iff_det_eq] using
    (@IsPreconnected.subsingleton ℤ₂ _ _ _ (isPreconnected_range f.2))
    (Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩)All goals completed! 🐙

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


lemma detRep_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
    detRep Λ = detRep Λ' := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:Λ' ∈ connectedComponent Λ⊢ detRep Λ = detRep Λ'
  simp only [detRep_apply, detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
    coeForℤ₂_apply, Subtype.mk.injEq]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:Λ' ∈ connectedComponent Λ⊢ (if (↑Λ).det = 1 then 1 else Additive.toMul 1) = if (↑Λ').det = 1 then 1 else Additive.toMul 1
  rw [det_on_connected_component hd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:Λ' ∈ connectedComponent Λ⊢ (if (↑Λ').det = 1 then 1 else Additive.toMul 1) = if (↑Λ').det = 1 then 1 else Additive.toMul 1All goals completed! 🐙]All goals completed! 🐙

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

lemma det_of_joined {Λ Λ' : LorentzGroup d} (h : Joined Λ Λ') : Λ.1.det = Λ'.1.det :=
  det_on_connected_component $ pathComponent_subset_component _ h

A Lorentz Matrix is proper if its determinant is 1.

@[simp]
def IsProper (Λ : LorentzGroup d) : Prop := Λ.1.det = 1

The predicate IsProper is decidable.

instance : DecidablePred (@IsProper d) := byd:ℕ⊢ DecidablePred IsProper
  intro Λd:ℕΛ:↑(𝓛 d)⊢ Decidable (IsProper Λ)
  apply Real.decidableEqAll goals completed! 🐙

The product of two proper Lorentz transformations is proper.


lemma isProper_mul {Λ Λ' : LorentzGroup d}
    (h : IsProper Λ) (h' : IsProper Λ') : IsProper (Λ * Λ') := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsProper Λh':IsProper Λ'⊢ IsProper (Λ * Λ')
  rw [IsProper,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsProper Λh':IsProper Λ'⊢ (↑(Λ * Λ')).det = 1All goals completed! 🐙 lorentzGroupIsGroup_mul_coe,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsProper Λh':IsProper Λ'⊢ (↑Λ * ↑Λ').det = 1All goals completed! 🐙 det_mul,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsProper Λh':IsProper Λ'⊢ (↑Λ).det * (↑Λ').det = 1All goals completed! 🐙 h,d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsProper Λh':IsProper Λ'⊢ 1 * (↑Λ').det = 1All goals completed! 🐙 h',d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsProper Λh':IsProper Λ'⊢ 1 * 1 = 1All goals completed! 🐙 mul_oned:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:IsProper Λh':IsProper Λ'⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙

A Lorentz transformation is proper if its image under the det-representation detRep is 1.


lemma isProper_iff (Λ : LorentzGroup d) : IsProper Λ ↔ detRep Λ = 1 := byd:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ detRep Λ = 1
  rw [show 1 = detRep 1 from Eq.symm (MonoidHom.map_one detRep),d:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ detRep Λ = detRep 1d:ℕΛ:↑(𝓛 d)⊢ ℕd:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ (↑Λ).det = (↑1).det detRep_apply,d:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ detContinuous Λ = detRep 1d:ℕΛ:↑(𝓛 d)⊢ ℕd:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ (↑Λ).det = (↑1).det detRep_apply,d:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ detContinuous Λ = detContinuous 1d:ℕΛ:↑(𝓛 d)⊢ ℕd:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ (↑Λ).det = (↑1).det
    detContinuous_eq_iff_det_eqd:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ (↑Λ).det = (↑1).detd:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ (↑Λ).det = (↑1).det]d:ℕΛ:↑(𝓛 d)⊢ IsProper Λ ↔ (↑Λ).det = (↑1).det
  simp only [IsProper, lorentzGroupIsGroup_one_coe, det_one]All goals completed! 🐙

The identity Lorentz transformation is proper.

lemma isProper_id : @IsProper d 1 := byd:ℕ⊢ IsProper 1
  simp [IsProper]All goals completed! 🐙

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


lemma isProper_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
    IsProper Λ ↔ IsProper Λ' := byd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:Λ' ∈ connectedComponent Λ⊢ IsProper Λ ↔ IsProper Λ'
  simp only [IsProper]d:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:Λ' ∈ connectedComponent Λ⊢ (↑Λ).det = 1 ↔ (↑Λ').det = 1
  rw [det_on_connected_component hd:ℕΛ:↑(𝓛 d)Λ':↑(𝓛 d)h:Λ' ∈ connectedComponent Λ⊢ (↑Λ').det = 1 ↔ (↑Λ').det = 1All goals completed! 🐙]All goals completed! 🐙