From 89e940a0299f69637521d7b2b002748aaab92ff2 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 17 May 2024 11:52:16 -0400 Subject: [PATCH] refactor: Partial refactor of the lorentz group --- HepLean/SpaceTime/LorentzGroup/Basic.lean | 204 ++++++++++++++++++ .../SpaceTime/LorentzGroup/Orthochronous.lean | 124 +++++++++++ HepLean/SpaceTime/LorentzGroup/Proper.lean | 123 +++++++++++ HepLean/SpaceTime/Metric.lean | 14 ++ 4 files changed, 465 insertions(+) create mode 100644 HepLean/SpaceTime/LorentzGroup/Basic.lean create mode 100644 HepLean/SpaceTime/LorentzGroup/Orthochronous.lean create mode 100644 HepLean/SpaceTime/LorentzGroup/Proper.lean diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean new file mode 100644 index 0000000..8def7a5 --- /dev/null +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.Metric +import Mathlib.GroupTheory.SpecificGroups.KleinFour +/-! +# The Lorentz Group + +We define the Lorentz group. + +## TODO + +- Show that the Lorentz is a Lie group. +- Prove that the restricted Lorentz group is equivalent to the connected component of the +identity. +- Define the continuous maps from `ℝ³` to `restrictedLorentzGroup` defining boosts. + +## References + +- http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf + +-/ + + +noncomputable section + +namespace spaceTime + +open Manifold +open Matrix +open Complex +open ComplexConjugate + +/-- We say a matrix `Λ` preserves `ηLin` if for all `x` and `y`, + `ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y`. -/ +def PreservesηLin (Λ : Matrix (Fin 4) (Fin 4) ℝ) : Prop := + ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y + +namespace PreservesηLin + +variable (Λ : Matrix (Fin 4) (Fin 4) ℝ) + +lemma iff_on_right : PreservesηLin Λ ↔ + ∀ (x y : spaceTime), ηLin x ((η * Λᵀ * η * Λ) *ᵥ y) = ηLin x y := by + 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 iff_matrix : PreservesηLin Λ ↔ η * Λᵀ * η * Λ = 1 := by + rw [iff_on_right, ηLin_matrix_eq_identity_iff (η * Λᵀ * η * Λ)] + apply Iff.intro + · simp_all [ηLin, implies_true, iff_true, one_mulVec] + · simp_all only [ηLin, LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply, + mulVec_mulVec, implies_true] + +lemma iff_matrix' : PreservesηLin Λ ↔ Λ * (η * Λᵀ * η) = 1 := by + rw [iff_matrix] + apply Iff.intro + intro h + exact mul_eq_one_comm.mp h + intro h + exact mul_eq_one_comm.mp h + +lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by + apply Iff.intro + intro h + have h1 := congrArg transpose ((iff_matrix Λ).mp h) + rw [transpose_mul, transpose_mul, transpose_mul, η_transpose, + ← mul_assoc, transpose_one] at h1 + rw [iff_matrix' Λ.transpose, ← h1] + repeat rw [← mul_assoc] + intro h + have h1 := congrArg transpose ((iff_matrix Λ.transpose).mp h) + rw [transpose_mul, transpose_mul, transpose_mul, η_transpose, + ← mul_assoc, transpose_one, transpose_transpose] at h1 + rw [iff_matrix', ← h1] + repeat rw [← mul_assoc] + +/-- The lift of a matrix which preserves `ηLin` to an invertible matrix. -/ +def liftGL {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) : GL (Fin 4) ℝ := + ⟨Λ, η * Λᵀ * η , (iff_matrix' Λ).mp h , (iff_matrix Λ).mp h⟩ + +end PreservesηLin + +/-- The Lorentz group as a subgroup of the general linear group over the reals. -/ +def lorentzGroup : Subgroup (GL (Fin 4) ℝ) where + carrier := {Λ | PreservesηLin Λ} + 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 + + +def PreservesηLin.liftLor {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) : + lorentzGroup := ⟨liftGL h, h⟩ + +namespace lorentzGroup + +lemma mem_iff (Λ : GL (Fin 4) ℝ): Λ ∈ lorentzGroup ↔ PreservesηLin Λ := by + rfl + +/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/ +def transpose (Λ : lorentzGroup) : lorentzGroup := + PreservesηLin.liftLor ((PreservesηLin.iff_transpose Λ.1).mp Λ.2) + + +def kernalMap : C(GL (Fin 4) ℝ, Matrix (Fin 4) (Fin 4) ℝ) where + toFun Λ := η * Λ.1ᵀ * η * Λ.1 + continuous_toFun := by + apply Continuous.mul _ Units.continuous_val + apply Continuous.mul _ continuous_const + exact Continuous.mul continuous_const (Continuous.matrix_transpose (Units.continuous_val)) + +lemma kernalMap_kernal_eq_lorentzGroup : lorentzGroup = kernalMap ⁻¹' {1} := by + ext Λ + erw [mem_iff Λ, PreservesηLin.iff_matrix] + rfl + +/-- The Lorentz Group is a closed subset of `GL (Fin 4) ℝ`. -/ +theorem isClosed_of_GL4 : IsClosed (lorentzGroup : Set (GL (Fin 4) ℝ)) := by + rw [kernalMap_kernal_eq_lorentzGroup] + exact continuous_iff_isClosed.mp kernalMap.2 {1} isClosed_singleton + +section Relations + +/-- The first column of a lorentz matrix. -/ +@[simp] +def fstCol (Λ : lorentzGroup) : spaceTime := fun i => Λ.1 i 0 + +lemma ηLin_fstCol (Λ : lorentzGroup) : ηLin (fstCol Λ) (fstCol Λ) = 1 := by + rw [ηLin_expand] + have h00 := congrFun (congrFun ((PreservesηLin.iff_matrix Λ.1).mp ((mem_iff Λ.1).mp Λ.2)) 0) 0 + simp only [Fin.isValue, mul_apply, transpose_apply, Fin.sum_univ_four, ne_eq, zero_ne_one, + not_false_eq_true, η_off_diagonal, zero_mul, add_zero, Fin.reduceEq, one_ne_zero, mul_zero, + zero_add, one_apply_eq] at h00 + simp only [η, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one, + vecCons_const, one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two, + Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00 + rw [← h00] + simp only [fstCol, Fin.isValue] + ring + +lemma zero_component (x : { x : spaceTime // ηLin x x = 1}) : + x.1 0 ^ 2 = 1 + ‖x.1.space‖ ^ 2 := by + sorry + +/-- The space-like part of the first row of of a Lorentz matrix. -/ +@[simp] +def fstSpaceRow (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 0 i.succ + +/-- The space-like part of the first column of of a Lorentz matrix. -/ +@[simp] +def fstSpaceCol (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 i.succ 0 + +lemma fstSpaceRow_transpose (Λ : lorentzGroup) : fstSpaceRow (transpose Λ) = fstSpaceCol Λ := by + rfl + +lemma fstSpaceCol_transpose (Λ : lorentzGroup) : fstSpaceCol (transpose Λ) = fstSpaceRow Λ := by + rfl + +lemma fst_col_normalized (Λ : lorentzGroup) : + (Λ.1 0 0) ^ 2 - ‖fstSpaceCol Λ‖ ^ 2 = 1 := by + rw [← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three] + simp + rw [show Fin.succ 2 = 3 by rfl] + have h00 := congrFun (congrFun ((PreservesηLin.iff_matrix Λ.1).mp ((mem_iff Λ.1).mp Λ.2)) 0) 0 + simp only [Fin.isValue, mul_apply, transpose_apply, Fin.sum_univ_four, ne_eq, zero_ne_one, + not_false_eq_true, η_off_diagonal, zero_mul, add_zero, Fin.reduceEq, one_ne_zero, mul_zero, + zero_add, one_apply_eq] at h00 + simp only [η, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one, + vecCons_const, one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two, + Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00 + rw [← h00] + ring + +lemma fst_row_normalized + +end Relations + +end lorentzGroup + +end spaceTime diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean new file mode 100644 index 0000000..7320ab2 --- /dev/null +++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.LorentzGroup.Proper +import Mathlib.GroupTheory.SpecificGroups.KleinFour +/-! +# The Orthochronous Lorentz Group + +We define the give a series of lemmas related to the orthochronous property of lorentz +matrices. + +-/ + + +noncomputable section + +namespace spaceTime + +open Manifold +open Matrix +open Complex +open ComplexConjugate + +namespace lorentzGroup + +/-- The determinant of a member of the lorentz group is `1` or `-1`. -/ +lemma det_eq_one_or_neg_one (Λ : 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 ((PreservesηLin.iff_matrix' Λ.1).mp ((mem_iff Λ.1).mp Λ.2))) + +local notation "ℤ₂" => Multiplicative (ZMod 2) + +instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin + +instance : DiscreteTopology ℤ₂ := by + exact forall_open_iff_discrete.mp fun _ => trivial + +instance : TopologicalGroup ℤ₂ := TopologicalGroup.mk + +/-- A continuous function from `({-1, 1} : Set ℝ)` to `ℤ₂`. -/ +@[simps!] +def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where + toFun x := if x = ⟨1, by simp⟩ then (Additive.toMul 0) else (Additive.toMul (1 : ZMod 2)) + continuous_toFun := by + haveI : DiscreteTopology ({-1, 1} : Set ℝ) := discrete_of_t1_of_finite + exact continuous_of_discreteTopology + +/-- The continuous map taking a lorentz matrix to its determinant. -/ +def detContinuous : C(lorentzGroup, ℤ₂) := + ContinuousMap.comp coeForℤ₂ { + toFun := fun Λ => ⟨Λ.1.1.det, Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩, + continuous_toFun := by + refine Continuous.subtype_mk ?_ _ + exact Continuous.matrix_det $ + Continuous.comp' Units.continuous_val continuous_subtype_val} + +lemma detContinuous_eq_iff_det_eq (Λ Λ' : lorentzGroup) : + detContinuous Λ = detContinuous Λ' ↔ Λ.1.1.det = Λ'.1.1.det := by + apply Iff.intro + intro h + simp [detContinuous] at h + cases' det_eq_one_or_neg_one Λ with h1 h1 + <;> cases' det_eq_one_or_neg_one Λ' with h2 h2 + <;> simp_all [h1, h2, h] + rw [← toMul_zero, @Equiv.apply_eq_iff_eq] at h + change (0 : Fin 2) = (1 : Fin 2) at h + simp only [Fin.isValue, zero_ne_one] at h + nth_rewrite 2 [← toMul_zero] at h + rw [@Equiv.apply_eq_iff_eq] at h + change (1 : Fin 2) = (0 : Fin 2) at h + simp [Fin.isValue, zero_ne_one] at h + intro h + simp [detContinuous, h] + + +/-- The representation taking a lorentz matrix to its determinant. -/ +@[simps!] +def detRep : lorentzGroup →* ℤ₂ where + toFun Λ := detContinuous Λ + map_one' := by + simp [detContinuous] + map_mul' := by + intro Λ1 Λ2 + simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero, + mul_ite, mul_one, ite_mul, one_mul] + cases' (det_eq_one_or_neg_one Λ1) with h1 h1 + <;> cases' (det_eq_one_or_neg_one Λ2) with h2 h2 + <;> simp [h1, h2, detContinuous] + rfl + +lemma detRep_continuous : Continuous detRep := detContinuous.2 + +lemma det_on_connected_component {Λ Λ' : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) : + Λ.1.1.det = Λ'.1.1.det := by + obtain ⟨s, hs, hΛ'⟩ := h + let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s detContinuous + haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1 + 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Λ'⟩) + +lemma det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.1.det = Λ'.1.1.det := + det_on_connected_component $ pathComponent_subset_component _ h + +/-- A Lorentz Matrix is proper if its determinant is 1. -/ +@[simp] +def IsProper (Λ : lorentzGroup) : Prop := Λ.1.1.det = 1 + +instance : DecidablePred IsProper := by + intro Λ + apply Real.decidableEq + +lemma IsProper_iff (Λ : lorentzGroup) : IsProper Λ ↔ detRep Λ = 1 := by + rw [show 1 = detRep 1 by simp] + rw [detRep_apply, detRep_apply, detContinuous_eq_iff_det_eq] + simp only [IsProper, OneMemClass.coe_one, Units.val_one, det_one] + + +end lorentzGroup + +end spaceTime +end diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean new file mode 100644 index 0000000..0416fcc --- /dev/null +++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean @@ -0,0 +1,123 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.LorentzGroup.Basic +import Mathlib.GroupTheory.SpecificGroups.KleinFour +/-! +# The Proper Lorentz Group + +We define the give a series of lemmas related to the determinant of the lorentz group. + +-/ + + +noncomputable section + +namespace spaceTime + +open Manifold +open Matrix +open Complex +open ComplexConjugate + +namespace lorentzGroup + +/-- The determinant of a member of the lorentz group is `1` or `-1`. -/ +lemma det_eq_one_or_neg_one (Λ : 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 ((PreservesηLin.iff_matrix' Λ.1).mp ((mem_iff Λ.1).mp Λ.2))) + +local notation "ℤ₂" => Multiplicative (ZMod 2) + +instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin + +instance : DiscreteTopology ℤ₂ := by + exact forall_open_iff_discrete.mp fun _ => trivial + +instance : TopologicalGroup ℤ₂ := TopologicalGroup.mk + +/-- A continuous function from `({-1, 1} : Set ℝ)` to `ℤ₂`. -/ +@[simps!] +def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where + toFun x := if x = ⟨1, by simp⟩ then (Additive.toMul 0) else (Additive.toMul (1 : ZMod 2)) + continuous_toFun := by + haveI : DiscreteTopology ({-1, 1} : Set ℝ) := discrete_of_t1_of_finite + exact continuous_of_discreteTopology + +/-- The continuous map taking a lorentz matrix to its determinant. -/ +def detContinuous : C(lorentzGroup, ℤ₂) := + ContinuousMap.comp coeForℤ₂ { + toFun := fun Λ => ⟨Λ.1.1.det, Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩, + continuous_toFun := by + refine Continuous.subtype_mk ?_ _ + exact Continuous.matrix_det $ + Continuous.comp' Units.continuous_val continuous_subtype_val} + +lemma detContinuous_eq_iff_det_eq (Λ Λ' : lorentzGroup) : + detContinuous Λ = detContinuous Λ' ↔ Λ.1.1.det = Λ'.1.1.det := by + apply Iff.intro + intro h + simp [detContinuous] at h + cases' det_eq_one_or_neg_one Λ with h1 h1 + <;> cases' det_eq_one_or_neg_one Λ' with h2 h2 + <;> simp_all [h1, h2, h] + rw [← toMul_zero, @Equiv.apply_eq_iff_eq] at h + change (0 : Fin 2) = (1 : Fin 2) at h + simp only [Fin.isValue, zero_ne_one] at h + nth_rewrite 2 [← toMul_zero] at h + rw [@Equiv.apply_eq_iff_eq] at h + change (1 : Fin 2) = (0 : Fin 2) at h + simp [Fin.isValue, zero_ne_one] at h + intro h + simp [detContinuous, h] + + +/-- The representation taking a lorentz matrix to its determinant. -/ +@[simps!] +def detRep : lorentzGroup →* ℤ₂ where + toFun Λ := detContinuous Λ + map_one' := by + simp [detContinuous] + map_mul' := by + intro Λ1 Λ2 + simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero, + mul_ite, mul_one, ite_mul, one_mul] + cases' (det_eq_one_or_neg_one Λ1) with h1 h1 + <;> cases' (det_eq_one_or_neg_one Λ2) with h2 h2 + <;> simp [h1, h2, detContinuous] + rfl + +lemma detRep_continuous : Continuous detRep := detContinuous.2 + +lemma det_on_connected_component {Λ Λ' : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) : + Λ.1.1.det = Λ'.1.1.det := by + obtain ⟨s, hs, hΛ'⟩ := h + let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s detContinuous + haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1 + 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Λ'⟩) + +lemma det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.1.det = Λ'.1.1.det := + det_on_connected_component $ pathComponent_subset_component _ h + +/-- A Lorentz Matrix is proper if its determinant is 1. -/ +@[simp] +def IsProper (Λ : lorentzGroup) : Prop := Λ.1.1.det = 1 + +instance : DecidablePred IsProper := by + intro Λ + apply Real.decidableEq + +lemma IsProper_iff (Λ : lorentzGroup) : IsProper Λ ↔ detRep Λ = 1 := by + rw [show 1 = detRep 1 by simp] + rw [detRep_apply, detRep_apply, detContinuous_eq_iff_det_eq] + simp only [IsProper, OneMemClass.coe_one, Units.val_one, det_one] + + +end lorentzGroup + +end spaceTime +end diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean index 9784913..6480472 100644 --- a/HepLean/SpaceTime/Metric.lean +++ b/HepLean/SpaceTime/Metric.lean @@ -118,6 +118,20 @@ lemma ηLin_expand (x y : spaceTime) : ηLin x y = x 0 * y 0 - x 1 * y 1 - x 2 * cons_val_zero, cons_val_one, head_cons, mul_neg, cons_val_two, tail_cons, cons_val_three] ring +lemma ηLin_expand_self (x : spaceTime) : ηLin x x = x 0 ^ 2 - ‖x.space‖ ^ 2 := by + rw [← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three, ηLin_expand] + simp only [Fin.isValue, space, cons_val_zero, RCLike.inner_apply, conj_trivial, cons_val_one, + head_cons, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons] + ring + +lemma time_elm_sq_of_ηLin (x : spaceTime) : x 0 ^ 2 = ηLin x x + ‖x.space‖ ^ 2 := by + rw [ηLin_expand_self] + ring + +lemma ηLin_leq_time_sq (x : spaceTime) : ηLin x x ≤ x 0 ^ 2 := by + rw [time_elm_sq_of_ηLin] + apply (le_add_iff_nonneg_right _).mpr $ sq_nonneg ‖x.space‖ + lemma ηLin_space_inner_product (x y : spaceTime) : ηLin x y = x 0 * y 0 - ⟪x.space, y.space⟫_ℝ := by rw [ηLin_expand, @PiLp.inner_apply, Fin.sum_univ_three]