From f1e5bc8ac356ee1e6b1417c323cf115105b06ae6 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 16 May 2024 07:42:22 -0400 Subject: [PATCH 01/24] Update README.md --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 648044d..aa0bfa8 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,10 @@ A project to digitalize high energy physics. ## Where to learn more +- Read the associated paper: + + https://arxiv.org/abs/2405.08863 + - The documentation for this project is at: https://heplean.github.io/HepLean/ From f0ef95b628efc3487dc118bc541c49031fcc3c53 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 16 May 2024 09:23:14 -0400 Subject: [PATCH 02/24] refactor: Update matrix notation --- HepLean/SpaceTime/Metric.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean index a62eb4e..6a04cca 100644 --- a/HepLean/SpaceTime/Metric.lean +++ b/HepLean/SpaceTime/Metric.lean @@ -24,7 +24,7 @@ open ComplexConjugate /-- The metric as a `4×4` real matrix. -/ def η : Matrix (Fin 4) (Fin 4) ℝ := - ![![1, 0, 0, 0], ![0, -1, 0, 0], ![0, 0, -1, 0], ![0, 0, 0, -1]] + !![1, 0, 0, 0; 0, -1, 0, 0; 0, 0, -1, 0; 0, 0, 0, -1] lemma η_off_diagonal {μ ν : Fin 4} (h : μ ≠ ν) : η μ ν = 0 := by fin_cases μ <;> @@ -46,8 +46,8 @@ lemma η_transpose : η.transpose = η := by rw [transpose_apply, η_symmetric] lemma det_η : η.det = - 1 := by - simp only [η, det_succ_row_zero, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val', - empty_val', cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, + simp only [η, det_succ_row_zero, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, of_apply, + cons_val', empty_val', cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, cons_val_one, head_cons, submatrix_submatrix, Function.comp_apply, Fin.succ_one_eq_two, cons_val_two, tail_cons, det_unique, Fin.default_eq_zero, cons_val_succ, head_fin_const, Fin.sum_univ_succ, Fin.val_zero, pow_zero, one_mul, Fin.zero_succAbove, Finset.univ_unique, From 2cda0a017d5cdf74595f8cda7b914ceb8f9aac02 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 16 May 2024 10:05:05 -0400 Subject: [PATCH 03/24] refactor: Lint --- HepLean/SpaceTime/LorentzGroup.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/HepLean/SpaceTime/LorentzGroup.lean b/HepLean/SpaceTime/LorentzGroup.lean index 1b858e9..372eaf5 100644 --- a/HepLean/SpaceTime/LorentzGroup.lean +++ b/HepLean/SpaceTime/LorentzGroup.lean @@ -199,9 +199,9 @@ lemma fst_col_normalized (Λ : lorentzGroup) : 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, 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 + 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 @@ -245,7 +245,6 @@ lemma norm_row_leq_abs_zero_zero (Λ : lorentzGroup) : ‖fstRowToEuclid Λ‖ simp only [le_add_iff_nonneg_left, zero_le_one] - lemma zero_zero_sq_ge_one (Λ : lorentzGroup) : 1 ≤ (Λ.1 0 0) ^ 2 := by rw [zero_zero_sq_col Λ] refine le_add_of_le_of_nonneg ?_ (sq_nonneg _) From 181407ac3b777d848a8d519069d2c15e29d3f411 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 16 May 2024 10:17:31 -0400 Subject: [PATCH 04/24] docs: Update Contributing file. --- CONTRIBUTING.md | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 794c3a1..401196e 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -7,6 +7,17 @@ This assumes you have already installed Lean and setup HepLean. To add a result to HepLean: - Create a new branch of HepLean. -- Name the branch something which tells people what sort of things you are adding e.g. "StandardModel-HiggsPotential" -- On pushing to a brach GitHub will run a number of continous integration checks on your code. -- Once you are happy, and your branch has passed the continous integration checks, make a pull-request to the main branch of HepLean. +- Name the branch something which tells people what sort of things you are adding e.g., "StandardModel-HiggsPotential" +- On pushing to a branch GitHub will run a number of continuous integration checks on your code. +- Once you are happy, and your branch has passed the continuous integration checks, make a pull-request to the main branch of HepLean. + +## Naming commits + +It is useful to prefix commits with one of the following. +- `feat:` When you add one or more new lemma, definition, or theorems. +- `refactor:` When you are improving the layout and structure of the code. +- `fix:` When fixing a mistake in a definition or other Lean code. +- `docs:` When adding a comment or updating documentation. +- `style:` When adding e.g., white space, a semicolon etc. But does not change the overall + structure of the code. +- `chore:` Updating e.g., workflows. \ No newline at end of file From afb5016d222fc931000c388e00a7379b5b31e3a0 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 16 May 2024 10:21:49 -0400 Subject: [PATCH 05/24] doc: Update README with contribution --- README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 651f908..a0a1ee1 100644 --- a/README.md +++ b/README.md @@ -33,6 +33,8 @@ A project to digitalize high energy physics. We follow here roughly the same contribution policies as MathLib4 (which can be found [here](https://leanprover-community.github.io/contribute/index.html)). +A guide to contributing can be found [here](https://github.com/HEPLean/HepLean/blob/master/CONTRIBUTING.md). + If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the lean Zulip, or email. ## Installation @@ -43,7 +45,7 @@ See: https://leanprover-community.github.io/get_started.html ### Quick installation -- clone this repository +- Clone this repository - Open a terminal in the corresponding directory. - Run `lake exe cache get`. - Rune `lake build`. From b3887dbaefc0d01fdd11eecf8c8b9d82cacbbe8d Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 16 May 2024 10:26:35 -0400 Subject: [PATCH 06/24] docs: Update readme --- README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index a0a1ee1..a5671e9 100644 --- a/README.md +++ b/README.md @@ -4,10 +4,10 @@ A project to digitalize high energy physics. ## Aims of this project -- Use Lean to create a exhaustive database of definitions, theorems, proofs and calculations in high energy physics. -- Make a libary that is easy to use by the high energy physics community. +- Use Lean to create an exhaustive database of definitions, theorems, proofs, and calculations in high energy physics. +- Make a library that is easy to use by the high energy physics community. - Keep the database up-to date with developments in MathLib4. -- Create github workflows of relevence to the high energy physics community. +- Create gitHub workflows of relevance to the high energy physics community. ## Where to learn more @@ -48,4 +48,4 @@ See: https://leanprover-community.github.io/get_started.html - Clone this repository - Open a terminal in the corresponding directory. - Run `lake exe cache get`. -- Rune `lake build`. +- Run `lake build`. From 9aa57c560b8c2f6d214610f4e9d6fe37fabc8934 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 16 May 2024 10:42:58 -0400 Subject: [PATCH 07/24] Docs: Update ReadMe --- README.md | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index a5671e9..9712d0d 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,10 @@ A project to digitalize high energy physics. ## Where to learn more +- Read the associated paper: + + https://arxiv.org/abs/2405.08863 + - The documentation for this project is at: https://heplean.github.io/HepLean/ @@ -27,7 +31,6 @@ A project to digitalize high energy physics. - A small example script relating to the three fermion anomaly cancellation condition can be found [here](https://live.lean-lang.org/#code=import%20Mathlib.Tactic.Polyrith%20%0A%0Atheorem%20threeFamily%20(a%20b%20c%20%3A%20ℚ)%20(h%20%3A%20a%20%2B%20b%20%2B%20c%20%3D%200)%20(h3%20%3A%20a%20%5E%203%20%2B%20b%20%5E%203%20%2B%20c%20%5E%203%20%3D%200)%20%3A%20%0A%20%20%20%20a%20%3D%200%20∨%20b%20%3D%200%20∨%20c%20%3D%200%20%20%3A%3D%20by%20%0A%20%20have%20h1%20%3A%20c%20%3D%20-%20(a%20%2B%20b)%20%3A%3D%20by%20%0A%20%20%20%20linear_combination%20h%20%0A%20%20have%20h4%20%3A%20%203%20*%20a%20*%20b%20*%20c%20%3D%200%20%3A%3D%20by%20%0A%20%20%20%20rw%20%5B←%20h3%2C%20h1%5D%0A%20%20%20%20ring%20%0A%20%20simp%20at%20h4%20%0A%20%20exact%20or_assoc.mp%20h4%0A%20%20%0A) - ## Contributing @@ -35,17 +38,19 @@ We follow here roughly the same contribution policies as MathLib4 (which can be A guide to contributing can be found [here](https://github.com/HEPLean/HepLean/blob/master/CONTRIBUTING.md). -If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the lean Zulip, or email. +If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the lean Zulip, or email. ## Installation ### Installing Lean 4 -See: https://leanprover-community.github.io/get_started.html +The installation instructions for Lean 4 are given here: https://leanprover-community.github.io/get_started.html. -### Quick installation +### Installing HepLean -- Clone this repository -- Open a terminal in the corresponding directory. -- Run `lake exe cache get`. -- Run `lake build`. +- Clone this repository (or download the repository as a Zip file) +- Open a terminal at the top-level in the corresponding directory. +- Run `lake exe cache get`. The command `lake` should have been installed when you installed Lean. +- Run `lake build`. +- Open the directory (not a single file) in Visual Studio Code (or another Lean compatible code editor). + From fdf5fda1e73e043ba40a3836ed1f00ddcc259373 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 17 May 2024 09:40:14 -0400 Subject: [PATCH 08/24] feat: some topological properties of lorentz group --- HepLean/SpaceTime/Basic.lean | 5 + HepLean/SpaceTime/LorentzGroup.lean | 73 ++++- .../SpaceTime/LorentzGroup/Connectedness.lean | 293 ++++++++++++++++++ HepLean/SpaceTime/Metric.lean | 31 +- 4 files changed, 389 insertions(+), 13 deletions(-) create mode 100644 HepLean/SpaceTime/LorentzGroup/Connectedness.lean diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean index cc1da21..f63058a 100644 --- a/HepLean/SpaceTime/Basic.lean +++ b/HepLean/SpaceTime/Basic.lean @@ -5,6 +5,8 @@ Authors: Joseph Tooby-Smith -/ import Mathlib.Data.Complex.Exponential import Mathlib.Geometry.Manifold.VectorBundle.Basic +import Mathlib.Analysis.InnerProductSpace.Adjoint + /-! # Space time @@ -36,6 +38,9 @@ open Matrix open Complex open ComplexConjugate +/-- The space part of spacetime. -/ +@[simp] +def space (x : spaceTime) : EuclideanSpace ℝ (Fin 3) := ![x 1, x 2, x 3] /-- The structure of a smooth manifold on spacetime. -/ def asSmoothManifold : ModelWithCorners ℝ spaceTime spaceTime := 𝓘(ℝ, spaceTime) diff --git a/HepLean/SpaceTime/LorentzGroup.lean b/HepLean/SpaceTime/LorentzGroup.lean index 372eaf5..d58d0cf 100644 --- a/HepLean/SpaceTime/LorentzGroup.lean +++ b/HepLean/SpaceTime/LorentzGroup.lean @@ -56,13 +56,10 @@ def lorentzGroup : Subgroup (GeneralLinearGroup (Fin 4) ℝ) where 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] +lemma preserve_ηLin_iff' (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + (∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔ + ∀ (x y : spaceTime), ηLin (x) ((η * Λᵀ * η * Λ) *ᵥ y) = ηLin x y := by apply Iff.intro intro h intro x y @@ -74,19 +71,73 @@ lemma mem_lorentzGroup_iff' (Λ : GeneralLinearGroup (Fin 4) ℝ) : rw [ηLin_mulVec_left, mulVec_mulVec] exact h x y + +lemma preserve_ηLin_iff'' (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + (∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔ + η * Λᵀ * η * Λ = 1 := by + rw [preserve_ηLin_iff', η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 preserve_ηLin_iff''' (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + (∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔ + Λ * (η * Λᵀ * η) = 1 := by + rw [preserve_ηLin_iff''] + apply Iff.intro + intro h + exact mul_eq_one_comm.mp h + intro h + exact mul_eq_one_comm.mp h + +lemma preserve_ηLin_iff_transpose (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + (∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔ + (∀ (x y : spaceTime), ηLin (Λᵀ *ᵥ x) (Λᵀ *ᵥ y) = ηLin x y) := by + apply Iff.intro + intro h + have h1 := congrArg transpose ((preserve_ηLin_iff'' Λ).mp h) + rw [transpose_mul, transpose_mul, transpose_mul, η_transpose, + ← mul_assoc, transpose_one] at h1 + rw [preserve_ηLin_iff''' Λ.transpose, ← h1] + repeat rw [← mul_assoc] + intro h + have h1 := congrArg transpose ((preserve_ηLin_iff'' Λ.transpose).mp h) + rw [transpose_mul, transpose_mul, transpose_mul, η_transpose, + ← mul_assoc, transpose_one, transpose_transpose] at h1 + rw [preserve_ηLin_iff''', ← h1] + repeat rw [← mul_assoc] + +def preserveηLinGLnLift {Λ : Matrix (Fin 4) (Fin 4) ℝ} + (h : ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) : GL (Fin 4) ℝ := + ⟨Λ, η * Λᵀ * η ,(preserve_ηLin_iff''' Λ).mp h , (preserve_ηLin_iff'' Λ).mp h⟩ + +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] + exact preserve_ηLin_iff' Λ.1 + + 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] + rw [mem_lorentzGroup_iff] + exact preserve_ηLin_iff'' Λ lemma mem_lorentzGroup_iff''' (Λ : GL (Fin 4) ℝ) : Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η = Λ⁻¹ := by rw [mem_lorentzGroup_iff''] exact Units.mul_eq_one_iff_eq_inv +def preserveηLinLorentzLift {Λ : Matrix (Fin 4) (Fin 4) ℝ} + (h : ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) : lorentzGroup := + ⟨preserveηLinGLnLift h, (mem_lorentzGroup_iff (preserveηLinGLnLift h)).mpr h⟩ +-- TODO: Simplify using preserveηLinLorentzLift. lemma mem_lorentzGroup_iff_transpose (Λ : GL (Fin 4) ℝ) : Λ ∈ lorentzGroup ↔ ⟨transpose Λ, (transpose Λ)⁻¹, by rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ).symm] @@ -148,6 +199,8 @@ lemma det_eq_one_or_neg_one (Λ : lorentzGroup) : Λ.1.1.det = 1 ∨ Λ.1.1.det local notation "ℤ₂" => Multiplicative (ZMod 2) +instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin + /-- A group homomorphism from `lorentzGroup` to `ℤ₂` taking a matrix to 0 if it's determinant is 1 and 1 if its determinant is -1.-/ @[simps!] diff --git a/HepLean/SpaceTime/LorentzGroup/Connectedness.lean b/HepLean/SpaceTime/LorentzGroup/Connectedness.lean new file mode 100644 index 0000000..d3a0960 --- /dev/null +++ b/HepLean/SpaceTime/LorentzGroup/Connectedness.lean @@ -0,0 +1,293 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.LorentzGroup +import Mathlib.GroupTheory.SpecificGroups.KleinFour +import Mathlib.Topology.Constructions +/-! +# Connectedness of the restricted Lorentz group + +In this file we provide a proof that the restricted Lorentz group is connected. + +## References + +- The main argument follows: Guillem Cobos, The Lorentz Group, 2015: + https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf + +-/ +noncomputable section +namespace spaceTime + +def stepFunction : ℝ → ℝ := fun t => + if t < -1 then -1 else + if t < 1 then t else 1 + +lemma stepFunction_continuous : Continuous stepFunction := by + apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_id continuous_const) + all_goals + intro a ha + rw [@Set.Iio_def, @frontier_Iio, @Set.mem_singleton_iff] at ha + rw [ha] + simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte] + +def lorentzDet (Λ : lorentzGroup) : ({-1, 1} : Set ℝ) := + ⟨Λ.1.1.det, by + simp + exact Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩ + +lemma lorentzDet_continuous : Continuous lorentzDet := by + refine Continuous.subtype_mk ?_ fun x => lorentzDet.proof_1 x + exact Continuous.matrix_det $ + Continuous.comp' Units.continuous_val continuous_subtype_val + +instance set_discrete : DiscreteTopology ({-1, 1} : Set ℝ) := discrete_of_t1_of_finite + +lemma lorentzDet_eq_if_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : + Λ.1.1.det = Λ'.1.1.det := by + obtain ⟨f, hf, hf2⟩ := h + have h1 : Joined (lorentzDet Λ) (lorentzDet Λ') := + ⟨ContinuousMap.comp ⟨lorentzDet, lorentzDet_continuous⟩ f, congrArg lorentzDet hf, + congrArg lorentzDet hf2⟩ + obtain ⟨g, hg1, hg2⟩ := h1 + have h2 := (@IsPreconnected.subsingleton ({-1, 1} : Set ℝ) _ _ _ (isPreconnected_range g.2)) + (Set.mem_range_self 0) (Set.mem_range_self 1) + rw [hg1, hg2] at h2 + simpa [lorentzDet] using h2 + +lemma det_on_connected_component {Λ Λ' : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) : + Λ.1.1.det = Λ'.1.1.det := by + obtain ⟨s, hs, hΛ'⟩ := h + let f : ContinuousMap s ({-1, 1} : Set ℝ) := + ContinuousMap.restrict s ⟨lorentzDet, lorentzDet_continuous⟩ + haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1 + have hf := (@IsPreconnected.subsingleton ({-1, 1} : Set ℝ) _ _ _ (isPreconnected_range f.2)) + (Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩) + simpa [lorentzDet, f] using hf + +lemma det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.1.det = Λ'.1.1.det := + det_on_connected_component $ pathComponent_subset_component _ h + +namespace restrictedLorentzGroup + +/-- The set of spacetime points such that the time element is positive, and which are +normalised to 1. -/ +def P : Set (spaceTime) := {x | x 0 > 0 ∧ ηLin x x = 1} + +lemma P_time_comp (x : P) : x.1 0 = √(1 + ‖x.1.space‖ ^ 2) := by + symm + rw [Real.sqrt_eq_cases] + apply Or.inl + refine And.intro ?_ (le_of_lt x.2.1) + rw [← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three] + simp only [Fin.isValue, space, Matrix.cons_val_zero, RCLike.inner_apply, conj_trivial, + Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, + Matrix.tail_cons] + have h1 := x.2.2 + rw [ηLin_expand] at h1 + linear_combination h1 + +def oneInP : P := ⟨![1, 0, 0, 0], by simp, by + rw [ηLin_expand] + simp⟩ + +def pathToOneInP (u : P) : Path oneInP u where + toFun t := ⟨![√(1 + t ^ 2 * ‖u.1.space‖ ^ 2), t * u.1 1, t * u.1 2, t * u.1 3], + by + simp + refine Right.add_pos_of_pos_of_nonneg (Real.zero_lt_one) $ + mul_nonneg (sq_nonneg _) (sq_nonneg _) + , by + rw [ηLin_expand] + simp + rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three] + simp + ring + refine Right.add_nonneg (zero_le_one' ℝ) $ + mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩ + continuous_toFun := by + refine Continuous.subtype_mk ?_ _ + apply (continuous_pi_iff).mpr + intro i + fin_cases i + <;> continuity + source' := by + simp + rfl + target' := by + simp + refine SetCoe.ext ?_ + funext i + fin_cases i + simp + exact (P_time_comp u).symm + all_goals rfl + + + +/-- P is a topological space with the subset topology. -/ +instance : TopologicalSpace P := instTopologicalSpaceSubtype + +lemma P_path_connected : IsPathConnected (@Set.univ P) := by + use oneInP + apply And.intro trivial ?_ + intro y _ + use pathToOneInP y + simp only [Set.mem_univ, implies_true] + + + +lemma P_abs_space_lt_time_comp (x : P) : ‖x.1.space‖ < x.1 0 := by + rw [P_time_comp, Real.lt_sqrt] + exact lt_one_add (‖(x.1).space‖ ^ 2) + exact norm_nonneg (x.1).space + +lemma η_P_P_pos (u v : P) : 0 < ηLin u v := + lt_of_lt_of_le (sub_pos.mpr (mul_lt_mul_of_nonneg_of_pos + (P_abs_space_lt_time_comp u) ((P_abs_space_lt_time_comp v).le) + (norm_nonneg (u.1).space) v.2.1)) (ηLin_ge_sub_norm u v) + +lemma η_P_continuous (u : spaceTime) : Continuous (fun (a : P) => ηLin u a) := by + simp only [ηLin_expand] + refine Continuous.add ?_ ?_ + refine Continuous.add ?_ ?_ + refine Continuous.add ?_ ?_ + refine Continuous.comp' (continuous_mul_left _) ?_ + apply (continuous_pi_iff).mp + exact continuous_subtype_val + all_goals apply Continuous.neg + all_goals apply Continuous.comp' (continuous_mul_left _) + all_goals apply (continuous_pi_iff).mp + all_goals exact continuous_subtype_val + + +lemma one_plus_η_P_P (u v : P) : 1 + ηLin u v ≠ 0 := by + linarith [η_P_P_pos u v] + +def φAux₁ (u v : P) : spaceTime →ₗ[ℝ] spaceTime where + toFun x := (2 * ηLin x u) • v + map_add' x y := by + simp only [map_add, LinearMap.add_apply] + rw [mul_add, add_smul] + map_smul' c x := by + simp only [LinearMapClass.map_smul, LinearMap.smul_apply, smul_eq_mul, + RingHom.id_apply] + rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul] + + +def φAux₂ (u v : P) : spaceTime →ₗ[ℝ] spaceTime where + toFun x := - (ηLin x (u + v) / (1 + ηLin u v)) • (u + v) + map_add' x y := by + simp only + rw [ηLin.map_add, div_eq_mul_one_div] + rw [show (ηLin x + ηLin y) (↑u + ↑v) = ηLin x (u+v) + ηLin y (u+v) from rfl] + rw [add_mul, neg_add, add_smul, ← div_eq_mul_one_div, ← div_eq_mul_one_div] + map_smul' c x := by + simp only + rw [ηLin.map_smul] + rw [show (c • ηLin x) (↑u + ↑v) = c * ηLin x (u+v) from rfl] + rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul] + rfl + +def φ (u v : P) : spaceTime →ₗ[ℝ] spaceTime := LinearMap.id + φAux₁ u v + φAux₂ u v + +lemma φ_u_u_eq_id (u : P) : φ u u = LinearMap.id := by + ext x + simp [φ] + rw [add_assoc] + rw [@add_right_eq_self] + rw [@add_eq_zero_iff_eq_neg] + rw [φAux₁, φAux₂] + simp only [LinearMap.coe_mk, AddHom.coe_mk, map_add, smul_add, neg_smul, neg_add_rev, neg_neg] + rw [← add_smul] + apply congr + apply congrArg + repeat rw [u.2.2] + field_simp + ring + rfl + +def φMat (u v : P) : Matrix (Fin 4) (Fin 4) ℝ := LinearMap.toMatrix stdBasis stdBasis (φ u v) + +lemma φMat_mulVec (u v : P) (x : spaceTime) : (φMat u v).mulVec x = φ u v x := + LinearMap.toMatrix_mulVec_repr stdBasis stdBasis (φ u v) x + + +lemma φMat_element (u v : P) (i j : Fin 4) : (φMat u v) i j = + η i i * (ηLin (stdBasis i) (stdBasis j) + 2 * ηLin (stdBasis j) u * ηLin (stdBasis i) v - + ηLin (stdBasis i) (u + v) * ηLin (stdBasis j) (u + v) / (1 + ηLin u v)) := by + rw [ηLin_matrix_stdBasis' j i (φMat u v), φMat_mulVec] + simp only [φ, φAux₁, φAux₂, map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_apply, + LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, smul_eq_mul, map_neg, + mul_eq_mul_left_iff] + apply Or.inl + ring + + +lemma φMat_continuous (u : P) : Continuous (φMat u) := by + refine continuous_matrix ?_ + intro i j + simp only [φMat_element] + refine Continuous.comp' (continuous_mul_left (η i i)) ?hf + refine Continuous.sub ?_ ?_ + refine Continuous.comp' (continuous_add_left ((ηLin (stdBasis i)) (stdBasis j))) ?_ + refine Continuous.comp' (continuous_mul_left (2 * (ηLin (stdBasis j)) ↑u)) ?_ + exact η_P_continuous _ + refine Continuous.mul ?_ ?_ + refine Continuous.mul ?_ ?_ + simp only [(ηLin _).map_add] + refine Continuous.comp' ?_ ?_ + exact continuous_add_left ((ηLin (stdBasis i)) ↑u) + exact η_P_continuous _ + simp only [(ηLin _).map_add] + refine Continuous.comp' ?_ ?_ + exact continuous_add_left _ + exact η_P_continuous _ + refine Continuous.inv₀ ?_ ?_ + refine Continuous.comp' (continuous_add_left 1) ?_ + exact η_P_continuous _ + exact fun x => one_plus_η_P_P u x + + +lemma φMat_in_lorentz (u v : P) (x y : spaceTime) : + ηLin ((φMat u v).mulVec x) ((φMat u v).mulVec y) = ηLin x y := by + rw [φMat_mulVec, φMat_mulVec, φ, φAux₁, φAux₂] + have h1 : (1 + (ηLin ↑u) ↑v) ≠ 0 := one_plus_η_P_P u v + simp only [map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_coe, + id_eq, LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, map_neg, LinearMap.smul_apply, + smul_eq_mul, LinearMap.neg_apply] + field_simp + simp only [v.2.2, mul_one, u.2.2] + rw [ηLin_symm v u, ηLin_symm u y, ηLin_symm v y] + ring + +def φLor (u v : P) : lorentzGroup := + preserveηLinLorentzLift (φMat_in_lorentz u v) + +lemma φLor_continuous (u : P) : Continuous (φLor u) := by + refine Continuous.subtype_mk ?_ fun x => (preserveηLinLorentzLift (φMat_in_lorentz u x)).2 + refine Units.continuous_iff.mpr (And.intro ?_ ?_) + exact φMat_continuous u + change Continuous fun x => (η * (φMat u x).transpose * η) + refine Continuous.matrix_mul ?_ continuous_const + refine Continuous.matrix_mul continuous_const ?_ + exact Continuous.matrix_transpose (φMat_continuous u) + + +lemma φLor_joined_to_identity (u v : P) : Joined 1 (φLor u v) := by + obtain ⟨f, _⟩ := P_path_connected.joinedIn u trivial v trivial + use ContinuousMap.comp ⟨φLor u, φLor_continuous u⟩ f + · simp only [ContinuousMap.toFun_eq_coe, ContinuousMap.comp_apply, ContinuousMap.coe_coe, + Path.source, ContinuousMap.coe_mk] + rw [@Subtype.ext_iff, φLor, preserveηLinLorentzLift] + refine Units.val_eq_one.mp ?_ + simp [preserveηLinGLnLift, φMat, φ_u_u_eq_id u ] + · simp + +end restrictedLorentzGroup + + + +end spaceTime +end diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean index 6a04cca..9784913 100644 --- a/HepLean/SpaceTime/Metric.lean +++ b/HepLean/SpaceTime/Metric.lean @@ -67,6 +67,9 @@ lemma η_sq : η * η = 1 := by vecHead, vecTail, Function.comp_apply] +lemma η_diag_mul_self (μ : Fin 4) : η μ μ * η μ μ = 1 := by + fin_cases μ + <;> simp [η] lemma η_mulVec (x : spaceTime) : η *ᵥ x = ![x 0, -x 1, -x 2, -x 3] := by rw [explicit x] @@ -92,7 +95,6 @@ def linearMapForSpaceTime (x : spaceTime) : spaceTime →ₗ[ℝ] ℝ where rfl /-- The metric as a bilinear map from `spaceTime` to `ℝ`. -/ -@[simps!] def ηLin : LinearMap.BilinForm ℝ spaceTime where toFun x := linearMapForSpaceTime x map_add' x y := by @@ -116,6 +118,25 @@ 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_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] + 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 ηLin_ge_abs_inner_product (x y : spaceTime) : + x 0 * y 0 - ‖⟪x.space, y.space⟫_ℝ‖ ≤ (ηLin x y) := by + rw [ηLin_space_inner_product, sub_le_sub_iff_left] + exact Real.le_norm_self ⟪x.space, y.space⟫_ℝ + +lemma ηLin_ge_sub_norm (x y : spaceTime) : + x 0 * y 0 - ‖x.space‖ * ‖y.space‖ ≤ (ηLin x y) := by + apply le_trans ?_ (ηLin_ge_abs_inner_product x y) + rw [sub_le_sub_iff_left] + exact norm_inner_le_norm x.space y.space + + lemma ηLin_symm (x y : spaceTime) : ηLin x y = ηLin y x := by rw [ηLin_expand, ηLin_expand] ring @@ -138,7 +159,7 @@ lemma ηLin_η_stdBasis (μ ν : Fin 4) : ηLin (stdBasis μ) (stdBasis ν) = η lemma ηLin_mulVec_left (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : ηLin (Λ *ᵥ x) y = ηLin x ((η * Λᵀ * η) *ᵥ y) := by - simp only [ηLin_apply_apply, mulVec_mulVec] + simp only [ηLin, LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply, mulVec_mulVec] rw [(vecMul_transpose Λ x).symm, ← dotProduct_mulVec, mulVec_mulVec] rw [← mul_assoc, ← mul_assoc, η_sq, one_mul] @@ -151,12 +172,16 @@ lemma ηLin_matrix_stdBasis (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : ηLin (stdBasis ν) (Λ *ᵥ stdBasis μ) = η ν ν * Λ ν μ := by rw [ηLin_stdBasis_apply, stdBasis_mulVec] +lemma ηLin_matrix_stdBasis' (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + Λ ν μ = η ν ν * ηLin (stdBasis ν) (Λ *ᵥ stdBasis μ) := by + rw [ηLin_matrix_stdBasis, ← mul_assoc, η_diag_mul_self, one_mul] + lemma ηLin_matrix_eq_identity_iff (Λ : Matrix (Fin 4) (Fin 4) ℝ) : Λ = 1 ↔ ∀ (x y : spaceTime), ηLin x y = ηLin x (Λ *ᵥ y) := by apply Iff.intro intro h subst h - simp only [ηLin_apply_apply, one_mulVec, implies_true] + simp only [ηLin, one_mulVec, implies_true] intro h funext μ ν have h1 := h (stdBasis μ) (stdBasis ν) 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 09/24] 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] From 7ebd2af7a5878a0a87dc35be735a66a0e0e4764a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 17 May 2024 15:10:35 -0400 Subject: [PATCH 10/24] refactor: Major refactor of Lorentz group --- HepLean/SpaceTime/FourVelocity.lean | 242 +++++++++ HepLean/SpaceTime/LorentzGroup.lean | 501 ------------------ HepLean/SpaceTime/LorentzGroup/Basic.lean | 59 +-- HepLean/SpaceTime/LorentzGroup/Boosts.lean | 170 ++++++ .../SpaceTime/LorentzGroup/Connectedness.lean | 293 ---------- .../SpaceTime/LorentzGroup/Orthochronous.lean | 229 +++++--- 6 files changed, 563 insertions(+), 931 deletions(-) create mode 100644 HepLean/SpaceTime/FourVelocity.lean delete mode 100644 HepLean/SpaceTime/LorentzGroup.lean create mode 100644 HepLean/SpaceTime/LorentzGroup/Boosts.lean delete mode 100644 HepLean/SpaceTime/LorentzGroup/Connectedness.lean diff --git a/HepLean/SpaceTime/FourVelocity.lean b/HepLean/SpaceTime/FourVelocity.lean new file mode 100644 index 0000000..f637944 --- /dev/null +++ b/HepLean/SpaceTime/FourVelocity.lean @@ -0,0 +1,242 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.Metric +/-! +# Four velocity + +We define + +- `PreFourVelocity` : as a space-time element with norm 1. +- `FourVelocity` : as a space-time element with norm 1 and future pointing. + +-/ +open spaceTime + +@[simp] +def PreFourVelocity : Set spaceTime := + fun x => ηLin x x = 1 + +instance : TopologicalSpace PreFourVelocity := by + exact instTopologicalSpaceSubtype + +namespace PreFourVelocity +lemma mem_PreFourVelocity_iff {x : spaceTime} : x ∈ PreFourVelocity ↔ ηLin x x = 1 := by + rfl + +def neg (v : PreFourVelocity) : PreFourVelocity := ⟨-v, by + rw [mem_PreFourVelocity_iff] + simp only [map_neg, LinearMap.neg_apply, neg_neg] + exact v.2 ⟩ + +lemma zero_sq (v : PreFourVelocity) : v.1 0 ^ 2 = 1 + ‖v.1.space‖ ^ 2 := by + rw [time_elm_sq_of_ηLin, v.2] + +lemma zero_abs_ge_one (v : PreFourVelocity) : 1 ≤ |v.1 0| := by + have h1 := ηLin_leq_time_sq v.1 + rw [v.2] at h1 + exact (one_le_sq_iff_one_le_abs _).mp h1 + + +lemma zero_abs_gt_norm_space (v : PreFourVelocity) : ‖v.1.space‖ < |v.1 0| := by + rw [(abs_norm _).symm, ← @sq_lt_sq, zero_sq] + simp only [space, Fin.isValue, lt_add_iff_pos_left, zero_lt_one] + +lemma zero_abs_ge_norm_space (v : PreFourVelocity) : ‖v.1.space‖ ≤ |v.1 0| := + le_of_lt (zero_abs_gt_norm_space v) + +lemma zero_le_minus_one_or_ge_one (v : PreFourVelocity) : v.1 0 ≤ -1 ∨ 1 ≤ v.1 0 := + le_abs'.mp (zero_abs_ge_one v) + +lemma zero_nonpos_iff (v : PreFourVelocity) : v.1 0 ≤ 0 ↔ v.1 0 ≤ - 1 := by + apply Iff.intro + · intro h + cases' zero_le_minus_one_or_ge_one v with h1 h1 + exact h1 + linarith + · intro h + linarith + +lemma zero_nonneg_iff (v : PreFourVelocity) : 0 ≤ v.1 0 ↔ 1 ≤ v.1 0 := by + apply Iff.intro + · intro h + cases' zero_le_minus_one_or_ge_one v with h1 h1 + linarith + exact h1 + · intro h + linarith + +def IsFourVelocity (v : PreFourVelocity) : Prop := 0 ≤ v.1 0 + + +lemma IsFourVelocity_abs_zero {v : PreFourVelocity} (hv : IsFourVelocity v) : + |v.1 0| = v.1 0 := abs_of_nonneg hv + +lemma not_IsFourVelocity_iff (v : PreFourVelocity) : ¬ IsFourVelocity v ↔ v.1 0 ≤ 0 := by + rw [IsFourVelocity, not_le] + apply Iff.intro + intro h + exact le_of_lt h + intro h + have h1 := (zero_nonpos_iff v).mp h + linarith + +lemma not_IsFourVelocity_iff_neg {v : PreFourVelocity} : ¬ IsFourVelocity v ↔ + IsFourVelocity (neg v):= by + rw [not_IsFourVelocity_iff, IsFourVelocity] + simp only [Fin.isValue, neg] + change _ ↔ 0 ≤ - v.1 0 + simp + +lemma zero_abs_mul_sub_norm_space (v v' : PreFourVelocity) : + 0 ≤ |v.1 0| * |v'.1 0| - ‖v.1.space‖ * ‖v'.1.space‖ := by + apply sub_nonneg.mpr + apply mul_le_mul (zero_abs_ge_norm_space v) (zero_abs_ge_norm_space v') ?_ ?_ + exact norm_nonneg v'.1.space + exact abs_nonneg (v.1 0) + + +lemma euclid_norm_IsFourVelocity_IsFourVelocity {v v' : PreFourVelocity} + (h : IsFourVelocity v) (h' : IsFourVelocity v') : + 0 ≤ (v.1 0) * (v'.1 0) + ⟪v.1.space, v'.1.space⟫_ℝ := by + apply le_trans (zero_abs_mul_sub_norm_space v v') + rw [IsFourVelocity_abs_zero h, IsFourVelocity_abs_zero h', sub_eq_add_neg] + apply (add_le_add_iff_left _).mpr + rw [@neg_le] + apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (v'.1).space⟫_ℝ|) ?_ + exact abs_real_inner_le_norm (v.1).space (v'.1).space + +lemma euclid_norm_not_IsFourVelocity_not_IsFourVelocity {v v' : PreFourVelocity} + (h : ¬ IsFourVelocity v) (h' : ¬ IsFourVelocity v') : + 0 ≤ (v.1 0) * (v'.1 0) + ⟪v.1.space, v'.1.space⟫_ℝ := by + have h1 := euclid_norm_IsFourVelocity_IsFourVelocity (not_IsFourVelocity_iff_neg.mp h) + (not_IsFourVelocity_iff_neg.mp h') + apply le_of_le_of_eq h1 ?_ + simp [neg, Fin.sum_univ_three, neg] + repeat rw [show (- v.1) _ = - v.1 _ from rfl] + repeat rw [show (- v'.1) _ = - v'.1 _ from rfl] + ring + +lemma euclid_norm_IsFourVelocity_not_IsFourVelocity {v v' : PreFourVelocity} + (h : IsFourVelocity v) (h' : ¬ IsFourVelocity v') : + (v.1 0) * (v'.1 0) + ⟪v.1.space, v'.1.space⟫_ℝ ≤ 0 := by + rw [show (0 : ℝ) = - 0 by simp, le_neg] + have h1 := euclid_norm_IsFourVelocity_IsFourVelocity h (not_IsFourVelocity_iff_neg.mp h') + apply le_of_le_of_eq h1 ?_ + simp [neg, Fin.sum_univ_three, neg] + repeat rw [show (- v'.1) _ = - v'.1 _ from rfl] + ring + +lemma euclid_norm_not_IsFourVelocity_IsFourVelocity {v v' : PreFourVelocity} + (h : ¬ IsFourVelocity v) (h' : IsFourVelocity v') : + (v.1 0) * (v'.1 0) + ⟪v.1.space, v'.1.space⟫_ℝ ≤ 0 := by + rw [show (0 : ℝ) = - 0 by simp, le_neg] + have h1 := euclid_norm_IsFourVelocity_IsFourVelocity h' (not_IsFourVelocity_iff_neg.mp h) + apply le_of_le_of_eq h1 ?_ + simp [neg, Fin.sum_univ_three, neg] + repeat rw [show (- v.1) _ = - v.1 _ from rfl] + ring + +end PreFourVelocity + +def FourVelocity : Set PreFourVelocity := + fun x => PreFourVelocity.IsFourVelocity x + +instance : TopologicalSpace FourVelocity := instTopologicalSpaceSubtype + +namespace FourVelocity +open PreFourVelocity + +lemma mem_FourVelocity_iff {x : PreFourVelocity} : x ∈ FourVelocity ↔ 0 ≤ x.1 0 := by + rfl + +lemma time_comp (x : FourVelocity) : x.1.1 0 = √(1 + ‖x.1.1.space‖ ^ 2) := by + symm + rw [Real.sqrt_eq_cases] + refine Or.inl (And.intro ?_ x.2) + rw [← PreFourVelocity.zero_sq x.1, sq] + +def zero : FourVelocity := ⟨⟨![1, 0, 0, 0], by + rw [mem_PreFourVelocity_iff, ηLin_expand]; simp⟩, by + rw [mem_FourVelocity_iff]; simp⟩ + + +noncomputable def pathFromZero (u : FourVelocity) : Path zero u where + toFun t := ⟨ + ⟨![√(1 + t ^ 2 * ‖u.1.1.space‖ ^ 2), t * u.1.1 1, t * u.1.1 2, t * u.1.1 3], + by + rw [mem_PreFourVelocity_iff, ηLin_expand] + simp only [space, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, + Matrix.cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, Matrix.tail_cons, + Matrix.cons_val_three] + rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three] + simp only [Fin.isValue, Matrix.cons_val_zero, RCLike.inner_apply, conj_trivial, + Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two, Nat.succ_eq_add_one, + Nat.reduceAdd, Matrix.tail_cons] + ring + refine Right.add_nonneg (zero_le_one' ℝ) $ + mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩, + by + rw [mem_FourVelocity_iff] + exact Real.sqrt_nonneg _⟩ + continuous_toFun := by + refine Continuous.subtype_mk ?_ _ + refine Continuous.subtype_mk ?_ _ + apply (continuous_pi_iff).mpr + intro i + fin_cases i + <;> continuity + source' := by + simp + rfl + target' := by + simp + refine SetCoe.ext ?_ + refine SetCoe.ext ?_ + funext i + fin_cases i + simp + exact (time_comp _).symm + all_goals rfl + +lemma isPathConnected_FourVelocity : IsPathConnected (@Set.univ FourVelocity) := by + use zero + apply And.intro trivial ?_ + intro y _ + use pathFromZero y + simp only [Set.mem_univ, implies_true] + +lemma η_pos (u v : FourVelocity) : 0 < ηLin u v := by + refine lt_of_lt_of_le ?_ (ηLin_ge_sub_norm u v) + apply sub_pos.mpr + refine mul_lt_mul_of_nonneg_of_pos ?_ ?_ ?_ ?_ + simpa [IsFourVelocity_abs_zero u.2] using zero_abs_gt_norm_space u.1 + simpa [IsFourVelocity_abs_zero v.2] using zero_abs_ge_norm_space v.1 + exact norm_nonneg u.1.1.space + have h2 := (mem_FourVelocity_iff).mp v.2 + rw [zero_nonneg_iff] at h2 + linarith + +lemma one_plus_ne_zero (u v : FourVelocity) : 1 + ηLin u v ≠ 0 := by + linarith [η_pos u v] + +lemma η_continuous (u : spaceTime) : Continuous (fun (a : FourVelocity) => ηLin u a) := by + simp only [ηLin_expand] + refine Continuous.add ?_ ?_ + refine Continuous.add ?_ ?_ + refine Continuous.add ?_ ?_ + refine Continuous.comp' (continuous_mul_left _) ?_ + apply (continuous_pi_iff).mp + exact Isometry.continuous fun x1 => congrFun rfl + all_goals apply Continuous.neg + all_goals apply Continuous.comp' (continuous_mul_left _) + all_goals apply (continuous_pi_iff).mp + all_goals exact Isometry.continuous fun x1 => congrFun rfl + + + + + +end FourVelocity diff --git a/HepLean/SpaceTime/LorentzGroup.lean b/HepLean/SpaceTime/LorentzGroup.lean deleted file mode 100644 index d58d0cf..0000000 --- a/HepLean/SpaceTime/LorentzGroup.lean +++ /dev/null @@ -1,501 +0,0 @@ -/- -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 -- A proof that the restricted Lorentz group is connected can be found at: - https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf - The proof involves the introduction of boosts. - --/ - -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 preserve_ηLin_iff' (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - (∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔ - ∀ (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 preserve_ηLin_iff'' (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - (∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔ - η * Λᵀ * η * Λ = 1 := by - rw [preserve_ηLin_iff', η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 preserve_ηLin_iff''' (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - (∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔ - Λ * (η * Λᵀ * η) = 1 := by - rw [preserve_ηLin_iff''] - apply Iff.intro - intro h - exact mul_eq_one_comm.mp h - intro h - exact mul_eq_one_comm.mp h - -lemma preserve_ηLin_iff_transpose (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - (∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔ - (∀ (x y : spaceTime), ηLin (Λᵀ *ᵥ x) (Λᵀ *ᵥ y) = ηLin x y) := by - apply Iff.intro - intro h - have h1 := congrArg transpose ((preserve_ηLin_iff'' Λ).mp h) - rw [transpose_mul, transpose_mul, transpose_mul, η_transpose, - ← mul_assoc, transpose_one] at h1 - rw [preserve_ηLin_iff''' Λ.transpose, ← h1] - repeat rw [← mul_assoc] - intro h - have h1 := congrArg transpose ((preserve_ηLin_iff'' Λ.transpose).mp h) - rw [transpose_mul, transpose_mul, transpose_mul, η_transpose, - ← mul_assoc, transpose_one, transpose_transpose] at h1 - rw [preserve_ηLin_iff''', ← h1] - repeat rw [← mul_assoc] - -def preserveηLinGLnLift {Λ : Matrix (Fin 4) (Fin 4) ℝ} - (h : ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) : GL (Fin 4) ℝ := - ⟨Λ, η * Λᵀ * η ,(preserve_ηLin_iff''' Λ).mp h , (preserve_ηLin_iff'' Λ).mp h⟩ - -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] - exact preserve_ηLin_iff' Λ.1 - - -lemma mem_lorentzGroup_iff'' (Λ : GL (Fin 4) ℝ) : - Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η * Λ.1 = 1 := by - rw [mem_lorentzGroup_iff] - exact preserve_ηLin_iff'' Λ - -lemma mem_lorentzGroup_iff''' (Λ : GL (Fin 4) ℝ) : - Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η = Λ⁻¹ := by - rw [mem_lorentzGroup_iff''] - exact Units.mul_eq_one_iff_eq_inv - -def preserveηLinLorentzLift {Λ : Matrix (Fin 4) (Fin 4) ℝ} - (h : ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) : lorentzGroup := - ⟨preserveηLinGLnLift h, (mem_lorentzGroup_iff (preserveηLinGLnLift h)).mpr h⟩ - --- TODO: Simplify using preserveηLinLorentzLift. -lemma mem_lorentzGroup_iff_transpose (Λ : GL (Fin 4) ℝ) : - Λ ∈ lorentzGroup ↔ ⟨transpose Λ, (transpose Λ)⁻¹, by - rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ).symm] - rw [show ((Λ)⁻¹).1 * Λ.1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.inv_mul_eq_one]] - rw [@transpose_eq_one], by - rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ).symm] - rw [show Λ.1 * ((Λ)⁻¹).1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.mul_inv_eq_one]] - rw [@transpose_eq_one]⟩ ∈ lorentzGroup := by - rw [mem_lorentzGroup_iff''', mem_lorentzGroup_iff'''] - simp only [coe_units_inv, transpose_transpose, Units.inv_mk] - apply Iff.intro - intro h - have h1 := congrArg transpose h - rw [transpose_mul, transpose_mul, transpose_transpose, η_transpose, ← mul_assoc] at h1 - rw [h1] - exact transpose_nonsing_inv _ - intro h - have h1 := congrArg transpose h - rw [transpose_mul, transpose_mul, η_transpose, ← mul_assoc] at h1 - rw [h1, transpose_nonsing_inv, transpose_transpose] - -/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/ -def lorentzGroupTranspose (Λ : lorentzGroup) : lorentzGroup := - ⟨⟨transpose Λ.1, (transpose Λ.1)⁻¹, by - rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ.1).symm] - rw [show ((Λ.1)⁻¹).1 * Λ.1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.inv_mul_eq_one]] - rw [@transpose_eq_one], by - rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ.1).symm] - rw [show Λ.1.1 * ((Λ.1)⁻¹).1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.mul_inv_eq_one]] - rw [@transpose_eq_one]⟩, - (mem_lorentzGroup_iff_transpose Λ.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 - -/-- The Lorentz Group is a closed subset of `GL (Fin 4) ℝ`. -/ -theorem lorentzGroup_isClosed : IsClosed (lorentzGroup : Set (GL (Fin 4) ℝ)) := by - rw [lorentzGroup_kernal] - exact continuous_iff_isClosed.mp lorentzMap_continuous {1} isClosed_singleton - -namespace lorentzGroup - - -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 ((mem_lorentzGroup_iff'' Λ.1).mp Λ.2)) - -local notation "ℤ₂" => Multiplicative (ZMod 2) - -instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin - -/-- A group homomorphism from `lorentzGroup` to `ℤ₂` taking a matrix to -0 if it's determinant is 1 and 1 if its determinant is -1.-/ -@[simps!] -def detRep : lorentzGroup →* ℤ₂ where - toFun Λ := if Λ.1.1.det = 1 then (Additive.toMul 0) else Additive.toMul (1 : ZMod 2) - map_one' := by - simp - 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] - rfl - -/-- A Lorentz Matrix is proper if its determinant is 1. -/ -def IsProper (Λ : lorentzGroup) : Prop := Λ.1.1.det = 1 - -instance : DecidablePred IsProper := by - intro Λ - apply Real.decidableEq - -lemma IsProper_iff (Λ : lorentzGroup) : - IsProper Λ ↔ detRep Λ = Additive.toMul 0 := by - apply Iff.intro - intro h - erw [detRep_apply, if_pos h] - simp only [toMul_zero] - intro h - by_cases h1 : IsProper Λ - exact h1 - erw [detRep_apply, if_neg h1] at h - contradiction - -section Orthochronous - -/-- The space-like part of the first row of of a Lorentz matrix. -/ -@[simp] -def fstRowToEuclid (Λ : 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 fstColToEuclid (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 i.succ 0 - -lemma fst_col_normalized (Λ : lorentzGroup) : - (Λ.1 0 0) ^ 2 - (Λ.1 1 0) ^ 2 - (Λ.1 2 0) ^ 2 - (Λ.1 3 0) ^ 2 = 1 := by - have h00 := congrFun (congrFun ((mem_lorentzGroup_iff'' Λ).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 (Λ : lorentzGroup) : - (Λ.1 0 0) ^ 2 - (Λ.1 0 1) ^ 2 - (Λ.1 0 2) ^ 2 - (Λ.1 0 3) ^ 2 = 1 := by - simpa using fst_col_normalized (lorentzGroupTranspose Λ) - - -lemma zero_zero_sq_col (Λ : lorentzGroup) : - (Λ.1 0 0) ^ 2 = 1 + (Λ.1 1 0) ^ 2 + (Λ.1 2 0) ^ 2 + (Λ.1 3 0) ^ 2 := by - rw [← fst_col_normalized Λ] - ring - -lemma zero_zero_sq_row (Λ : lorentzGroup) : - (Λ.1 0 0) ^ 2 = 1 + (Λ.1 0 1) ^ 2 + (Λ.1 0 2) ^ 2 + (Λ.1 0 3) ^ 2 := by - rw [← fst_row_normalized Λ] - ring - -lemma zero_zero_sq_col' (Λ : lorentzGroup) : - (Λ.1 0 0) ^ 2 = 1 + ‖fstColToEuclid Λ‖ ^ 2 := by - rw [zero_zero_sq_col, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three] - simp only [Fin.isValue, fstColToEuclid, Fin.succ_zero_eq_one, RCLike.inner_apply, conj_trivial, - Fin.succ_one_eq_two] - rw [show (Fin.succ 2) = 3 by rfl] - ring_nf - -lemma zero_zero_sq_row' (Λ : lorentzGroup) : - (Λ.1 0 0) ^ 2 = 1 + ‖fstRowToEuclid Λ‖ ^ 2 := by - rw [zero_zero_sq_row, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three] - simp only [Fin.isValue, fstRowToEuclid, Fin.succ_zero_eq_one, RCLike.inner_apply, conj_trivial, - Fin.succ_one_eq_two] - rw [show (Fin.succ 2) = 3 by rfl] - ring_nf - -lemma norm_col_leq_abs_zero_zero (Λ : lorentzGroup) : ‖fstColToEuclid Λ‖ ≤ |Λ.1 0 0| := by - rw [(abs_norm (fstColToEuclid Λ)).symm, ← @sq_le_sq, zero_zero_sq_col'] - simp only [le_add_iff_nonneg_left, zero_le_one] - -lemma norm_row_leq_abs_zero_zero (Λ : lorentzGroup) : ‖fstRowToEuclid Λ‖ ≤ |Λ.1 0 0| := by - rw [(abs_norm (fstRowToEuclid Λ)).symm, ← @sq_le_sq, zero_zero_sq_row'] - simp only [le_add_iff_nonneg_left, zero_le_one] - - -lemma zero_zero_sq_ge_one (Λ : lorentzGroup) : 1 ≤ (Λ.1 0 0) ^ 2 := by - rw [zero_zero_sq_col Λ] - refine le_add_of_le_of_nonneg ?_ (sq_nonneg _) - refine le_add_of_le_of_nonneg ?_ (sq_nonneg _) - refine le_add_of_le_of_nonneg (le_refl 1) (sq_nonneg _) - -lemma abs_zero_zero_ge_one (Λ : lorentzGroup) : 1 ≤ |Λ.1 0 0| := - (one_le_sq_iff_one_le_abs _).mp (zero_zero_sq_ge_one Λ) - -lemma zero_zero_le_minus_one_or_ge_one (Λ : lorentzGroup) : (Λ.1 0 0) ≤ - 1 ∨ 1 ≤ (Λ.1 0 0) := - le_abs'.mp (abs_zero_zero_ge_one Λ) - -lemma zero_zero_nonpos_iff (Λ : lorentzGroup) : (Λ.1 0 0) ≤ 0 ↔ (Λ.1 0 0) ≤ - 1 := by - apply Iff.intro - · intro h - cases' zero_zero_le_minus_one_or_ge_one Λ with h1 h1 - exact h1 - linarith - · intro h - linarith - -lemma zero_zero_nonneg_iff (Λ : lorentzGroup) : 0 ≤ (Λ.1 0 0) ↔ 1 ≤ (Λ.1 0 0) := by - apply Iff.intro - · intro h - cases' zero_zero_le_minus_one_or_ge_one Λ with h1 h1 - linarith - exact h1 - · intro h - linarith - -/-- An element of the lorentz group is orthochronous if its time-time element is non-negative. -/ -@[simp] -def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0 - -instance : Decidable (IsOrthochronous Λ) := - Real.decidableLE 0 (Λ.1 0 0) - -lemma not_IsOrthochronous_iff (Λ : lorentzGroup) : ¬ IsOrthochronous Λ ↔ Λ.1 0 0 ≤ 0 := by - rw [IsOrthochronous, not_le] - apply Iff.intro - intro h - exact le_of_lt h - intro h - have h1 := (zero_zero_nonpos_iff Λ).mp h - linarith - - -lemma IsOrthochronous_abs_zero_zero {Λ : lorentzGroup} (h : IsOrthochronous Λ) : - |Λ.1 0 0| = Λ.1 0 0 := - abs_eq_self.mpr h - -lemma not_IsOrthochronous_abs_zero_zero {Λ : lorentzGroup} (h : ¬ IsOrthochronous Λ) : - Λ.1 0 0 = - |Λ.1 0 0| := by - refine neg_eq_iff_eq_neg.mp (abs_eq_neg_self.mpr ?_).symm - simp only [IsOrthochronous, Fin.isValue, not_le] at h - exact le_of_lt h - -lemma schwartz_identity_fst_row_col (Λ Λ' : lorentzGroup) : - ‖⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ‖ ≤ ‖fstRowToEuclid Λ‖ * ‖fstColToEuclid Λ'‖ := - norm_inner_le_norm (fstRowToEuclid Λ) (fstColToEuclid Λ') - -lemma zero_zero_mul (Λ Λ' : lorentzGroup) : - (Λ * Λ').1 0 0 = (Λ.1 0 0) * (Λ'.1 0 0) + ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ := by - rw [@Subgroup.coe_mul, @GeneralLinearGroup.coe_mul, mul_apply, Fin.sum_univ_four] - rw [@PiLp.inner_apply, Fin.sum_univ_three] - simp - rw [show (Fin.succ 2) = 3 by rfl] - ring_nf -example (a b c : ℝ ) (h : a - b ≤ a + c) : - b ≤ c := by - exact (add_le_add_iff_left a).mp h - -lemma zero_zero_mul_sub_row_col (Λ Λ' : lorentzGroup) : - 0 ≤ |Λ.1 0 0| * |Λ'.1 0 0| - ‖fstRowToEuclid Λ‖ * ‖fstColToEuclid Λ'‖ := - sub_nonneg.mpr (mul_le_mul (norm_row_leq_abs_zero_zero Λ) (norm_col_leq_abs_zero_zero Λ') - (norm_nonneg (fstColToEuclid Λ')) (abs_nonneg (Λ.1 0 0))) - -lemma orthchro_mul_orthchro {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ) - (h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by - apply le_trans (zero_zero_mul_sub_row_col Λ Λ') - have h1 := zero_zero_mul Λ Λ' - rw [← IsOrthochronous_abs_zero_zero h, ← IsOrthochronous_abs_zero_zero h'] at h1 - refine le_trans - (?_ : _ ≤ |Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|)) ?_ - · erw [add_le_add_iff_left] - simp only [neg_mul, neg_neg, neg_le] - exact schwartz_identity_fst_row_col Λ Λ' - · rw [h1, add_le_add_iff_left] - exact neg_abs_le ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ - -lemma not_orthchro_mul_not_orthchro {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ) - (h' : ¬ IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by - apply le_trans (zero_zero_mul_sub_row_col Λ Λ') - refine le_trans - (?_ : _ ≤ |Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|)) ?_ - · erw [add_le_add_iff_left] - simp only [neg_mul, neg_neg, neg_le] - exact schwartz_identity_fst_row_col Λ Λ' - · rw [zero_zero_mul Λ Λ', not_IsOrthochronous_abs_zero_zero h, - not_IsOrthochronous_abs_zero_zero h'] - simp only [Fin.isValue, abs_neg, _root_.abs_abs, conj_trivial, mul_neg, neg_mul, neg_neg, - add_le_add_iff_left] - exact neg_abs_le ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ - -lemma orthchro_mul_not_orthchro {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ) - (h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by - rw [not_IsOrthochronous_iff] - refine le_trans - (?_ : _ ≤ - (|Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|))) ?_ - · rw [zero_zero_mul Λ Λ', ← IsOrthochronous_abs_zero_zero h, - not_IsOrthochronous_abs_zero_zero h'] - simp only [Fin.isValue, mul_neg, _root_.abs_abs, abs_neg, neg_add_rev, neg_neg, - le_add_neg_iff_add_le, neg_add_cancel_comm] - exact le_abs_self ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ - · apply le_trans ?_ (neg_nonpos_of_nonneg (zero_zero_mul_sub_row_col Λ Λ')) - simp only [Fin.isValue, neg_add_rev, neg_neg, neg_sub, add_neg_le_iff_le_add, sub_add_cancel] - exact schwartz_identity_fst_row_col _ _ - -lemma not_orthchro_mul_orthchro {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ) - (h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by - rw [not_IsOrthochronous_iff] - refine le_trans - (?_ : _ ≤ - (|Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|))) ?_ - · rw [zero_zero_mul Λ Λ', ← IsOrthochronous_abs_zero_zero h', - not_IsOrthochronous_abs_zero_zero h] - simp only [Fin.isValue, neg_mul, PiLp.inner_apply, fstRowToEuclid, fstColToEuclid, - RCLike.inner_apply, conj_trivial, abs_neg, _root_.abs_abs, neg_add_rev, neg_neg, - le_add_neg_iff_add_le, neg_add_cancel_comm] - exact le_abs_self ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ - · apply le_trans ?_ (neg_nonpos_of_nonneg (zero_zero_mul_sub_row_col Λ Λ')) - simp only [Fin.isValue, neg_add_rev, neg_neg, neg_sub, add_neg_le_iff_le_add, sub_add_cancel] - exact schwartz_identity_fst_row_col _ _ - -/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernal consists of precisely the -orthochronous elements. -/ -@[simps!] -def orthochronousRep : lorentzGroup →* ℤ₂ where - toFun Λ := if IsOrthochronous Λ then (Additive.toMul 0) else Additive.toMul (1 : ZMod 2) - map_one' := by - simp - map_mul' := by - intro Λ1 Λ2 - simp only [toMul_zero, mul_ite, mul_one, ite_mul, one_mul] - cases' (em (IsOrthochronous Λ1)) with h h - <;> cases' (em (IsOrthochronous Λ2)) with h' h' - rw [if_pos (orthchro_mul_orthchro h h'), if_pos h, if_pos h'] - rw [if_neg (orthchro_mul_not_orthchro h h'), if_neg h', if_pos h] - rw [if_neg (not_orthchro_mul_orthchro h h'), if_pos h', if_neg h] - rw [if_pos (not_orthchro_mul_not_orthchro h h'), if_neg h', if_neg h] - rfl - -lemma IsOrthochronous_iff (Λ : lorentzGroup) : - IsOrthochronous Λ ↔ orthochronousRep Λ = Additive.toMul 0 := by - apply Iff.intro - intro h - erw [orthochronousRep_apply, if_pos h] - simp only [toMul_zero] - intro h - by_cases h1 : IsOrthochronous Λ - exact h1 - erw [orthochronousRep_apply, if_neg h1] at h - contradiction - - - -end Orthochronous - -end lorentzGroup - -open lorentzGroup in -/-- The restricted lorentz group consists of those elements of the `lorentzGroup` which are -proper and orthochronous. -/ -def restrictedLorentzGroup : Subgroup (lorentzGroup) where - carrier := {Λ | IsProper Λ ∧ IsOrthochronous Λ} - mul_mem' {Λa Λb} := by - intro ha hb - apply And.intro - rw [IsProper_iff, detRep.map_mul, (IsProper_iff Λa).mp ha.1, (IsProper_iff Λb).mp hb.1] - simp only [toMul_zero, mul_one] - rw [IsOrthochronous_iff, orthochronousRep.map_mul, (IsOrthochronous_iff Λa).mp ha.2, - (IsOrthochronous_iff Λb).mp hb.2] - simp - one_mem' := by - simp only [IsOrthochronous, Fin.isValue, Set.mem_setOf_eq, OneMemClass.coe_one, Units.val_one, - one_apply_eq, zero_le_one, and_true] - rw [IsProper_iff, detRep.map_one] - simp - inv_mem' {Λ} := by - intro h - apply And.intro - rw [IsProper_iff, detRep.map_inv, (IsProper_iff Λ).mp h.1] - simp only [toMul_zero, inv_one] - rw [IsOrthochronous_iff, orthochronousRep.map_inv, (IsOrthochronous_iff Λ).mp h.2] - simp - -/-- The restricted lorentz group is a topological group. -/ -instance : TopologicalGroup restrictedLorentzGroup := - Subgroup.instTopologicalGroupSubtypeMem restrictedLorentzGroup - -end spaceTime - -end diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index 8def7a5..2e13118 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.Metric +import HepLean.SpaceTime.FourVelocity import Mathlib.GroupTheory.SpecificGroups.KleinFour /-! # The Lorentz Group @@ -112,7 +113,7 @@ def lorentzGroup : Subgroup (GL (Fin 4) ℝ) where instance : TopologicalGroup lorentzGroup := Subgroup.instTopologicalGroupSubtypeMem lorentzGroup - +@[simps!] def PreservesηLin.liftLor {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) : lorentzGroup := ⟨liftGL h, h⟩ @@ -143,62 +144,6 @@ 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/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean new file mode 100644 index 0000000..2de9a49 --- /dev/null +++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.LorentzGroup.Orthochronous +import Mathlib.GroupTheory.SpecificGroups.KleinFour +import Mathlib.Topology.Constructions +/-! +# Boosts + +This file defines those Lorentz which are boosts. + +We first define generalised boosts, which are restricted lorentz transforamations taking +a four velocity `u` to a four velcoity `v`. + +A boost is the speical case of a generalised boost when `u = stdBasis 0`. + +## TODO + +- Show that generalised boosts are in the restircted Lorentz group. +- Define boosts. + +## References + +- The main argument follows: Guillem Cobos, The Lorentz Group, 2015: + https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf + +-/ +noncomputable section +namespace spaceTime + +namespace lorentzGroup + +open FourVelocity + + +def genBoostAux₁ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where + toFun x := (2 * ηLin x u) • v.1.1 + map_add' x y := by + simp only [map_add, LinearMap.add_apply] + rw [mul_add, add_smul] + map_smul' c x := by + simp only [LinearMapClass.map_smul, LinearMap.smul_apply, smul_eq_mul, + RingHom.id_apply] + rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul] + + +def genBoostAux₂ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where + toFun x := - (ηLin x (u + v) / (1 + ηLin u v)) • (u + v) + map_add' x y := by + simp only + rw [ηLin.map_add, div_eq_mul_one_div] + rw [show (ηLin x + ηLin y) (↑u + ↑v) = ηLin x (u+v) + ηLin y (u+v) from rfl] + rw [add_mul, neg_add, add_smul, ← div_eq_mul_one_div, ← div_eq_mul_one_div] + map_smul' c x := by + simp only + rw [ηLin.map_smul] + rw [show (c • ηLin x) (↑u + ↑v) = c * ηLin x (u+v) from rfl] + rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul] + rfl + +def genBoost (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime := + LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v + +namespace genBoost + +lemma self (u : FourVelocity) : genBoost u u = LinearMap.id := by + ext x + simp [genBoost] + rw [add_assoc] + rw [@add_right_eq_self] + rw [@add_eq_zero_iff_eq_neg] + rw [genBoostAux₁, genBoostAux₂] + simp only [LinearMap.coe_mk, AddHom.coe_mk, map_add, smul_add, neg_smul, neg_add_rev, neg_neg] + rw [← add_smul] + apply congr + apply congrArg + repeat rw [u.1.2] + field_simp + ring + rfl + +def toMatrix (u v : FourVelocity) : Matrix (Fin 4) (Fin 4) ℝ := + LinearMap.toMatrix stdBasis stdBasis (genBoost u v) + +lemma toMatrix_mulVec (u v : FourVelocity) (x : spaceTime) : + (toMatrix u v).mulVec x = genBoost u v x := + LinearMap.toMatrix_mulVec_repr stdBasis stdBasis (genBoost u v) x + +lemma toMatrix_apply (u v : FourVelocity) (i j : Fin 4) : + (toMatrix u v) i j = + η i i * (ηLin (stdBasis i) (stdBasis j) + 2 * ηLin (stdBasis j) u * ηLin (stdBasis i) v - + ηLin (stdBasis i) (u + v) * ηLin (stdBasis j) (u + v) / (1 + ηLin u v)) := by + rw [ηLin_matrix_stdBasis' j i (toMatrix u v), toMatrix_mulVec] + simp only [genBoost, genBoostAux₁, genBoostAux₂, map_add, smul_add, neg_smul, LinearMap.add_apply, + LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, smul_eq_mul, + map_neg, mul_eq_mul_left_iff] + apply Or.inl + ring + +lemma toMatrix_continuous (u : FourVelocity) : Continuous (toMatrix u) := by + refine continuous_matrix ?_ + intro i j + simp only [toMatrix_apply] + refine Continuous.comp' (continuous_mul_left (η i i)) ?hf + refine Continuous.sub ?_ ?_ + refine Continuous.comp' (continuous_add_left ((ηLin (stdBasis i)) (stdBasis j))) ?_ + refine Continuous.comp' (continuous_mul_left (2 * (ηLin (stdBasis j)) ↑u)) ?_ + exact η_continuous _ + refine Continuous.mul ?_ ?_ + refine Continuous.mul ?_ ?_ + simp only [(ηLin _).map_add] + refine Continuous.comp' ?_ ?_ + exact continuous_add_left ((ηLin (stdBasis i)) ↑u) + exact η_continuous _ + simp only [(ηLin _).map_add] + refine Continuous.comp' ?_ ?_ + exact continuous_add_left _ + exact η_continuous _ + refine Continuous.inv₀ ?_ ?_ + refine Continuous.comp' (continuous_add_left 1) ?_ + exact η_continuous _ + exact fun x => one_plus_ne_zero u x + + + +lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u v) := by + intro x y + rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂] + have h1 : (1 + (ηLin ↑u) ↑v) ≠ 0 := one_plus_ne_zero u v + simp only [map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_coe, + id_eq, LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, map_neg, LinearMap.smul_apply, + smul_eq_mul, LinearMap.neg_apply] + field_simp + rw [u.1.2, v.1.2, ηLin_symm v u, ηLin_symm u y, ηLin_symm v y] + ring + +def toLorentz (u v : FourVelocity) : lorentzGroup := + PreservesηLin.liftLor (toMatrix_PreservesηLin u v) + +lemma toLorentz_continuous (u : FourVelocity) : Continuous (toLorentz u) := by + refine Continuous.subtype_mk ?_ fun x => (PreservesηLin.liftLor (toMatrix_PreservesηLin u x)).2 + refine Units.continuous_iff.mpr (And.intro ?_ ?_) + exact toMatrix_continuous u + change Continuous fun x => (η * (toMatrix u x).transpose * η) + refine Continuous.matrix_mul ?_ continuous_const + refine Continuous.matrix_mul continuous_const ?_ + exact Continuous.matrix_transpose (toMatrix_continuous u) + + +lemma toLorentz_joined_to_1 (u v : FourVelocity) : Joined 1 (toLorentz u v) := by + obtain ⟨f, _⟩ := isPathConnected_FourVelocity.joinedIn u trivial v trivial + use ContinuousMap.comp ⟨toLorentz u, toLorentz_continuous u⟩ f + · simp only [ContinuousMap.toFun_eq_coe, ContinuousMap.comp_apply, ContinuousMap.coe_coe, + Path.source, ContinuousMap.coe_mk] + rw [@Subtype.ext_iff, toLorentz, PreservesηLin.liftLor] + refine Units.val_eq_one.mp ?_ + simp [PreservesηLin.liftGL, toMatrix, self u] + · simp + + +end genBoost + + +end lorentzGroup + + +end spaceTime +end diff --git a/HepLean/SpaceTime/LorentzGroup/Connectedness.lean b/HepLean/SpaceTime/LorentzGroup/Connectedness.lean deleted file mode 100644 index d3a0960..0000000 --- a/HepLean/SpaceTime/LorentzGroup/Connectedness.lean +++ /dev/null @@ -1,293 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license. -Authors: Joseph Tooby-Smith --/ -import HepLean.SpaceTime.LorentzGroup -import Mathlib.GroupTheory.SpecificGroups.KleinFour -import Mathlib.Topology.Constructions -/-! -# Connectedness of the restricted Lorentz group - -In this file we provide a proof that the restricted Lorentz group is connected. - -## References - -- The main argument follows: Guillem Cobos, The Lorentz Group, 2015: - https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf - --/ -noncomputable section -namespace spaceTime - -def stepFunction : ℝ → ℝ := fun t => - if t < -1 then -1 else - if t < 1 then t else 1 - -lemma stepFunction_continuous : Continuous stepFunction := by - apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_id continuous_const) - all_goals - intro a ha - rw [@Set.Iio_def, @frontier_Iio, @Set.mem_singleton_iff] at ha - rw [ha] - simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte] - -def lorentzDet (Λ : lorentzGroup) : ({-1, 1} : Set ℝ) := - ⟨Λ.1.1.det, by - simp - exact Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩ - -lemma lorentzDet_continuous : Continuous lorentzDet := by - refine Continuous.subtype_mk ?_ fun x => lorentzDet.proof_1 x - exact Continuous.matrix_det $ - Continuous.comp' Units.continuous_val continuous_subtype_val - -instance set_discrete : DiscreteTopology ({-1, 1} : Set ℝ) := discrete_of_t1_of_finite - -lemma lorentzDet_eq_if_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : - Λ.1.1.det = Λ'.1.1.det := by - obtain ⟨f, hf, hf2⟩ := h - have h1 : Joined (lorentzDet Λ) (lorentzDet Λ') := - ⟨ContinuousMap.comp ⟨lorentzDet, lorentzDet_continuous⟩ f, congrArg lorentzDet hf, - congrArg lorentzDet hf2⟩ - obtain ⟨g, hg1, hg2⟩ := h1 - have h2 := (@IsPreconnected.subsingleton ({-1, 1} : Set ℝ) _ _ _ (isPreconnected_range g.2)) - (Set.mem_range_self 0) (Set.mem_range_self 1) - rw [hg1, hg2] at h2 - simpa [lorentzDet] using h2 - -lemma det_on_connected_component {Λ Λ' : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) : - Λ.1.1.det = Λ'.1.1.det := by - obtain ⟨s, hs, hΛ'⟩ := h - let f : ContinuousMap s ({-1, 1} : Set ℝ) := - ContinuousMap.restrict s ⟨lorentzDet, lorentzDet_continuous⟩ - haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1 - have hf := (@IsPreconnected.subsingleton ({-1, 1} : Set ℝ) _ _ _ (isPreconnected_range f.2)) - (Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩) - simpa [lorentzDet, f] using hf - -lemma det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.1.det = Λ'.1.1.det := - det_on_connected_component $ pathComponent_subset_component _ h - -namespace restrictedLorentzGroup - -/-- The set of spacetime points such that the time element is positive, and which are -normalised to 1. -/ -def P : Set (spaceTime) := {x | x 0 > 0 ∧ ηLin x x = 1} - -lemma P_time_comp (x : P) : x.1 0 = √(1 + ‖x.1.space‖ ^ 2) := by - symm - rw [Real.sqrt_eq_cases] - apply Or.inl - refine And.intro ?_ (le_of_lt x.2.1) - rw [← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three] - simp only [Fin.isValue, space, Matrix.cons_val_zero, RCLike.inner_apply, conj_trivial, - Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, - Matrix.tail_cons] - have h1 := x.2.2 - rw [ηLin_expand] at h1 - linear_combination h1 - -def oneInP : P := ⟨![1, 0, 0, 0], by simp, by - rw [ηLin_expand] - simp⟩ - -def pathToOneInP (u : P) : Path oneInP u where - toFun t := ⟨![√(1 + t ^ 2 * ‖u.1.space‖ ^ 2), t * u.1 1, t * u.1 2, t * u.1 3], - by - simp - refine Right.add_pos_of_pos_of_nonneg (Real.zero_lt_one) $ - mul_nonneg (sq_nonneg _) (sq_nonneg _) - , by - rw [ηLin_expand] - simp - rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three] - simp - ring - refine Right.add_nonneg (zero_le_one' ℝ) $ - mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩ - continuous_toFun := by - refine Continuous.subtype_mk ?_ _ - apply (continuous_pi_iff).mpr - intro i - fin_cases i - <;> continuity - source' := by - simp - rfl - target' := by - simp - refine SetCoe.ext ?_ - funext i - fin_cases i - simp - exact (P_time_comp u).symm - all_goals rfl - - - -/-- P is a topological space with the subset topology. -/ -instance : TopologicalSpace P := instTopologicalSpaceSubtype - -lemma P_path_connected : IsPathConnected (@Set.univ P) := by - use oneInP - apply And.intro trivial ?_ - intro y _ - use pathToOneInP y - simp only [Set.mem_univ, implies_true] - - - -lemma P_abs_space_lt_time_comp (x : P) : ‖x.1.space‖ < x.1 0 := by - rw [P_time_comp, Real.lt_sqrt] - exact lt_one_add (‖(x.1).space‖ ^ 2) - exact norm_nonneg (x.1).space - -lemma η_P_P_pos (u v : P) : 0 < ηLin u v := - lt_of_lt_of_le (sub_pos.mpr (mul_lt_mul_of_nonneg_of_pos - (P_abs_space_lt_time_comp u) ((P_abs_space_lt_time_comp v).le) - (norm_nonneg (u.1).space) v.2.1)) (ηLin_ge_sub_norm u v) - -lemma η_P_continuous (u : spaceTime) : Continuous (fun (a : P) => ηLin u a) := by - simp only [ηLin_expand] - refine Continuous.add ?_ ?_ - refine Continuous.add ?_ ?_ - refine Continuous.add ?_ ?_ - refine Continuous.comp' (continuous_mul_left _) ?_ - apply (continuous_pi_iff).mp - exact continuous_subtype_val - all_goals apply Continuous.neg - all_goals apply Continuous.comp' (continuous_mul_left _) - all_goals apply (continuous_pi_iff).mp - all_goals exact continuous_subtype_val - - -lemma one_plus_η_P_P (u v : P) : 1 + ηLin u v ≠ 0 := by - linarith [η_P_P_pos u v] - -def φAux₁ (u v : P) : spaceTime →ₗ[ℝ] spaceTime where - toFun x := (2 * ηLin x u) • v - map_add' x y := by - simp only [map_add, LinearMap.add_apply] - rw [mul_add, add_smul] - map_smul' c x := by - simp only [LinearMapClass.map_smul, LinearMap.smul_apply, smul_eq_mul, - RingHom.id_apply] - rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul] - - -def φAux₂ (u v : P) : spaceTime →ₗ[ℝ] spaceTime where - toFun x := - (ηLin x (u + v) / (1 + ηLin u v)) • (u + v) - map_add' x y := by - simp only - rw [ηLin.map_add, div_eq_mul_one_div] - rw [show (ηLin x + ηLin y) (↑u + ↑v) = ηLin x (u+v) + ηLin y (u+v) from rfl] - rw [add_mul, neg_add, add_smul, ← div_eq_mul_one_div, ← div_eq_mul_one_div] - map_smul' c x := by - simp only - rw [ηLin.map_smul] - rw [show (c • ηLin x) (↑u + ↑v) = c * ηLin x (u+v) from rfl] - rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul] - rfl - -def φ (u v : P) : spaceTime →ₗ[ℝ] spaceTime := LinearMap.id + φAux₁ u v + φAux₂ u v - -lemma φ_u_u_eq_id (u : P) : φ u u = LinearMap.id := by - ext x - simp [φ] - rw [add_assoc] - rw [@add_right_eq_self] - rw [@add_eq_zero_iff_eq_neg] - rw [φAux₁, φAux₂] - simp only [LinearMap.coe_mk, AddHom.coe_mk, map_add, smul_add, neg_smul, neg_add_rev, neg_neg] - rw [← add_smul] - apply congr - apply congrArg - repeat rw [u.2.2] - field_simp - ring - rfl - -def φMat (u v : P) : Matrix (Fin 4) (Fin 4) ℝ := LinearMap.toMatrix stdBasis stdBasis (φ u v) - -lemma φMat_mulVec (u v : P) (x : spaceTime) : (φMat u v).mulVec x = φ u v x := - LinearMap.toMatrix_mulVec_repr stdBasis stdBasis (φ u v) x - - -lemma φMat_element (u v : P) (i j : Fin 4) : (φMat u v) i j = - η i i * (ηLin (stdBasis i) (stdBasis j) + 2 * ηLin (stdBasis j) u * ηLin (stdBasis i) v - - ηLin (stdBasis i) (u + v) * ηLin (stdBasis j) (u + v) / (1 + ηLin u v)) := by - rw [ηLin_matrix_stdBasis' j i (φMat u v), φMat_mulVec] - simp only [φ, φAux₁, φAux₂, map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_apply, - LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, smul_eq_mul, map_neg, - mul_eq_mul_left_iff] - apply Or.inl - ring - - -lemma φMat_continuous (u : P) : Continuous (φMat u) := by - refine continuous_matrix ?_ - intro i j - simp only [φMat_element] - refine Continuous.comp' (continuous_mul_left (η i i)) ?hf - refine Continuous.sub ?_ ?_ - refine Continuous.comp' (continuous_add_left ((ηLin (stdBasis i)) (stdBasis j))) ?_ - refine Continuous.comp' (continuous_mul_left (2 * (ηLin (stdBasis j)) ↑u)) ?_ - exact η_P_continuous _ - refine Continuous.mul ?_ ?_ - refine Continuous.mul ?_ ?_ - simp only [(ηLin _).map_add] - refine Continuous.comp' ?_ ?_ - exact continuous_add_left ((ηLin (stdBasis i)) ↑u) - exact η_P_continuous _ - simp only [(ηLin _).map_add] - refine Continuous.comp' ?_ ?_ - exact continuous_add_left _ - exact η_P_continuous _ - refine Continuous.inv₀ ?_ ?_ - refine Continuous.comp' (continuous_add_left 1) ?_ - exact η_P_continuous _ - exact fun x => one_plus_η_P_P u x - - -lemma φMat_in_lorentz (u v : P) (x y : spaceTime) : - ηLin ((φMat u v).mulVec x) ((φMat u v).mulVec y) = ηLin x y := by - rw [φMat_mulVec, φMat_mulVec, φ, φAux₁, φAux₂] - have h1 : (1 + (ηLin ↑u) ↑v) ≠ 0 := one_plus_η_P_P u v - simp only [map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_coe, - id_eq, LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, map_neg, LinearMap.smul_apply, - smul_eq_mul, LinearMap.neg_apply] - field_simp - simp only [v.2.2, mul_one, u.2.2] - rw [ηLin_symm v u, ηLin_symm u y, ηLin_symm v y] - ring - -def φLor (u v : P) : lorentzGroup := - preserveηLinLorentzLift (φMat_in_lorentz u v) - -lemma φLor_continuous (u : P) : Continuous (φLor u) := by - refine Continuous.subtype_mk ?_ fun x => (preserveηLinLorentzLift (φMat_in_lorentz u x)).2 - refine Units.continuous_iff.mpr (And.intro ?_ ?_) - exact φMat_continuous u - change Continuous fun x => (η * (φMat u x).transpose * η) - refine Continuous.matrix_mul ?_ continuous_const - refine Continuous.matrix_mul continuous_const ?_ - exact Continuous.matrix_transpose (φMat_continuous u) - - -lemma φLor_joined_to_identity (u v : P) : Joined 1 (φLor u v) := by - obtain ⟨f, _⟩ := P_path_connected.joinedIn u trivial v trivial - use ContinuousMap.comp ⟨φLor u, φLor_continuous u⟩ f - · simp only [ContinuousMap.toFun_eq_coe, ContinuousMap.comp_apply, ContinuousMap.coe_coe, - Path.source, ContinuousMap.coe_mk] - rw [@Subtype.ext_iff, φLor, preserveηLinLorentzLift] - refine Units.val_eq_one.mp ?_ - simp [preserveηLinGLnLift, φMat, φ_u_u_eq_id u ] - · simp - -end restrictedLorentzGroup - - - -end spaceTime -end diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean index 7320ab2..75b9c9f 100644 --- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean +++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ +import HepLean.SpaceTime.FourVelocity import HepLean.SpaceTime.LorentzGroup.Proper import Mathlib.GroupTheory.SpecificGroups.KleinFour /-! @@ -11,6 +12,10 @@ import Mathlib.GroupTheory.SpecificGroups.KleinFour We define the give a series of lemmas related to the orthochronous property of lorentz matrices. +## TODO + +- Prove topological properties. + -/ @@ -24,100 +29,164 @@ open Complex open ComplexConjugate namespace lorentzGroup +open PreFourVelocity -/-- 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))) +/-- The first column of a lorentz matrix as a `PreFourVelocity`. -/ +@[simp] +def fstCol (Λ : lorentzGroup) : PreFourVelocity := ⟨Λ.1 *ᵥ stdBasis 0, by + rw [mem_PreFourVelocity_iff, ηLin_expand] + simp only [Fin.isValue, stdBasis_mulVec] + 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⟩ + +def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0 + +lemma IsOrthochronous_iff_transpose (Λ : lorentzGroup) : + IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by + simp [IsOrthochronous] + simp [transpose] + +lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) : + IsOrthochronous Λ ↔ IsFourVelocity (fstCol Λ) := by + simp [IsOrthochronous, IsFourVelocity] + rw [stdBasis_mulVec] + +def mapZeroZeroComp : C(lorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0, by + refine Continuous.matrix_elem ?_ 0 0 + refine Continuous.comp' Units.continuous_val continuous_subtype_val⟩ + + +def stepFunction : ℝ → ℝ := fun t => + if t ≤ -1 then -1 else + if 1 ≤ t then 1 else t + +lemma stepFunction_continuous : Continuous stepFunction := by + apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_const continuous_id) + <;> intro a ha + rw [@Set.Iic_def, @frontier_Iic, @Set.mem_singleton_iff] at ha + rw [ha] + simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte] + have h1 : ¬ (1 : ℝ) ≤ 0 := by simp + rw [if_neg h1] + rw [Set.Ici_def, @frontier_Ici, @Set.mem_singleton_iff] at ha + simp [ha] + +def orthchroMapReal : C(lorentzGroup, ℝ) := ContinuousMap.comp + ⟨stepFunction, stepFunction_continuous⟩ mapZeroZeroComp + +lemma orthchroMapReal_on_IsOrthochronous {Λ : lorentzGroup} (h : IsOrthochronous Λ) : + orthchroMapReal Λ = 1 := by + rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h + simp only [IsFourVelocity] at h + rw [zero_nonneg_iff] at h + simp [stdBasis_mulVec] at h + have h1 : ¬ Λ.1 0 0 ≤ (-1 : ℝ) := by linarith + change stepFunction (Λ.1 0 0) = 1 + rw [stepFunction, if_neg h1, if_pos h] + + +lemma orthchroMapReal_on_not_IsOrthochronous {Λ : lorentzGroup} (h : ¬ IsOrthochronous Λ) : + orthchroMapReal Λ = - 1 := by + rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h + rw [not_IsFourVelocity_iff, zero_nonpos_iff] at h + simp only [fstCol, Fin.isValue, stdBasis_mulVec] at h + change stepFunction (Λ.1 0 0) = - 1 + rw [stepFunction, if_pos h] + +lemma orthchroMapReal_minus_one_or_one (Λ : lorentzGroup) : + orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 := by + by_cases h : IsOrthochronous Λ + apply Or.inr $ orthchroMapReal_on_IsOrthochronous h + apply Or.inl $ orthchroMapReal_on_not_IsOrthochronous h local notation "ℤ₂" => Multiplicative (ZMod 2) -instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin +def orthchroMap : C(lorentzGroup, ℤ₂) := + ContinuousMap.comp coeForℤ₂ { + toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩, + continuous_toFun := Continuous.subtype_mk (ContinuousMap.continuous orthchroMapReal) _} -instance : DiscreteTopology ℤ₂ := by - exact forall_open_iff_discrete.mp fun _ => trivial +lemma orthchroMap_IsOrthochronous {Λ : lorentzGroup} (h : IsOrthochronous Λ) : + orthchroMap Λ = 1 := by + simp [orthchroMap, orthchroMapReal_on_IsOrthochronous h] -instance : TopologicalGroup ℤ₂ := TopologicalGroup.mk +lemma orthchroMap_not_IsOrthochronous {Λ : lorentzGroup} (h : ¬ IsOrthochronous Λ) : + orthchroMap Λ = Additive.toMul (1 : ZMod 2) := by + simp [orthchroMap, orthchroMapReal_on_not_IsOrthochronous h] + rfl -/-- 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 +lemma zero_zero_mul (Λ Λ' : lorentzGroup) : + (Λ * Λ').1 0 0 = (fstCol (transpose Λ)).1 0 * (fstCol Λ').1 0 + + ⟪(fstCol (transpose Λ)).1.space, (fstCol Λ').1.space⟫_ℝ := by + rw [@Subgroup.coe_mul, @GeneralLinearGroup.coe_mul, mul_apply, Fin.sum_univ_four] + rw [@PiLp.inner_apply, Fin.sum_univ_three] + simp [transpose, stdBasis_mulVec] + ring -/-- 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 mul_othchron_of_othchron_othchron {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ) + (h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by + rw [IsOrthochronous_iff_transpose] at h + rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h' + rw [IsOrthochronous, zero_zero_mul] + exact euclid_norm_IsFourVelocity_IsFourVelocity h h' -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] +lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ) + (h' : ¬ IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by + rw [IsOrthochronous_iff_transpose] at h + rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h' + rw [IsOrthochronous, zero_zero_mul] + exact euclid_norm_not_IsFourVelocity_not_IsFourVelocity h h' +lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ) + (h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by + rw [IsOrthochronous_iff_transpose] at h + rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h' + rw [IsOrthochronous_iff_fstCol_IsFourVelocity, not_IsFourVelocity_iff] + simp [stdBasis_mulVec] + change (Λ * Λ').1 0 0 ≤ _ + rw [zero_zero_mul] + exact euclid_norm_IsFourVelocity_not_IsFourVelocity h h' -/-- The representation taking a lorentz matrix to its determinant. -/ -@[simps!] -def detRep : lorentzGroup →* ℤ₂ where - toFun Λ := detContinuous Λ +lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ) + (h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by + rw [IsOrthochronous_iff_transpose] at h + rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h' + rw [IsOrthochronous_iff_fstCol_IsFourVelocity, not_IsFourVelocity_iff] + simp [stdBasis_mulVec] + change (Λ * Λ').1 0 0 ≤ _ + rw [zero_zero_mul] + exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h' + +def orthchroRep : lorentzGroup →* ℤ₂ where + toFun := orthchroMap 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] + have h1 : IsOrthochronous 1 := by simp [IsOrthochronous] + rw [orthchroMap_IsOrthochronous h1] + map_mul' Λ Λ' := by + simp + by_cases h : IsOrthochronous Λ + <;> by_cases h' : IsOrthochronous Λ' + rw [orthchroMap_IsOrthochronous h, orthchroMap_IsOrthochronous h', + orthchroMap_IsOrthochronous (mul_othchron_of_othchron_othchron h h')] + simp + rw [orthchroMap_IsOrthochronous h, orthchroMap_not_IsOrthochronous h', + orthchroMap_not_IsOrthochronous (mul_not_othchron_of_othchron_not_othchron h h')] + simp + rw [orthchroMap_not_IsOrthochronous h, orthchroMap_IsOrthochronous h', + orthchroMap_not_IsOrthochronous (mul_not_othchron_of_not_othchron_othchron h h')] + simp + rw [orthchroMap_not_IsOrthochronous h, orthchroMap_not_IsOrthochronous h', + orthchroMap_IsOrthochronous (mul_othchron_of_not_othchron_not_othchron h h')] + simp only [Nat.reduceAdd] 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 From c61e2774e17d99774d5423c12570320e2de98a89 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 17 May 2024 15:28:05 -0400 Subject: [PATCH 11/24] refactor: Lint --- HepLean.lean | 6 ++++- HepLean/SpaceTime/FourVelocity.lean | 13 ++++++++--- HepLean/SpaceTime/LorentzGroup/Basic.lean | 6 +++-- HepLean/SpaceTime/LorentzGroup/Boosts.lean | 9 +++++--- .../SpaceTime/LorentzGroup/Orthochronous.lean | 22 ++++++++++++------- 5 files changed, 39 insertions(+), 17 deletions(-) diff --git a/HepLean.lean b/HepLean.lean index 6c336db..fa45853 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -56,7 +56,11 @@ import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters import HepLean.SpaceTime.Basic import HepLean.SpaceTime.CliffordAlgebra -import HepLean.SpaceTime.LorentzGroup +import HepLean.SpaceTime.FourVelocity +import HepLean.SpaceTime.LorentzGroup.Basic +import HepLean.SpaceTime.LorentzGroup.Boosts +import HepLean.SpaceTime.LorentzGroup.Orthochronous +import HepLean.SpaceTime.LorentzGroup.Proper import HepLean.SpaceTime.Metric import HepLean.StandardModel.Basic import HepLean.StandardModel.HiggsBoson.Basic diff --git a/HepLean/SpaceTime/FourVelocity.lean b/HepLean/SpaceTime/FourVelocity.lean index f637944..9b60b2d 100644 --- a/HepLean/SpaceTime/FourVelocity.lean +++ b/HepLean/SpaceTime/FourVelocity.lean @@ -15,6 +15,7 @@ We define -/ open spaceTime +/-- A `spaceTime` vector for which `ηLin x x = 1`. -/ @[simp] def PreFourVelocity : Set spaceTime := fun x => ηLin x x = 1 @@ -26,6 +27,7 @@ namespace PreFourVelocity lemma mem_PreFourVelocity_iff {x : spaceTime} : x ∈ PreFourVelocity ↔ ηLin x x = 1 := by rfl +/-- The negative of a `PreFourVelocity` as a `PreFourVelocity`. -/ def neg (v : PreFourVelocity) : PreFourVelocity := ⟨-v, by rw [mem_PreFourVelocity_iff] simp only [map_neg, LinearMap.neg_apply, neg_neg] @@ -68,6 +70,7 @@ lemma zero_nonneg_iff (v : PreFourVelocity) : 0 ≤ v.1 0 ↔ 1 ≤ v.1 0 := by · intro h linarith +/-- A `PreFourVelocity` is a `FourVelocity` if its time componenet is non-negative. -/ def IsFourVelocity (v : PreFourVelocity) : Prop := 0 ≤ v.1 0 @@ -141,6 +144,7 @@ lemma euclid_norm_not_IsFourVelocity_IsFourVelocity {v v' : PreFourVelocity} end PreFourVelocity +/-- The set of `PreFourVelocity`'s which are four velocities. -/ def FourVelocity : Set PreFourVelocity := fun x => PreFourVelocity.IsFourVelocity x @@ -158,11 +162,13 @@ lemma time_comp (x : FourVelocity) : x.1.1 0 = √(1 + ‖x.1.1.space‖ ^ 2) := refine Or.inl (And.intro ?_ x.2) rw [← PreFourVelocity.zero_sq x.1, sq] +/-- The `FourVelocity` which has all space components zero. -/ def zero : FourVelocity := ⟨⟨![1, 0, 0, 0], by rw [mem_PreFourVelocity_iff, ηLin_expand]; simp⟩, by rw [mem_FourVelocity_iff]; simp⟩ +/-- A continuous path from the zero `FourVelocity` to any other. -/ noncomputable def pathFromZero (u : FourVelocity) : Path zero u where toFun t := ⟨ ⟨![√(1 + t ^ 2 * ‖u.1.1.space‖ ^ 2), t * u.1.1 1, t * u.1.1 2, t * u.1.1 3], @@ -189,15 +195,16 @@ noncomputable def pathFromZero (u : FourVelocity) : Path zero u where fin_cases i <;> continuity source' := by - simp + simp only [Set.Icc.coe_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, space, + Fin.isValue, zero_mul, add_zero, Real.sqrt_one] rfl target' := by - simp + simp only [Set.Icc.coe_one, one_pow, space, Fin.isValue, one_mul] refine SetCoe.ext ?_ refine SetCoe.ext ?_ funext i fin_cases i - simp + simp only [Fin.isValue, Fin.zero_eta, Matrix.cons_val_zero] exact (time_comp _).symm all_goals rfl diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index 2e13118..2c2d119 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -113,9 +113,9 @@ def lorentzGroup : Subgroup (GL (Fin 4) ℝ) where instance : TopologicalGroup lorentzGroup := Subgroup.instTopologicalGroupSubtypeMem lorentzGroup -@[simps!] +/-- The lift of a matrix perserving `ηLin` to a Lorentz Group element. -/ def PreservesηLin.liftLor {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) : - lorentzGroup := ⟨liftGL h, h⟩ + lorentzGroup := ⟨liftGL h, h⟩ namespace lorentzGroup @@ -127,6 +127,8 @@ def transpose (Λ : lorentzGroup) : lorentzGroup := PreservesηLin.liftLor ((PreservesηLin.iff_transpose Λ.1).mp Λ.2) +/-- The continuous map from `GL (Fin 4) ℝ` to `Matrix (Fin 4) (Fin 4) ℝ` whose kernal is +the Lorentz group. -/ def kernalMap : C(GL (Fin 4) ℝ, Matrix (Fin 4) (Fin 4) ℝ) where toFun Λ := η * Λ.1ᵀ * η * Λ.1 continuous_toFun := by diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean index 2de9a49..a0c35ea 100644 --- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean +++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean @@ -34,7 +34,7 @@ namespace lorentzGroup open FourVelocity - +/-- An auxillary linear map used in the definition of a genearlised boost. -/ def genBoostAux₁ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where toFun x := (2 * ηLin x u) • v.1.1 map_add' x y := by @@ -45,7 +45,7 @@ def genBoostAux₁ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where RingHom.id_apply] rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul] - +/-- An auxillary linear map used in the definition of a genearlised boost. -/ def genBoostAux₂ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where toFun x := - (ηLin x (u + v) / (1 + ηLin u v)) • (u + v) map_add' x y := by @@ -60,6 +60,8 @@ def genBoostAux₂ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul] rfl +/-- An genearlised boost. This is a Lorentz transformation which takes the four velocity `u` +to `v`. -/ def genBoost (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime := LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v @@ -81,6 +83,7 @@ lemma self (u : FourVelocity) : genBoost u u = LinearMap.id := by ring rfl +/-- A generalised boost as a matrix. -/ def toMatrix (u v : FourVelocity) : Matrix (Fin 4) (Fin 4) ℝ := LinearMap.toMatrix stdBasis stdBasis (genBoost u v) @@ -124,7 +127,6 @@ lemma toMatrix_continuous (u : FourVelocity) : Continuous (toMatrix u) := by exact fun x => one_plus_ne_zero u x - lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u v) := by intro x y rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂] @@ -136,6 +138,7 @@ lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u rw [u.1.2, v.1.2, ηLin_symm v u, ηLin_symm u y, ηLin_symm v y] ring +/-- A generalised boost as an element of the Lorentz Group. -/ def toLorentz (u v : FourVelocity) : lorentzGroup := PreservesηLin.liftLor (toMatrix_PreservesηLin u v) diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean index 75b9c9f..832953f 100644 --- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean +++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean @@ -46,23 +46,25 @@ def fstCol (Λ : lorentzGroup) : PreFourVelocity := ⟨Λ.1 *ᵥ stdBasis 0, by rw [← h00] ring⟩ +/-- A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative. -/ def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0 lemma IsOrthochronous_iff_transpose (Λ : lorentzGroup) : IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by - simp [IsOrthochronous] - simp [transpose] + simp only [IsOrthochronous, Fin.isValue, transpose, PreservesηLin.liftLor, PreservesηLin.liftGL, + transpose_transpose, transpose_apply] lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) : IsOrthochronous Λ ↔ IsFourVelocity (fstCol Λ) := by simp [IsOrthochronous, IsFourVelocity] rw [stdBasis_mulVec] +/-- The continuous map taking a Lorentz transformation to its `0 0` element. -/ def mapZeroZeroComp : C(lorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0, by refine Continuous.matrix_elem ?_ 0 0 refine Continuous.comp' Units.continuous_val continuous_subtype_val⟩ - +/-- An auxillary function used in the definition of `orthchroMapReal`. -/ def stepFunction : ℝ → ℝ := fun t => if t ≤ -1 then -1 else if 1 ≤ t then 1 else t @@ -78,6 +80,8 @@ lemma stepFunction_continuous : Continuous stepFunction := by rw [Set.Ici_def, @frontier_Ici, @Set.mem_singleton_iff] at ha simp [ha] +/-- The continuous map from `lorentzGroup` to `ℝ` wh +taking Orthochronous elements to `1` and non-orthochronous to `-1`. -/ def orthchroMapReal : C(lorentzGroup, ℝ) := ContinuousMap.comp ⟨stepFunction, stepFunction_continuous⟩ mapZeroZeroComp @@ -108,6 +112,7 @@ lemma orthchroMapReal_minus_one_or_one (Λ : lorentzGroup) : local notation "ℤ₂" => Multiplicative (ZMod 2) +/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/ def orthchroMap : C(lorentzGroup, ℤ₂) := ContinuousMap.comp coeForℤ₂ { toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩, @@ -127,7 +132,7 @@ lemma zero_zero_mul (Λ Λ' : lorentzGroup) : ⟪(fstCol (transpose Λ)).1.space, (fstCol Λ').1.space⟫_ℝ := by rw [@Subgroup.coe_mul, @GeneralLinearGroup.coe_mul, mul_apply, Fin.sum_univ_four] rw [@PiLp.inner_apply, Fin.sum_univ_three] - simp [transpose, stdBasis_mulVec] + simp [transpose, stdBasis_mulVec, PreservesηLin.liftLor, PreservesηLin.liftGL] ring lemma mul_othchron_of_othchron_othchron {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ) @@ -164,24 +169,25 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬ rw [zero_zero_mul] exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h' +/-- The representation from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/ def orthchroRep : lorentzGroup →* ℤ₂ where toFun := orthchroMap map_one' := by have h1 : IsOrthochronous 1 := by simp [IsOrthochronous] rw [orthchroMap_IsOrthochronous h1] map_mul' Λ Λ' := by - simp + simp only by_cases h : IsOrthochronous Λ <;> by_cases h' : IsOrthochronous Λ' rw [orthchroMap_IsOrthochronous h, orthchroMap_IsOrthochronous h', orthchroMap_IsOrthochronous (mul_othchron_of_othchron_othchron h h')] - simp + simp only [mul_one] rw [orthchroMap_IsOrthochronous h, orthchroMap_not_IsOrthochronous h', orthchroMap_not_IsOrthochronous (mul_not_othchron_of_othchron_not_othchron h h')] - simp + simp only [Nat.reduceAdd, one_mul] rw [orthchroMap_not_IsOrthochronous h, orthchroMap_IsOrthochronous h', orthchroMap_not_IsOrthochronous (mul_not_othchron_of_not_othchron_othchron h h')] - simp + simp only [Nat.reduceAdd, mul_one] rw [orthchroMap_not_IsOrthochronous h, orthchroMap_not_IsOrthochronous h', orthchroMap_IsOrthochronous (mul_othchron_of_not_othchron_not_othchron h h')] simp only [Nat.reduceAdd] From 2195936a88475d159a1b873307c62f76f098979f Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:15 +0200 Subject: [PATCH 12/24] Update Basic.lean --- HepLean/AnomalyCancellation/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index 382bcb7..651118c 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -77,7 +77,7 @@ namespace ACCSystemLinear structure LinSols (χ : ACCSystemLinear) where /-- The underlying charge. -/ val : χ.1.charges - /-- The condition that the charge satifies the linear ACCs. -/ + /-- The condition that the charge satisfies the linear ACCs. -/ linearSol : ∀ i : Fin χ.numberLinear, χ.linearACCs i val = 0 /-- Two solutions are equal if the underlying charges are equal. -/ @@ -172,7 +172,7 @@ namespace ACCSystemQuad /-- The type of solutions to the linear and quadratic ACCs. -/ structure QuadSols (χ : ACCSystemQuad) extends χ.LinSols where - /-- The condition that the charge satifies the quadratic ACCs. -/ + /-- The condition that the charge satisfies the quadratic ACCs. -/ quadSol : ∀ i : Fin χ.numberQuadratic, (χ.quadraticACCs i) val = 0 /-- Two `QuadSols` are equal if the underlying charges are equal. -/ @@ -225,7 +225,7 @@ namespace ACCSystem /-- The type of solutions to the anomaly cancellation conditions. -/ structure Sols (χ : ACCSystem) extends χ.QuadSols where - /-- The condition that the charge satifies the cubic ACC. -/ + /-- The condition that the charge satisfies the cubic ACC. -/ cubicSol : χ.cubicACC val = 0 /-- Two solutions are equal if the underlying charges are equal. -/ From 718b1049d123e54f4f1089ac766e2134e3e43965 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:16 +0200 Subject: [PATCH 13/24] Update Basic.lean --- HepLean/AnomalyCancellation/MSSMNu/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean index 839e1d9..1b8ce7c 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean @@ -206,7 +206,7 @@ lemma accSU2_ext {S T : MSSMCharges.charges} rw [hd, hu] rfl -/-- The anomaly cancelation condition for SU(3) anomaly. -/ +/-- The anomaly cancellation condition for SU(3) anomaly. -/ @[simp] def accSU3 : MSSMCharges.charges →ₗ[ℚ] ℚ where toFun S := ∑ i, (2 * (Q S i) + (U S i) + (D S i)) From 1e0a0487a0ff2b1c2b1745052f6a65d7238ae3b1 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:18 +0200 Subject: [PATCH 14/24] Update HyperCharge.lean --- HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean index 8af33de..23268af 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean @@ -8,7 +8,7 @@ import Mathlib.Tactic.Polyrith /-! # Hypercharge in MSSM. -Relavent definitions for the MSSM hypercharge. +Relevant definitions for the MSSM hypercharge. -/ From 1da2fd17382e80ed58679b1cb9e1af7540f937ea Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:21 +0200 Subject: [PATCH 15/24] Update LineInCubic.lean --- HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean index 834dc5b..db47ec0 100644 --- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean +++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean @@ -67,7 +67,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) - (lineInCubic_expand h g f hS 1 2) / 6 -/-- We say a `LinSol` satifies `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/ +/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/ def lineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop := ∀ (M : (FamilyPermutations (2 * n.succ)).group ), lineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S) From 90deb528a2a73863412ffabf5777f17b0a37c1d3 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:22 +0200 Subject: [PATCH 16/24] Update LineInPlaneCond.lean --- HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean index 3d87877..8ea80f4 100644 --- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean +++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean @@ -12,7 +12,7 @@ import Mathlib.RepresentationTheory.Basic /-! # Line in plane condition -We say a `LinSol` satifies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in +We say a `LinSol` satisfies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in `Fin n`, we have `S i1 = S i2` or `S i1 = - S i2` or `2 S i3 + S i1 + S i2 = 0`. @@ -21,7 +21,7 @@ The main reference for this material is - https://arxiv.org/pdf/1912.04804.pdf -We will show that `n ≥ 4` the `line in plane` condition on solutions inplies the +We will show that `n ≥ 4` the `line in plane` condition on solutions implies the `constAbs` condition. -/ From a25dcb4d9c0ec84e95fd6a344a2f2b8089c39b74 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:24 +0200 Subject: [PATCH 17/24] Update BasisLinear.lean --- HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean index ef0361d..30c7570 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean @@ -10,7 +10,7 @@ import Mathlib.Logic.Equiv.Fin /-! # Basis of `LinSols` in the odd case -We give a basis of `LinSols` in the odd case. This basis has the special propoerty +We give a basis of `LinSols` in the odd case. This basis has the special property that splits into two planes on which every point is a solution to the ACCs. -/ universe v u From c768e660a1590272d540546eb7f0d16e8f635c64 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:25 +0200 Subject: [PATCH 18/24] Update LineInCubic.lean --- HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean index d7a9000..d5153b5 100644 --- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean +++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean @@ -16,10 +16,10 @@ import Mathlib.RepresentationTheory.Basic # Line In Cubic Odd case We say that a linear solution satisfies the `lineInCubic` property -if the line through that point and through the two different planes formed by the baisis of +if the line through that point and through the two different planes formed by the basis of `LinSols` lies in the cubic. -We show that for a solution all its permutations satsfiy this property, +We show that for a solution all its permutations satisfy this property, then the charge must be zero. The main reference for this file is: @@ -34,7 +34,7 @@ open BigOperators variable {n : ℕ} open VectorLikeOddPlane -/-- A property on `LinSols`, statified if every point on the line between the two planes +/-- A property on `LinSols`, satisfied if every point on the line between the two planes in the basis through that point is in the cubic. -/ def lineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop := ∀ (g f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) , @@ -64,7 +64,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S -/-- We say a `LinSol` satifies `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/ +/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/ def lineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop := ∀ (M : (FamilyPermutations (2 * n + 1)).group ), lineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S) From a368679152e51e33692309fa10f515285d64d54c Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:28 +0200 Subject: [PATCH 19/24] Update Basic.lean --- HepLean/AnomalyCancellation/SM/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean index cd71230..5f68cc6 100644 --- a/HepLean/AnomalyCancellation/SM/Basic.lean +++ b/HepLean/AnomalyCancellation/SM/Basic.lean @@ -13,7 +13,7 @@ import Mathlib.Logic.Equiv.Fin /-! # Anomaly cancellation conditions for n family SM. -We define the ACC system for the Standard Model with`n`-famlies and no RHN. +We define the ACC system for the Standard Model with`n`-families and no RHN. -/ @@ -21,7 +21,7 @@ universe v u open Nat open BigOperators -/-- Aassociate to each (including RHN) SM fermion a set of charges-/ +/-- Associate to each (including RHN) SM fermion a set of charges-/ @[simps!] def SMCharges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk (5 * n) From 7515fde40251735fa2b3350183fc1cd07db369df Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:30 +0200 Subject: [PATCH 20/24] Update FamilyMaps.lean --- HepLean/AnomalyCancellation/SM/FamilyMaps.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean index 2dc75d6..37c5bae 100644 --- a/HepLean/AnomalyCancellation/SM/FamilyMaps.lean +++ b/HepLean/AnomalyCancellation/SM/FamilyMaps.lean @@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SM.Basic /-! # Family maps for the Standard Model ACCs -We define the a series of maps between the charges for different numbers of famlies. +We define the a series of maps between the charges for different numbers of families. -/ @@ -84,7 +84,7 @@ other charges zero. -/ def familyEmbedding (m n : ℕ) : (SMCharges m).charges →ₗ[ℚ] (SMCharges n).charges := chargesMapOfSpeciesMap (speciesEmbed m n) -/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in +/-- For species, the embedding of the `1`-family charges into the `n`-family charges in a universal manor. -/ @[simps!] def speciesFamilyUniversial (n : ℕ) : @@ -98,7 +98,7 @@ def speciesFamilyUniversial (n : ℕ) : simp [HSMul.hSMul] --rw [show Rat.cast a = a from rfl] -/-- The embeddding of the `1`-family charges into the `n`-family charges in +/-- The embedding of the `1`-family charges into the `n`-family charges in a universal manor. -/ def familyUniversal ( n : ℕ) : (SMCharges 1).charges →ₗ[ℚ] (SMCharges n).charges := chargesMapOfSpeciesMap (speciesFamilyUniversial n) From e77dd4b09877d8b770cccbde482a8e8275272cae Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:31 +0200 Subject: [PATCH 21/24] Update Lemmas.lean --- HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean index e24ce3a..6288867 100644 --- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean +++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean @@ -12,7 +12,7 @@ import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization The main result of this file is the conclusion of this paper: https://arxiv.org/abs/1907.00514 -That eveery solution to the ACCs without gravity satifies for free the gravitational anomaly. +That eveery solution to the ACCs without gravity satisfies for free the gravitational anomaly. -/ universe v u @@ -67,7 +67,7 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0 rw [← hS'] exact S'.grav_of_cubic hC FLTThree -/-- Any solution to the ACCs without gravity satifies the gravitational ACC. -/ +/-- Any solution to the ACCs without gravity satisfies the gravitational ACC. -/ theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWith ℚ 3) : accGrav S.val = 0 := by by_cases hQ : Q S.val (0 : Fin 1)= 0 From 1cd9dd3ed4ef5b422aa9d923963bc7566a257a93 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:34 +0200 Subject: [PATCH 22/24] Update FamilyMaps.lean --- HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean index 8ffd5e8..1c11dca 100644 --- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean +++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean @@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.SMNu.Basic /-! # Family maps for the Standard Model for RHN ACCs -We define the a series of maps between the charges for different numbers of famlies. +We define the a series of maps between the charges for different numbers of families. -/ @@ -89,7 +89,7 @@ other charges zero. -/ def familyEmbedding (m n : ℕ) : (SMνCharges m).charges →ₗ[ℚ] (SMνCharges n).charges := chargesMapOfSpeciesMap (speciesEmbed m n) -/-- For species, the embeddding of the `1`-family charges into the `n`-family charges in +/-- For species, the embedding of the `1`-family charges into the `n`-family charges in a universal manor. -/ @[simps!] def speciesFamilyUniversial (n : ℕ) : @@ -103,7 +103,7 @@ def speciesFamilyUniversial (n : ℕ) : simp [HSMul.hSMul] -- rw [show Rat.cast a = a from rfl] -/-- The embeddding of the `1`-family charges into the `n`-family charges in +/-- The embedding of the `1`-family charges into the `n`-family charges in a universal manor. -/ def familyUniversal (n : ℕ) : (SMνCharges 1).charges →ₗ[ℚ] (SMνCharges n).charges := chargesMapOfSpeciesMap (speciesFamilyUniversial n) From ee3c7580b58a479b3de5c44e30f7a7c44abfe64b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 20 May 2024 00:19:36 +0200 Subject: [PATCH 23/24] Update Basic.lean --- HepLean/FlavorPhysics/CKMMatrix/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean index 36cba92..611612e 100644 --- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean +++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean @@ -9,7 +9,7 @@ import Mathlib.Tactic.Polyrith /-! # The CKM Matrix -The definition of the type of CKM matries as unitary $3×3$-matries. +The definition of the type of CKM matrices as unitary $3×3$-matrices. An equivalence relation on CKM matrices is defined, where two matrices are equivalent if they are related by phase shifts. From 68888861b976b7c798db3f36321a40053fae1896 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 20 May 2024 08:13:59 -0400 Subject: [PATCH 24/24] Update README.md --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 9712d0d..72011f3 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,9 @@ # High Energy Physics in Lean +[![](https://img.shields.io/badge/Read_The-Docs-green)](https://heplean.github.io/HepLean/) +[![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls) +[![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com) + A project to digitalize high energy physics. ## Aims of this project