refactor: Move spacetime

HepLean/SpaceTime/LorentzGroup.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.Metric
+/-!
+# The Lorentz Group
+
+We define the Lorentz group, and show it is a closed subgroup General Linear Group.
+
+## TODO
+
+- Show that the Lorentz is a Lie group.
+- Define the proper Lorentz group.
+- Define the restricted Lorentz group, and prove it is connected.
+
+-/
+
+noncomputable section
+
+namespace spaceTime
+
+open Manifold
+open Matrix
+open Complex
+open ComplexConjugate
+
+/-- The Lorentz group as a subgroup of the general linear group over the reals. -/
+def lorentzGroup : Subgroup (GeneralLinearGroup (Fin 4) ℝ) where
+  carrier := {Λ | ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y}
+  mul_mem' {a b} := by
+    intros ha hb x y
+    simp only [Units.val_mul, mulVec_mulVec]
+    rw [← mulVec_mulVec, ← mulVec_mulVec, ha, hb]
+  one_mem' := by
+    intros x y
+    simp
+  inv_mem' {a} := by
+    intros ha x y
+    simp only [coe_units_inv, ← ha ((a.1⁻¹) *ᵥ x) ((a.1⁻¹) *ᵥ y), mulVec_mulVec]
+    have hx : (a.1 * (a.1)⁻¹) = 1 := by
+      simp only [@Units.mul_eq_one_iff_inv_eq, coe_units_inv]
+    simp [hx]
+
+/-- The Lorentz group is a topological group with the subset topology. -/
+instance : TopologicalGroup lorentzGroup :=
+  Subgroup.instTopologicalGroupSubtypeMem lorentzGroup
+
+lemma mem_lorentzGroup_iff (Λ : GeneralLinearGroup (Fin 4) ℝ) :
+    Λ ∈ lorentzGroup ↔ ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y := by
+  rfl
+
+lemma mem_lorentzGroup_iff' (Λ : GeneralLinearGroup (Fin 4) ℝ) :
+    Λ ∈ lorentzGroup ↔ ∀ (x y : spaceTime), ηLin (x) ((η * Λ.1ᵀ * η * Λ.1) *ᵥ y) = ηLin x y := by
+  rw [mem_lorentzGroup_iff]
+  apply Iff.intro
+  intro h
+  intro x y
+  have h1 := h x y
+  rw [ηLin_mulVec_left, mulVec_mulVec] at h1
+  exact h1
+  intro h
+  intro x y
+  rw [ηLin_mulVec_left, mulVec_mulVec]
+  exact h x y
+
+lemma mem_lorentzGroup_iff'' (Λ : GL (Fin 4) ℝ) :
+    Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η * Λ.1 = 1 := by
+  rw [mem_lorentzGroup_iff', ηLin_matrix_eq_identity_iff (η * Λ.1ᵀ * η * Λ.1)]
+  apply Iff.intro
+  · simp_all only [ηLin_apply_apply, implies_true, iff_true, one_mulVec]
+  · simp_all only [ηLin_apply_apply, mulVec_mulVec, implies_true]
+
+lemma det_lorentzGroup (Λ : lorentzGroup) : Λ.1.1.det = 1 ∨ Λ.1.1.det = -1 := by
+  simpa [← sq, det_one, det_mul, det_mul, det_mul, det_transpose, det_η] using
+    (congrArg det ((mem_lorentzGroup_iff'' Λ.1).mp Λ.2))
+
+/-- A continous map from `GL (Fin 4) ℝ` to  `Matrix (Fin 4) (Fin 4) ℝ` for which the Lorentz
+group is the kernal. -/
+def lorentzMap (Λ : GL (Fin 4) ℝ) : Matrix (Fin 4) (Fin 4) ℝ := η * Λ.1ᵀ * η * Λ.1
+
+lemma lorentzMap_continuous : Continuous lorentzMap := by
+  apply Continuous.mul _ Units.continuous_val
+  apply Continuous.mul _ continuous_const
+  exact Continuous.mul continuous_const (Continuous.matrix_transpose (Units.continuous_val))
+
+lemma lorentzGroup_kernal : lorentzGroup = lorentzMap ⁻¹' {1} := by
+  ext Λ
+  erw [mem_lorentzGroup_iff'' Λ]
+  rfl
+
+theorem lorentzGroup_isClosed : IsClosed (lorentzGroup : Set (GeneralLinearGroup (Fin 4) ℝ)) := by
+  rw [lorentzGroup_kernal]
+  exact continuous_iff_isClosed.mp lorentzMap_continuous {1} isClosed_singleton
+
+
+end spaceTime
+
+end