From 675b9a989a4d3f142c67d682ef68b22ea477e83a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 1 Jul 2024 16:56:15 -0400 Subject: [PATCH 1/6] refactor: Major refactor of lorentz group --- HepLean/SpaceTime/Basic.lean | 1 - HepLean/SpaceTime/LorentzGroup/Basic.lean | 227 +++++++------ HepLean/SpaceTime/LorentzGroup/Boosts.lean | 31 +- .../SpaceTime/LorentzGroup/Orthochronous.lean | 146 ++++----- HepLean/SpaceTime/LorentzGroup/Proper.lean | 38 ++- HepLean/SpaceTime/LorentzTensors/Basic.lean | 17 + HepLean/SpaceTime/LorentzVector/Basic.lean | 116 +++++++ HepLean/SpaceTime/LorentzVector/NormOne.lean | 172 ++++++++++ HepLean/SpaceTime/Metric.lean | 6 + HepLean/SpaceTime/MinkowskiMetric.lean | 307 ++++++++++++++++++ docs/references.bib | 13 +- 11 files changed, 866 insertions(+), 208 deletions(-) create mode 100644 HepLean/SpaceTime/LorentzTensors/Basic.lean create mode 100644 HepLean/SpaceTime/LorentzVector/Basic.lean create mode 100644 HepLean/SpaceTime/LorentzVector/NormOne.lean create mode 100644 HepLean/SpaceTime/MinkowskiMetric.lean diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean index c625e93..fae801a 100644 --- a/HepLean/SpaceTime/Basic.lean +++ b/HepLean/SpaceTime/Basic.lean @@ -22,7 +22,6 @@ def SpaceTime : Type := Fin 4 → ℝ /-- Give spacetime the structure of an additive commutative monoid. -/ instance : AddCommMonoid SpaceTime := Pi.addCommMonoid - /-- Give spacetime the structure of a module over the reals. -/ instance : Module ℝ SpaceTime := Pi.module _ _ _ diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index 9eaa8dc..446a3b9 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -3,8 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import HepLean.SpaceTime.Metric +import HepLean.SpaceTime.MinkowskiMetric import HepLean.SpaceTime.AsSelfAdjointMatrix +import HepLean.SpaceTime.LorentzVector.NormOne /-! # The Lorentz Group @@ -26,7 +27,6 @@ identity. noncomputable section -namespace SpaceTime open Manifold open Matrix @@ -34,146 +34,139 @@ open Complex open ComplexConjugate /-! -## Matrices which preserve `ηLin` +## Matrices which preserves the Minkowski metric We start studying the properties of matrices which preserve `ηLin`. These matrices form the Lorentz group, which we will define in the next section at `lorentzGroup`. -/ +variable {d : ℕ} -/-- 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 +open minkowskiMetric in +/-- The Lorentz group is the subset of matrices which preserve the minkowski metric. -/ +def LorentzGroup (d : ℕ) : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) := + {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ | + ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ} -namespace PreservesηLin -variable (Λ : Matrix (Fin 4) (Fin 4) ℝ) +namespace LorentzGroup +/-- Notation for the Lorentz group. -/ +scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup -lemma iff_norm : PreservesηLin Λ ↔ - ∀ (x : SpaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ x) = ηLin x x := by +open minkowskiMetric + +variable {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} + +/-! + +# Membership conditions + +-/ + +lemma mem_iff_norm : Λ ∈ LorentzGroup d ↔ + ∀ (x : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ x⟫ₘ = ⟪x, x⟫ₘ := by refine Iff.intro (fun h x => h x x) (fun h x y => ?_) have hp := h (x + y) have hn := h (x - y) rw [mulVec_add] at hp rw [mulVec_sub] at hn simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn - rw [ηLin_symm (Λ *ᵥ y) (Λ *ᵥ x), ηLin_symm y x] at hp hn + rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn linear_combination hp / 4 + -1 * hn / 4 -lemma iff_det_selfAdjoint : PreservesηLin Λ ↔ - ∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)), - det ((toSelfAdjointMatrix ∘ toLin stdBasis stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1 - = det x.1 := by - rw [iff_norm] - apply Iff.intro - intro h x - have h1 := congrArg ofReal $ h (toSelfAdjointMatrix.symm x) - simpa [← det_eq_ηLin] using h1 - intro h x - have h1 := h (toSelfAdjointMatrix x) - simpa [det_eq_ηLin] using h1 - -lemma iff_on_right : PreservesηLin Λ ↔ - ∀ (x y : SpaceTime), ηLin x ((η * Λᵀ * η * Λ) *ᵥ y) = ηLin x y := by +lemma mem_iff_on_right : Λ ∈ LorentzGroup d ↔ + ∀ (x y : LorentzVector d), ⟪x, (dual Λ * Λ) *ᵥ y⟫ₘ = ⟪x, y⟫ₘ := by apply Iff.intro intro h x y have h1 := h x y - rw [ηLin_mulVec_left, mulVec_mulVec] at h1 + rw [← dual_mulVec_right, mulVec_mulVec] at h1 exact h1 intro h x y - rw [ηLin_mulVec_left, mulVec_mulVec] + rw [← dual_mulVec_right, 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] - · exact fun a x y => Eq.symm (Real.ext_cauchy (congrArg Real.cauchy (a x y))) +lemma mem_iff_dual_mul_self : Λ ∈ LorentzGroup d ↔ dual Λ * Λ = 1 := by + rw [mem_iff_on_right, matrix_eq_id_iff] + exact forall_comm -lemma iff_matrix' : PreservesηLin Λ ↔ Λ * (η * Λᵀ * η) = 1 := by - rw [iff_matrix] +lemma mem_iff_self_mul_dual : Λ ∈ LorentzGroup d ↔ Λ * dual Λ = 1 := by + rw [mem_iff_dual_mul_self] exact mul_eq_one_comm -lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by +lemma mem_iff_transpose : Λ ∈ LorentzGroup d ↔ Λᵀ ∈ LorentzGroup d := 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] - noncomm_ring - 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] + · intro h + have h1 := congrArg transpose ((mem_iff_dual_mul_self).mp h) + rw [dual, transpose_mul, transpose_mul, transpose_mul, minkowskiMatrix.eq_transpose, + ← mul_assoc, transpose_one] at h1 + rw [mem_iff_self_mul_dual, ← h1, dual] + noncomm_ring + · intro h + have h1 := congrArg transpose ((mem_iff_dual_mul_self).mp h) + rw [dual, transpose_mul, transpose_mul, transpose_mul, minkowskiMatrix.eq_transpose, + ← mul_assoc, transpose_one, transpose_transpose] at h1 + rw [mem_iff_self_mul_dual, ← h1, dual] + noncomm_ring + +lemma mem_mul (hΛ : Λ ∈ LorentzGroup d) (hΛ' : Λ' ∈ LorentzGroup d) : Λ * Λ' ∈ LorentzGroup d := by + rw [mem_iff_dual_mul_self, dual_mul] + trans dual Λ' * (dual Λ * Λ) * Λ' noncomm_ring + rw [(mem_iff_dual_mul_self).mp hΛ] + simp [(mem_iff_dual_mul_self).mp hΛ'] -/-- 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⟩ - -lemma mul {Λ Λ' : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) (h' : PreservesηLin Λ') : - PreservesηLin (Λ * Λ') := by - intro x y - rw [← mulVec_mulVec, ← mulVec_mulVec, h, h'] - -lemma one : PreservesηLin 1 := by - intro x y +lemma one_mem : 1 ∈ LorentzGroup d := by + rw [mem_iff_dual_mul_self] simp -lemma η : PreservesηLin η := by - simp [iff_matrix, η_transpose, η_sq] +lemma dual_mem (h : Λ ∈ LorentzGroup d) : dual Λ ∈ LorentzGroup d := by + rw [mem_iff_dual_mul_self, dual_dual] + exact mem_iff_self_mul_dual.mp h -end PreservesηLin +end LorentzGroup /-! -## The Lorentz group -We define the Lorentz group as the set of matrices which preserve `ηLin`. -We show that the Lorentz group is indeed a group. +# The Lorentz group as a group -/ -/-- The Lorentz group is the subset of matrices which preserve ηLin. -/ -def LorentzGroup : Type := {Λ : Matrix (Fin 4) (Fin 4) ℝ // PreservesηLin Λ} - @[simps mul_coe one_coe inv div] -instance lorentzGroupIsGroup : Group LorentzGroup where - mul A B := ⟨A.1 * B.1, PreservesηLin.mul A.2 B.2⟩ +instance lorentzGroupIsGroup : Group (LorentzGroup d) where + mul A B := ⟨A.1 * B.1, LorentzGroup.mem_mul A.2 B.2⟩ mul_assoc A B C := by apply Subtype.eq exact Matrix.mul_assoc A.1 B.1 C.1 - one := ⟨1, PreservesηLin.one⟩ + one := ⟨1, LorentzGroup.one_mem⟩ one_mul A := by apply Subtype.eq exact Matrix.one_mul A.1 mul_one A := by apply Subtype.eq exact Matrix.mul_one A.1 - inv A := ⟨η * A.1ᵀ * η , PreservesηLin.mul (PreservesηLin.mul PreservesηLin.η - ((PreservesηLin.iff_transpose A.1).mp A.2)) PreservesηLin.η⟩ + inv A := ⟨minkowskiMetric.dual A.1, LorentzGroup.dual_mem A.2⟩ mul_left_inv A := by apply Subtype.eq - exact (PreservesηLin.iff_matrix A.1).mp A.2 + exact LorentzGroup.mem_iff_dual_mul_self.mp A.2 -/-- Notation for the Lorentz group. -/ -scoped[SpaceTime] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup - - -/-- `lorentzGroup` has the subtype topology. -/ -instance : TopologicalSpace LorentzGroup := instTopologicalSpaceSubtype +/-- `LorentzGroup` has the subtype topology. -/ +instance : TopologicalSpace (LorentzGroup d) := instTopologicalSpaceSubtype namespace LorentzGroup -lemma coe_inv (A : LorentzGroup) : (A⁻¹).1 = A.1⁻¹:= by +open minkowskiMetric + +variable {Λ Λ' : LorentzGroup d} + +@[simp] +lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= by refine (inv_eq_left_inv ?h).symm - exact (PreservesηLin.iff_matrix A.1).mp A.2 + exact mem_iff_dual_mul_self.mp Λ.2 /-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/ -def transpose (Λ : LorentzGroup) : LorentzGroup := ⟨Λ.1ᵀ, (PreservesηLin.iff_transpose Λ.1).mp Λ.2⟩ +def transpose (Λ : LorentzGroup d) : LorentzGroup d := + ⟨Λ.1ᵀ, mem_iff_transpose.mp Λ.2⟩ /-! @@ -186,9 +179,9 @@ embedding. -/ /-- The homomorphism of the Lorentz group into `GL (Fin 4) ℝ`. -/ -def toGL : LorentzGroup →* GL (Fin 4) ℝ where - toFun A := ⟨A.1, (A⁻¹).1, mul_eq_one_comm.mpr $ (PreservesηLin.iff_matrix A.1).mp A.2, - (PreservesηLin.iff_matrix A.1).mp A.2⟩ +def toGL : LorentzGroup d →* GL (Fin 1 ⊕ Fin d) ℝ where + toFun A := ⟨A.1, (A⁻¹).1, mul_eq_one_comm.mpr $ mem_iff_dual_mul_self.mp A.2, + mem_iff_dual_mul_self.mp A.2⟩ map_one' := by simp rfl @@ -197,7 +190,7 @@ def toGL : LorentzGroup →* GL (Fin 4) ℝ where ext rfl -lemma toGL_injective : Function.Injective toGL := by +lemma toGL_injective : Function.Injective (@toGL d) := by intro A B h apply Subtype.eq rw [@Units.ext_iff] at h @@ -206,20 +199,21 @@ lemma toGL_injective : Function.Injective toGL := by /-- The homomorphism from the Lorentz Group into the monoid of matrices times the opposite of the monoid of matrices. -/ @[simps!] -def toProd : LorentzGroup →* (Matrix (Fin 4) (Fin 4) ℝ) × (Matrix (Fin 4) (Fin 4) ℝ)ᵐᵒᵖ := +def toProd : LorentzGroup d →* (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) × + (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)ᵐᵒᵖ := MonoidHom.comp (Units.embedProduct _) toGL -lemma toProd_eq_transpose_η : toProd A = (A.1, ⟨η * A.1ᵀ * η⟩) := rfl +lemma toProd_eq_transpose_η : toProd Λ = (Λ.1, MulOpposite.op $ minkowskiMetric.dual Λ.1) := rfl -lemma toProd_injective : Function.Injective toProd := by +lemma toProd_injective : Function.Injective (@toProd d) := by intro A B h rw [toProd_eq_transpose_η, toProd_eq_transpose_η] at h rw [@Prod.mk.inj_iff] at h apply Subtype.eq exact h.1 -lemma toProd_continuous : Continuous toProd := by - change Continuous (fun A => (A.1, ⟨η * A.1ᵀ * η⟩)) +lemma toProd_continuous : Continuous (@toProd d) := by + change Continuous (fun A => (A.1, ⟨dual A.1⟩)) refine continuous_prod_mk.mpr (And.intro ?_ ?_) exact continuous_iff_le_induced.mpr fun U a => a refine Continuous.comp' ?_ ?_ @@ -230,7 +224,7 @@ lemma toProd_continuous : Continuous toProd := by /-- The embedding from the Lorentz Group into the monoid of matrices times the opposite of the monoid of matrices. -/ -lemma toProd_embedding : Embedding toProd where +lemma toProd_embedding : Embedding (@toProd d) where inj := toProd_injective induced := by refine (inducing_iff ⇑toProd).mp ?_ @@ -238,7 +232,7 @@ lemma toProd_embedding : Embedding toProd where exact (inducing_iff (Prod.fst ∘ ⇑toProd)).mpr rfl /-- The embedding from the Lorentz Group into `GL (Fin 4) ℝ`. -/ -lemma toGL_embedding : Embedding toGL.toFun where +lemma toGL_embedding : Embedding (@toGL d).toFun where inj := toGL_injective induced := by refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm @@ -248,11 +242,48 @@ lemma toGL_embedding : Embedding toGL.toFun where exact exists_exists_and_eq_and -instance : TopologicalGroup LorentzGroup := Inducing.topologicalGroup toGL toGL_embedding.toInducing +instance : TopologicalGroup (LorentzGroup d) := +Inducing.topologicalGroup toGL toGL_embedding.toInducing + +section +open LorentzVector +/-! + +# To a norm one Lorentz vector + +-/ + +/-- The first column of a lorentz matrix as a `NormOneLorentzVector`. -/ +@[simps!] +def toNormOneLorentzVector (Λ : LorentzGroup d) : NormOneLorentzVector d := + ⟨Λ.1 *ᵥ timeVec, by rw [NormOneLorentzVector.mem_iff, Λ.2, minkowskiMetric.on_timeVec]⟩ + +/-! + +# The time like element + +-/ + +/-- The time like element of a Lorentz matrix. -/ +@[simp] +def timeComp (Λ : LorentzGroup d) : ℝ := Λ.1 (Sum.inl 0) (Sum.inl 0) + +lemma timeComp_eq_toNormOneLorentzVector : timeComp Λ = (toNormOneLorentzVector Λ).1.time := by + simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue, timeComp] + erw [Pi.basisFun_apply, mulVec_stdBasis] + +lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') = + ⟪toNormOneLorentzVector (transpose Λ), (toNormOneLorentzVector Λ').1.spaceReflection⟫ₘ := by + simp only [timeComp, Fin.isValue, lorentzGroupIsGroup_mul_coe, mul_apply, Fintype.sum_sum_type, + Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, toNormOneLorentzVector, + transpose, timeVec, right_spaceReflection, time, space, PiLp.inner_apply, Function.comp_apply, + RCLike.inner_apply, conj_trivial] + erw [Pi.basisFun_apply, mulVec_stdBasis] + simp + + +end end LorentzGroup - - -end SpaceTime diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean index 1d49d9e..a11246a 100644 --- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean +++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzGroup.Proper import Mathlib.Topology.Constructions -import HepLean.SpaceTime.FourVelocity +import HepLean.SpaceTime.LorentzVector.NormOne /-! # Boosts @@ -28,15 +28,17 @@ A boost is the special case of a generalised boost when `u = stdBasis 0`. -/ noncomputable section -namespace SpaceTime namespace LorentzGroup -open FourVelocity +open NormOneLorentzVector +open minkowskiMetric + +variable {d : ℕ} /-- An auxillary linear map used in the definition of a generalised boost. -/ -def genBoostAux₁ (u v : FourVelocity) : SpaceTime →ₗ[ℝ] SpaceTime where - toFun x := (2 * ηLin x u) • v.1.1 +def genBoostAux₁ (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] LorentzVector d where + toFun x := (2 * ⟪x, u⟫ₘ) • v.1.1 map_add' x y := by simp only [map_add, LinearMap.add_apply] rw [mul_add, add_smul] @@ -46,17 +48,21 @@ def genBoostAux₁ (u v : FourVelocity) : SpaceTime →ₗ[ℝ] SpaceTime where 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) +def genBoostAux₂ (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] LorentzVector d where + toFun x := - (⟪x, u.1.1 + v⟫ₘ / (1 + ⟪u.1.1, v⟫ₘ)) • (u.1.1 + 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] + rw [← add_smul] + apply congrFun + apply congrArg + field_simp + apply congrFun + apply congrArg + ring 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 [map_smul] + rw [show (c • minkowskiMetric x) (↑u + ↑v) = c * minkowskiMetric x (u+v) from rfl] rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul] rfl @@ -174,5 +180,4 @@ end genBoost end LorentzGroup -end SpaceTime end diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean index 3f26bc2..7719ec4 100644 --- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean +++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean @@ -3,7 +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.LorentzVector.NormOne import HepLean.SpaceTime.LorentzGroup.Proper /-! # The Orthochronous Lorentz Group @@ -20,7 +20,6 @@ matrices. noncomputable section -namespace SpaceTime open Manifold open Matrix @@ -28,37 +27,50 @@ open Complex open ComplexConjugate namespace LorentzGroup -open PreFourVelocity -/-- 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 Λ.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 [η_explicit, 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 - exact h00⟩ +variable {d : ℕ} +variable (Λ : LorentzGroup d) +open LorentzVector +open minkowskiMetric /-- A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative. -/ -def IsOrthochronous (Λ : LorentzGroup) : Prop := 0 ≤ Λ.1 0 0 +def IsOrthochronous : Prop := 0 ≤ timeComp Λ -lemma IsOrthochronous_iff_transpose (Λ : LorentzGroup) : +lemma IsOrthochronous_iff_futurePointing : + IsOrthochronous Λ ↔ (toNormOneLorentzVector Λ) ∈ NormOneLorentzVector.FuturePointing d := by + simp only [IsOrthochronous, timeComp_eq_toNormOneLorentzVector] + rw [NormOneLorentzVector.FuturePointing.mem_iff_time_nonneg] + +lemma IsOrthochronous_iff_transpose : IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by rfl -lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : LorentzGroup) : - IsOrthochronous Λ ↔ IsFourVelocity (fstCol Λ) := by - simp [IsOrthochronous, IsFourVelocity] - rw [stdBasis_mulVec] +lemma IsOrthochronous_iff_ge_one : + IsOrthochronous Λ ↔ 1 ≤ timeComp Λ := by + rw [IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.mem_iff, + NormOneLorentzVector.time_pos_iff] + simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue] + erw [Pi.basisFun_apply, mulVec_stdBasis] + rfl + +lemma not_orthochronous_iff_le_neg_one : + ¬ IsOrthochronous Λ ↔ timeComp Λ ≤ -1 := by + rw [timeComp, IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.not_mem_iff, + NormOneLorentzVector.time_nonpos_iff] + simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue] + erw [Pi.basisFun_apply, mulVec_stdBasis] + +lemma not_orthochronous_iff_le_zero : + ¬ IsOrthochronous Λ ↔ timeComp Λ ≤ 0 := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + rw [not_orthochronous_iff_le_neg_one] at h + linarith + rw [IsOrthochronous_iff_ge_one] + linarith + /-- The continuous map taking a Lorentz transformation to its `0 0` element. -/ -def mapZeroZeroComp : C(LorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0, - Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) 0 0⟩ +def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => timeComp Λ , + Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩ /-- An auxillary function used in the definition of `orthchroMapReal`. -/ def stepFunction : ℝ → ℝ := fun t => @@ -78,29 +90,23 @@ lemma stepFunction_continuous : Continuous stepFunction := by /-- 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 +def orthchroMapReal : C(LorentzGroup d, ℝ) := ContinuousMap.comp + ⟨stepFunction, stepFunction_continuous⟩ timeCompCont -lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup} (h : IsOrthochronous Λ) : +lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup d} (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] + rw [IsOrthochronous_iff_ge_one, timeComp] at h + change stepFunction (Λ.1 _ _) = 1 + rw [stepFunction, if_pos h, if_neg] + linarith - -lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup} (h : ¬ IsOrthochronous Λ) : +lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup d} (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 [not_orthochronous_iff_le_neg_one] at h + change stepFunction (timeComp _)= - 1 rw [stepFunction, if_pos h] -lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup) : +lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup d) : orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 := by by_cases h : IsOrthochronous Λ apply Or.inr $ orthchroMapReal_on_IsOrthochronous h @@ -109,65 +115,50 @@ 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, ℤ₂) := +def orthchroMap : C(LorentzGroup d, ℤ₂) := ContinuousMap.comp coeForℤ₂ { toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩, continuous_toFun := Continuous.subtype_mk (ContinuousMap.continuous orthchroMapReal) _} -lemma orthchroMap_IsOrthochronous {Λ : LorentzGroup} (h : IsOrthochronous Λ) : +lemma orthchroMap_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ) : orthchroMap Λ = 1 := by simp [orthchroMap, orthchroMapReal_on_IsOrthochronous h] -lemma orthchroMap_not_IsOrthochronous {Λ : LorentzGroup} (h : ¬ IsOrthochronous Λ) : +lemma orthchroMap_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) : orthchroMap Λ = Additive.toMul (1 : ZMod 2) := by simp [orthchroMap, orthchroMapReal_on_not_IsOrthochronous h] rfl -lemma zero_zero_mul (Λ Λ' : LorentzGroup) : - (Λ * Λ').1 0 0 = (fstCol (transpose Λ)).1 0 * (fstCol Λ').1 0 + - ⟪(fstCol (transpose Λ)).1.space, (fstCol Λ').1.space⟫_ℝ := by - simp only [Fin.isValue, lorentzGroupIsGroup_mul_coe, mul_apply, Fin.sum_univ_four, fstCol, - transpose, stdBasis_mulVec, transpose_apply, space, PiLp.inner_apply, Nat.succ_eq_add_one, - Nat.reduceAdd, RCLike.inner_apply, conj_trivial, Fin.sum_univ_three, cons_val_zero, - cons_val_one, head_cons, cons_val_two, tail_cons] - ring - -lemma mul_othchron_of_othchron_othchron {Λ Λ' : LorentzGroup} (h : IsOrthochronous Λ) +lemma mul_othchron_of_othchron_othchron {Λ Λ' : LorentzGroup d} (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' + rw [IsOrthochronous_iff_futurePointing] at h h' + rw [IsOrthochronous, timeComp_mul] + exact NormOneLorentzVector.FuturePointing.metric_reflect_mem_mem h h' -lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup} (h : ¬ IsOrthochronous Λ) +lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup d} (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' + rw [IsOrthochronous_iff_futurePointing] at h h' + rw [IsOrthochronous, timeComp_mul] + exact NormOneLorentzVector.FuturePointing.metric_reflect_not_mem_not_mem h h' -lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup} (h : IsOrthochronous Λ) +lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ) (h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by + rw [not_orthochronous_iff_le_zero, timeComp_mul] 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' + rw [IsOrthochronous_iff_futurePointing] at h h' + exact NormOneLorentzVector.FuturePointing.metric_reflect_mem_not_mem h h' -lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : LorentzGroup} (h : ¬ IsOrthochronous Λ) +lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : LorentzGroup d} (h : ¬ IsOrthochronous Λ) (h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by + rw [not_orthochronous_iff_le_zero, timeComp_mul] 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' + rw [IsOrthochronous_iff_futurePointing] at h h' + exact NormOneLorentzVector.FuturePointing.metric_reflect_not_mem_mem h h' /-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/ -def orthchroRep : LorentzGroup →* ℤ₂ where +def orthchroRep : LorentzGroup d →* ℤ₂ where toFun := orthchroMap map_one' := orthchroMap_IsOrthochronous (by simp [IsOrthochronous]) map_mul' Λ Λ' := by @@ -189,5 +180,4 @@ def orthchroRep : LorentzGroup →* ℤ₂ where end LorentzGroup -end SpaceTime end diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean index 67d4a1d..56b1ff7 100644 --- a/HepLean/SpaceTime/LorentzGroup/Proper.lean +++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean @@ -14,7 +14,6 @@ We define the give a series of lemmas related to the determinant of the lorentz noncomputable section -namespace SpaceTime open Manifold open Matrix @@ -23,10 +22,16 @@ open ComplexConjugate namespace LorentzGroup +open minkowskiMetric + +variable {d : ℕ} + /-- The determinant of a member of the lorentz group is `1` or `-1`. -/ -lemma det_eq_one_or_neg_one (Λ : 𝓛) : Λ.1.det = 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 Λ.2)) +lemma det_eq_one_or_neg_one (Λ : 𝓛 d) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by + have h1 := (congrArg det ((mem_iff_self_mul_dual).mp Λ.2)) + simp [det_mul, det_dual] at h1 + exact mul_self_eq_one_iff.mp h1 + local notation "ℤ₂" => Multiplicative (ZMod 2) @@ -47,7 +52,7 @@ def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where exact continuous_of_discreteTopology /-- The continuous map taking a lorentz matrix to its determinant. -/ -def detContinuous : C(𝓛, ℤ₂) := +def detContinuous : C(𝓛 d, ℤ₂) := ContinuousMap.comp coeForℤ₂ { toFun := fun Λ => ⟨Λ.1.det, Or.symm (LorentzGroup.det_eq_one_or_neg_one _)⟩, continuous_toFun := by @@ -56,7 +61,7 @@ def detContinuous : C(𝓛, ℤ₂) := Continuous.comp' (continuous_iff_le_induced.mpr fun U a => a) continuous_id' } -lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup) : +lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) : detContinuous Λ = detContinuous Λ' ↔ Λ.1.det = Λ'.1.det := by apply Iff.intro intro h @@ -75,7 +80,7 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup) : /-- The representation taking a lorentz matrix to its determinant. -/ @[simps!] -def detRep : 𝓛 →* ℤ₂ where +def detRep : 𝓛 d →* ℤ₂ where toFun Λ := detContinuous Λ map_one' := by simp [detContinuous, lorentzGroupIsGroup] @@ -88,9 +93,9 @@ def detRep : 𝓛 →* ℤ₂ where <;> simp [h1, h2, detContinuous] rfl -lemma detRep_continuous : Continuous detRep := detContinuous.2 +lemma detRep_continuous : Continuous (@detRep d) := detContinuous.2 -lemma det_on_connected_component {Λ Λ' : LorentzGroup} (h : Λ' ∈ connectedComponent Λ) : +lemma det_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) : Λ.1.det = Λ'.1.det := by obtain ⟨s, hs, hΛ'⟩ := h let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s detContinuous @@ -99,36 +104,35 @@ lemma det_on_connected_component {Λ Λ' : LorentzGroup} (h : Λ' ∈ connected (@IsPreconnected.subsingleton ℤ₂ _ _ _ (isPreconnected_range f.2)) (Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩) -lemma detRep_on_connected_component {Λ Λ' : LorentzGroup} (h : Λ' ∈ connectedComponent Λ) : +lemma detRep_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) : detRep Λ = detRep Λ' := by simp [detRep_apply, detRep_apply, detContinuous] rw [det_on_connected_component h] -lemma det_of_joined {Λ Λ' : LorentzGroup} (h : Joined Λ Λ') : Λ.1.det = Λ'.1.det := +lemma det_of_joined {Λ Λ' : LorentzGroup d} (h : Joined Λ Λ') : Λ.1.det = Λ'.1.det := det_on_connected_component $ pathComponent_subset_component _ h /-- A Lorentz Matrix is proper if its determinant is 1. -/ @[simp] -def IsProper (Λ : LorentzGroup) : Prop := Λ.1.det = 1 +def IsProper (Λ : LorentzGroup d) : Prop := Λ.1.det = 1 -instance : DecidablePred IsProper := by +instance : DecidablePred (@IsProper d) := by intro Λ apply Real.decidableEq -lemma IsProper_iff (Λ : LorentzGroup) : IsProper Λ ↔ detRep Λ = 1 := by +lemma IsProper_iff (Λ : LorentzGroup d) : IsProper Λ ↔ detRep Λ = 1 := by rw [show 1 = detRep 1 from Eq.symm (MonoidHom.map_one detRep)] rw [detRep_apply, detRep_apply, detContinuous_eq_iff_det_eq] simp only [IsProper, lorentzGroupIsGroup_one_coe, det_one] -lemma id_IsProper : IsProper 1 := by +lemma id_IsProper : (@IsProper d) 1 := by simp [IsProper] -lemma isProper_on_connected_component {Λ Λ' : LorentzGroup} (h : Λ' ∈ connectedComponent Λ) : +lemma isProper_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) : IsProper Λ ↔ IsProper Λ' := by simp [detRep_apply, detRep_apply, detContinuous] rw [det_on_connected_component h] end LorentzGroup -end SpaceTime end diff --git a/HepLean/SpaceTime/LorentzTensors/Basic.lean b/HepLean/SpaceTime/LorentzTensors/Basic.lean new file mode 100644 index 0000000..dac4a95 --- /dev/null +++ b/HepLean/SpaceTime/LorentzTensors/Basic.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +/-! + +# Lorentz Tensors + +This file is currently a stub. + +The aim is to define Lorentz tensors, and devlop a systematic way to manipulate them. + +To manipulate them we will use the theory of modular operads +(see e.g. [Raynor][raynor2021graphical]). + +-/ diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean new file mode 100644 index 0000000..9b58852 --- /dev/null +++ b/HepLean/SpaceTime/LorentzVector/Basic.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import Mathlib.Data.Complex.Exponential +import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners +import Mathlib.Analysis.InnerProductSpace.PiL2 +import Mathlib.LinearAlgebra.Matrix.DotProduct +import LeanCopilot +/-! + +# Lorentz vectors + +(aka 4-vectors) + +In this file we define a Lorentz vector (in 4d, this is more often called a 4-vector). + +One of the most important example of a Lorentz vector is SpaceTime. +-/ + +/- The number of space dimensions . -/ +variable (d : ℕ) + +/-- The type of Lorentz Vectors in `d`-space dimensions. -/ +def LorentzVector : Type := (Fin 1 ⊕ Fin d) → ℝ + +/-- An instance of a additive commutative monoid on `LorentzVector`. -/ +instance : AddCommMonoid (LorentzVector d) := Pi.addCommMonoid + +/-- An instance of a module on `LorentzVector`. -/ +noncomputable instance : Module ℝ (LorentzVector d) := Pi.module _ _ _ + +instance : AddCommGroup (LorentzVector d) := Pi.addCommGroup + +namespace LorentzVector + +variable {d : ℕ} + +variable (v : LorentzVector d) + +/-- The space components. -/ +@[simp] +def space : EuclideanSpace ℝ (Fin d) := v ∘ Sum.inr + +/-- The time component. -/ +@[simp] +def time : ℝ := v (Sum.inl 0) + +/-! + +# The standard basis + +-/ + +/-- The standard basis of `LorentzVector`. -/ +@[simps!] +noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin (d)) ℝ (LorentzVector d) := Pi.basisFun ℝ _ + +/-- The standard unit time vector. -/ +@[simp] +noncomputable def timeVec : (LorentzVector d) := stdBasis (Sum.inl 0) + +@[simp] +lemma timeVec_space : (@timeVec d).space = 0 := by + funext i + simp [space, stdBasis] + erw [Pi.basisFun_apply] + simp_all only [Fin.isValue, LinearMap.stdBasis_apply', ↓reduceIte] + +@[simp] +lemma timeVec_time: (@timeVec d).time = 1 := by + simp [space, stdBasis] + erw [Pi.basisFun_apply] + simp_all only [Fin.isValue, LinearMap.stdBasis_apply', ↓reduceIte] + +/-! + +# Reflection of space + +-/ + +/-- The reflection of space as a linear map. -/ +@[simps!] +def spaceReflectionLin : LorentzVector d →ₗ[ℝ] LorentzVector d where + toFun x := Sum.elim (x ∘ Sum.inl) (- x ∘ Sum.inr) + map_add' x y := by + funext i + rcases i with i | i + · simp only [Sum.elim_inl] + apply Eq.refl + · simp only [Sum.elim_inr, Pi.neg_apply] + apply neg_add + map_smul' c x := by + funext i + rcases i with i | i + · simp only [Sum.elim_inl, Pi.smul_apply] + apply smul_eq_mul + · simp [ HSMul.hSMul, SMul.smul] + + +/-- The reflection of space. -/ +@[simp] +def spaceReflection : LorentzVector d := spaceReflectionLin v + +@[simp] +lemma spaceReflection_space : v.spaceReflection.space = - v.space := by + rfl + +@[simp] +lemma spaceReflection_time : v.spaceReflection.time = v.time := by + rfl + + + +end LorentzVector diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean new file mode 100644 index 0000000..588db82 --- /dev/null +++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean @@ -0,0 +1,172 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.LorentzVector.Basic +import HepLean.SpaceTime.MinkowskiMetric +/-! + +# Lorentz vectors with norm one + +-/ + +open minkowskiMetric + +@[simp] +def NormOneLorentzVector (d : ℕ) : Set (LorentzVector d) := + fun x => ⟪x, x⟫ₘ = 1 + +namespace NormOneLorentzVector + +variable {d : ℕ} + +variable (v w : NormOneLorentzVector d) + +lemma mem_iff {x : LorentzVector d} : x ∈ NormOneLorentzVector d ↔ ⟪x, x⟫ₘ = 1 := by + rfl + +/-- The negative of a `NormOneLorentzVector` as a `NormOneLorentzVector`. -/ +def neg : NormOneLorentzVector d := ⟨- v, by + rw [mem_iff] + simp only [map_neg, LinearMap.neg_apply, neg_neg] + exact v.2⟩ + +lemma time_sq : v.1.time ^ 2 = 1 + ‖v.1.space‖ ^ 2 := by + rw [time_sq_eq_metric_add_space, v.2] + +lemma abs_time_ge_one : 1 ≤ |v.1.time| := by + have h1 := leq_time_sq v.1 + rw [v.2] at h1 + exact (one_le_sq_iff_one_le_abs _).mp h1 + +lemma norm_space_le_abs_time : ‖v.1.space‖ < |v.1.time| := by + rw [(abs_norm _).symm, ← @sq_lt_sq, time_sq] + exact lt_one_add (‖(v.1).space‖ ^ 2) + +lemma norm_space_leq_abs_time : ‖v.1.space‖ ≤ |v.1.time| := + le_of_lt (norm_space_le_abs_time v) + +lemma time_le_minus_one_or_ge_one : v.1.time ≤ -1 ∨ 1 ≤ v.1.time := + le_abs'.mp (abs_time_ge_one v) + +lemma time_nonpos_iff : v.1.time ≤ 0 ↔ v.1.time ≤ - 1 := by + apply Iff.intro + · intro h + cases' time_le_minus_one_or_ge_one v with h1 h1 + exact h1 + linarith + · intro h + linarith + + +lemma time_nonneg_iff : 0 ≤ v.1.time ↔ 1 ≤ v.1.time := by + apply Iff.intro + · intro h + cases' time_le_minus_one_or_ge_one v with h1 h1 + linarith + exact h1 + · intro h + linarith + +lemma time_pos_iff : 0 < v.1.time ↔ 1 ≤ v.1.time := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · exact (time_nonneg_iff v).mp (le_of_lt h) + · linarith + +lemma time_abs_sub_space_norm : + 0 ≤ |v.1.time| * |w.1.time| - ‖v.1.space‖ * ‖w.1.space‖ := by + apply sub_nonneg.mpr + apply mul_le_mul (norm_space_leq_abs_time v) (norm_space_leq_abs_time w) ?_ ?_ + exact norm_nonneg w.1.space + exact abs_nonneg (v.1 _) + +/-! + +# Future pointing norm one Lorentz vectors + +-/ + +/-- The future pointing Lorentz vectors with Norm one. -/ +def FuturePointing (d : ℕ) : Set (NormOneLorentzVector d) := + fun x => 0 < x.1.time + +namespace FuturePointing + +variable (f f' : FuturePointing d) + +lemma mem_iff : v ∈ FuturePointing d ↔ 0 < v.1.time := by + rfl + +lemma mem_iff_time_nonneg : v ∈ FuturePointing d ↔ 0 ≤ v.1.time := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + exact le_of_lt ((mem_iff v).mp h) + have h1 := (mem_iff v).mp + simp at h1 + rw [@time_nonneg_iff] at h + rw [mem_iff] + linarith + +lemma not_mem_iff : v ∉ FuturePointing d ↔ v.1.time ≤ 0 := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + exact le_of_not_lt ((mem_iff v).mp.mt h) + have h1 := (mem_iff v).mp.mt + simp at h1 + exact h1 h + +lemma not_mem_iff_neg : v ∉ FuturePointing d ↔ neg v ∈ FuturePointing d := by + rw [not_mem_iff, mem_iff_time_nonneg] + simp only [Fin.isValue, neg] + change _ ↔ 0 ≤ - v.1 _ + exact Iff.symm neg_nonneg + +lemma time_nonneg : 0 ≤ f.1.1.time := le_of_lt f.2 + +lemma abs_time : |f.1.1.time| = f.1.1.time := abs_of_nonneg (time_nonneg f) + +/-! + +# The value sign of ⟪v, w.1.spaceReflection⟫ₘ different v and w + +-/ + +section +variable {v w : NormOneLorentzVector d} + +lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) : + 0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by + apply le_trans (time_abs_sub_space_norm v w) + rw [abs_time ⟨v, h⟩, abs_time ⟨w, hw⟩ , sub_eq_add_neg, right_spaceReflection] + apply (add_le_add_iff_left _).mpr + rw [neg_le] + apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (w.1).space⟫_ℝ|) ?_ + exact abs_real_inner_le_norm (v.1).space (w.1).space + + +lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) : + 0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by + have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) ((not_mem_iff_neg w).mp hw) + apply le_of_le_of_eq h1 ?_ + simp [neg] + + +lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) : + ⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by + rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg] + have h1 := metric_reflect_mem_mem h ((not_mem_iff_neg w).mp hw) + apply le_of_le_of_eq h1 ?_ + simp [neg] + +lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw : w ∈ FuturePointing d) : + ⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by + rw [show (0 : ℝ) = - 0 by simp, le_neg] + have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) hw + apply le_of_le_of_eq h1 ?_ + simp [neg] + +end + +end FuturePointing + + +end NormOneLorentzVector diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean index 3a7ca46..3c54274 100644 --- a/HepLean/SpaceTime/Metric.lean +++ b/HepLean/SpaceTime/Metric.lean @@ -11,6 +11,12 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic This file introduces the metric on spacetime in the (+, -, -, -) signature. +## TODO + +This file needs refactoring. +- The metric should be defined as a bilinear map on `LorentzVector d`. +- From this definition, we should derive the metric as a matrix. + -/ noncomputable section diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean new file mode 100644 index 0000000..bfc842d --- /dev/null +++ b/HepLean/SpaceTime/MinkowskiMetric.lean @@ -0,0 +1,307 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.LorentzVector.Basic +import Mathlib.Algebra.Lie.Classical +import Mathlib.LinearAlgebra.QuadraticForm.Basic +/-! + +# The Minkowski Metric + +This file introduces the Minkowski metric on spacetime in the mainly-minus signature. + +We define the minkowski metric as a bilinear map on the vector space +of Lorentz vectors in d dimensions. + +-/ + + +open Matrix + +/-! + +# The definition of the Minkowski Matrix + +-/ +/-- The `d.succ`-dimensional real of the form `diag(1, -1, -1, -1, ...)`. -/ +def minkowskiMatrix {d : ℕ} : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := + LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin d) ℝ + +namespace minkowskiMatrix + +variable {d : ℕ} + +scoped[minkowskiMatrix] notation "η" => minkowskiMatrix + +@[simp] +lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by + simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] + ext1 i j + rcases i with i | i <;> rcases j with j | j + · simp only [diagonal, of_apply, Sum.inl.injEq, Sum.elim_inl, mul_one] + split + · simp_all only [one_apply_eq] + · simp_all only [ne_eq, Sum.inl.injEq, not_false_eq_true, one_apply_ne] + · simp only [ne_eq, not_false_eq_true, diagonal_apply_ne, one_apply_ne] + · simp only [ne_eq, not_false_eq_true, diagonal_apply_ne, one_apply_ne] + · simp only [diagonal, of_apply, Sum.inr.injEq, Sum.elim_inr, mul_neg, mul_one, neg_neg] + split + · simp_all only [one_apply_eq] + · simp_all only [ne_eq, Sum.inr.injEq, not_false_eq_true, one_apply_ne] + +@[simp] +lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by + simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose] + + +@[simp] +lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by + simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] + + + +end minkowskiMatrix + + +/-! + +# The definition of the Minkowski Metric + +-/ + +/-- Given a Lorentz vector `v` we define the the linear map `w ↦ v * η * w -/ +@[simps!] +def minkowskiLinearForm {d : ℕ} (v : LorentzVector d) : LorentzVector d →ₗ[ℝ] ℝ where + toFun w := v ⬝ᵥ (minkowskiMatrix *ᵥ w) + map_add' y z := by + noncomm_ring + rw [mulVec_add, dotProduct_add] + map_smul' c y := by + simp only [RingHom.id_apply, smul_eq_mul] + rw [mulVec_smul, dotProduct_smul] + rfl + +/-- The Minkowski metric as a bilinear map. -/ +def minkowskiMetric {d : ℕ} : LorentzVector d →ₗ[ℝ] LorentzVector d →ₗ[ℝ] ℝ where + toFun v := minkowskiLinearForm v + map_add' y z := by + ext1 x + simp only [minkowskiLinearForm_apply, LinearMap.add_apply] + apply add_dotProduct + map_smul' c y := by + ext1 x + simp only [minkowskiLinearForm_apply, RingHom.id_apply, LinearMap.smul_apply, smul_eq_mul] + rw [smul_dotProduct] + rfl + +namespace minkowskiMetric + +open minkowskiMatrix + +open LorentzVector + +variable {d : ℕ} +variable (v w : LorentzVector d) + +scoped[minkowskiMetric] notation "⟪" v "," w "⟫ₘ" => minkowskiMetric v w +/-! + +# Equalitites involving the Minkowski metric + +-/ + +/-- The Minkowski metric expressed as a sum. -/ +lemma as_sum : + ⟪v, w⟫ₘ = v.time * w.time - ∑ i, v.space i * w.space i := by + simp only [minkowskiMetric, LinearMap.coe_mk, AddHom.coe_mk, minkowskiLinearForm_apply, + dotProduct, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal, Fintype.sum_sum_type, + Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Sum.elim_inl, one_mul, + Finset.sum_singleton, Sum.elim_inr, neg_mul, mul_neg, Finset.sum_neg_distrib, time, space, + Function.comp_apply, minkowskiMatrix] + ring + + +/-- The Minkowski metric expressed as a sum for a single vector. -/ +lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by + rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum] + noncomm_ring + +lemma eq_time_minus_inner_prod : ⟪v, w⟫ₘ = v.time * w.time - ⟪v.space, w.space⟫_ℝ := by + rw [as_sum, @PiLp.inner_apply] + noncomm_ring + +lemma self_eq_time_minus_norm : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by + rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum] + noncomm_ring + +/-- The Minkowski metric is symmetric. -/ +lemma symm : ⟪v, w⟫ₘ = ⟪w, v⟫ₘ := by + simp only [as_sum] + ac_rfl + +lemma time_sq_eq_metric_add_space : v.time ^ 2 = ⟪v, v⟫ₘ + ‖v.space‖ ^ 2 := by + rw [self_eq_time_minus_norm] + exact Eq.symm (sub_add_cancel (v.time ^ 2) (‖v.space‖ ^ 2)) + +/-! + +# Minkowski metric and space reflections + +-/ + +lemma right_spaceReflection : ⟪v, w.spaceReflection⟫ₘ = v.time * w.time + ⟪v.space, w.space⟫_ℝ := by + rw [eq_time_minus_inner_prod, spaceReflection_space, spaceReflection_time] + simp only [time, Fin.isValue, space, inner_neg_right, PiLp.inner_apply, Function.comp_apply, + RCLike.inner_apply, conj_trivial, sub_neg_eq_add] + + +lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v = 0 := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · rw [right_spaceReflection] at h + have h2 : 0 ≤ ⟪v.space, v.space⟫_ℝ := real_inner_self_nonneg + have h3 : v.time * v.time = 0 := by linarith [mul_self_nonneg v.time] + have h4 : ⟪v.space, v.space⟫_ℝ = 0 := by linarith + simp only [time, Fin.isValue, mul_eq_zero, or_self] at h3 + rw [@inner_self_eq_zero] at h4 + funext i + rcases i with i | i + · fin_cases i + exact h3 + · simpa using congrFun h4 i + · rw [h] + simp only [map_zero, LinearMap.zero_apply] +/-! + +# Non degeneracy of the Minkowski metric + +-/ + +/-- The metric tensor is non-degenerate. -/ +lemma nondegenerate : (∀ w, ⟪w, v⟫ₘ = 0) ↔ v = 0 := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · exact (self_spaceReflection_eq_zero_iff _ ).mp ((symm _ _).trans $ h v.spaceReflection) + · simp [h] + + +/-! + +# Inequalitites involving the Minkowski metric + +-/ + +lemma leq_time_sq : ⟪v, v⟫ₘ ≤ v.time ^ 2 := by + rw [time_sq_eq_metric_add_space] + exact (le_add_iff_nonneg_right _).mpr $ sq_nonneg ‖v.space‖ + +lemma ge_abs_inner_product : v.time * w.time - ‖⟪v.space, w.space⟫_ℝ‖ ≤ ⟪v, w⟫ₘ := by + rw [eq_time_minus_inner_prod, sub_le_sub_iff_left] + exact Real.le_norm_self ⟪v.space, w.space⟫_ℝ + +lemma ge_sub_norm : v.time * w.time - ‖v.space‖ * ‖w.space‖ ≤ ⟪v, w⟫ₘ := by + apply le_trans ?_ (ge_abs_inner_product v w) + rw [sub_le_sub_iff_left] + exact norm_inner_le_norm v.space w.space + +/-! + +# The Minkowski metric and the standard basis + +-/ + +lemma on_timeVec : ⟪timeVec, @timeVec d⟫ₘ = 1 := by + rw [self_eq_time_minus_norm, timeVec_time, timeVec_space] + simp [LorentzVector.stdBasis, minkowskiMetric] + +/-! + +# The Minkowski metric and matrices + +-/ +section matrices + +variable (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) + +/-- The dual of a matrix with respect to the Minkowski metric. -/ +def dual : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := η * Λᵀ * η + +@[simp] +lemma dual_id : @dual d 1 = 1 := by + simpa only [dual, transpose_one, mul_one] using minkowskiMatrix.sq + +@[simp] +lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by + simp only [dual, transpose_mul] + trans η * Λ'ᵀ * (η * η) * Λᵀ * η + noncomm_ring [minkowskiMatrix.sq] + noncomm_ring + +@[simp] +lemma dual_dual : dual (dual Λ) = Λ := by + simp only [dual, transpose_mul, transpose_transpose, eq_transpose] + trans (η * η) * Λ * (η * η) + noncomm_ring + noncomm_ring [minkowskiMatrix.sq] + +@[simp] +lemma dual_eta : @dual d η = η := by + simp only [dual, eq_transpose] + noncomm_ring [minkowskiMatrix.sq] + +@[simp] +lemma dual_transpose : dual Λᵀ = (dual Λ)ᵀ := by + simp only [dual, transpose_transpose, transpose_mul, eq_transpose] + noncomm_ring + +@[simp] +lemma det_dual : (dual Λ).det = Λ.det := by + simp only [dual, det_mul, minkowskiMatrix.det_eq_neg_one_pow_d, det_transpose] + group + norm_cast + simp + +@[simp] +lemma dual_mulVec_right : ⟪x, (dual Λ) *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ := by + simp only [minkowskiMetric, LinearMap.coe_mk, AddHom.coe_mk, dual, minkowskiLinearForm_apply, + mulVec_mulVec, ← mul_assoc, minkowskiMatrix.sq, one_mul, (vecMul_transpose Λ x).symm, ← + dotProduct_mulVec] + +@[simp] +lemma dual_mulVec_left : ⟪(dual Λ) *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ := by + rw [symm, dual_mulVec_right, symm] + +lemma matrix_apply_eq_iff_sub : ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ ↔ ⟪v, (Λ - Λ') *ᵥ w⟫ₘ = 0 := by + rw [← sub_eq_zero, ← LinearMap.map_sub, sub_mulVec] + +lemma matrix_eq_iff_eq_forall' : (∀ v, Λ *ᵥ v= Λ' *ᵥ v) ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · intro w v + rw [h w] + · simp only [matrix_apply_eq_iff_sub] at h + intro v + refine sub_eq_zero.1 ?_ + have h1 := h v + rw [nondegenerate] at h1 + simp [sub_mulVec] at h1 + exact h1 + +lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by + rw [← matrix_eq_iff_eq_forall'] + refine Iff.intro (fun h => ?_) (fun h => ?_) + · rw [h] + simp + · rw [← (LinearMap.toMatrix stdBasis stdBasis).toEquiv.symm.apply_eq_iff_eq] + ext1 x + simp only [LinearEquiv.coe_toEquiv_symm, LinearMap.toMatrix_symm, EquivLike.coe_coe, + toLin_apply, h, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.sum_singleton] + +lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by + rw [matrix_eq_iff_eq_forall] + simp + + +end matrices + +end minkowskiMetric diff --git a/docs/references.bib b/docs/references.bib index c99cd7f..6022c68 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -1,3 +1,4 @@ + # To normalize: # bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i docs/references.bib -o docs/references.bib @@ -5,7 +6,6 @@ # To link to an entry in `references.bib`, use the following formats: # [Author, *Title* (optional location)][bibkey] - @Article{ Allanach:2021yjy, author = "Allanach, B. C. and Madigan, Maeve and Tooby-Smith, Joseph", @@ -33,3 +33,14 @@ pages = "009", year = "2020" } + +@Article{ raynor2021graphical, + title = {Graphical combinatorics and a distributive law for modular + operads}, + author = {Raynor, Sophie}, + journal = {Advances in Mathematics}, + volume = {392}, + pages = {108011}, + year = {2021}, + publisher = {Elsevier} +} From c64d926e7c2009e6d90d58343fc9d9ad4eb069cf Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 2 Jul 2024 10:13:52 -0400 Subject: [PATCH 2/6] refactor: Lorentz Group etc. --- HepLean.lean | 8 +- HepLean/SpaceTime/AsSelfAdjointMatrix.lean | 92 ------ HepLean/SpaceTime/FourVelocity.lean | 248 ---------------- HepLean/SpaceTime/LorentzAlgebra/Basic.lean | 103 +++---- HepLean/SpaceTime/LorentzAlgebra/Basis.lean | 143 +-------- HepLean/SpaceTime/LorentzGroup/Basic.lean | 2 +- HepLean/SpaceTime/LorentzGroup/Boosts.lean | 82 +++--- HepLean/SpaceTime/LorentzGroup/Rotations.lean | 35 ++- .../LorentzVector/AsSelfAdjointMatrix.lean | 145 ++++++++++ HepLean/SpaceTime/LorentzVector/Basic.lean | 26 +- HepLean/SpaceTime/LorentzVector/NormOne.lean | 131 ++++++++- HepLean/SpaceTime/Metric.lean | 273 ------------------ HepLean/SpaceTime/MinkowskiMetric.lean | 67 ++++- HepLean/SpaceTime/SL2C/Basic.lean | 23 +- scripts/lint-all.sh | 1 - 15 files changed, 488 insertions(+), 891 deletions(-) delete mode 100644 HepLean/SpaceTime/AsSelfAdjointMatrix.lean delete mode 100644 HepLean/SpaceTime/FourVelocity.lean create mode 100644 HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean delete mode 100644 HepLean/SpaceTime/Metric.lean diff --git a/HepLean.lean b/HepLean.lean index 7940592..96bf060 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -60,10 +60,8 @@ import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters import HepLean.Mathematics.LinearMaps import HepLean.Mathematics.SO3.Basic -import HepLean.SpaceTime.AsSelfAdjointMatrix import HepLean.SpaceTime.Basic import HepLean.SpaceTime.CliffordAlgebra -import HepLean.SpaceTime.FourVelocity import HepLean.SpaceTime.LorentzAlgebra.Basic import HepLean.SpaceTime.LorentzAlgebra.Basis import HepLean.SpaceTime.LorentzGroup.Basic @@ -71,7 +69,11 @@ import HepLean.SpaceTime.LorentzGroup.Boosts import HepLean.SpaceTime.LorentzGroup.Orthochronous import HepLean.SpaceTime.LorentzGroup.Proper import HepLean.SpaceTime.LorentzGroup.Rotations -import HepLean.SpaceTime.Metric +import HepLean.SpaceTime.LorentzTensors.Basic +import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix +import HepLean.SpaceTime.LorentzVector.Basic +import HepLean.SpaceTime.LorentzVector.NormOne +import HepLean.SpaceTime.MinkowskiMetric import HepLean.SpaceTime.SL2C.Basic import HepLean.StandardModel.Basic import HepLean.StandardModel.HiggsBoson.Basic diff --git a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean deleted file mode 100644 index 5c65d64..0000000 --- a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean +++ /dev/null @@ -1,92 +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.LinearAlgebra.Matrix.SpecialLinearGroup -/-! -# Spacetime as a self-adjoint matrix - -There is a linear equivalence between the vector space of space-time points -and the vector space of 2×2-complex self-adjoint matrices. - -In this file we define this linear equivalence in `toSelfAdjointMatrix`. - --/ -namespace SpaceTime - -open Matrix -open MatrixGroups -open Complex - -/-- A 2×2-complex matrix formed from a space-time point. -/ -@[simp] -def toMatrix (x : SpaceTime) : Matrix (Fin 2) (Fin 2) ℂ := - !![x 0 + x 3, x 1 - x 2 * I; x 1 + x 2 * I, x 0 - x 3] - -/-- The matrix `x.toMatrix` for `x ∈ spaceTime` is self adjoint. -/ -lemma toMatrix_isSelfAdjoint (x : SpaceTime) : IsSelfAdjoint x.toMatrix := by - rw [isSelfAdjoint_iff, star_eq_conjTranspose, ← Matrix.ext_iff] - intro i j - fin_cases i <;> fin_cases j <;> - simp [toMatrix, conj_ofReal] - rfl - -/-- A self-adjoint matrix formed from a space-time point. -/ -@[simps!] -def toSelfAdjointMatrix' (x : SpaceTime) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) := - ⟨x.toMatrix, toMatrix_isSelfAdjoint x⟩ - -/-- A self-adjoint matrix formed from a space-time point. -/ -@[simp] -noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : SpaceTime := - ![1/2 * (x.1 0 0 + x.1 1 1).re, (x.1 1 0).re, (x.1 1 0).im , (x.1 0 0 - x.1 1 1).re/2] - -/-- The linear equivalence between the vector-space `spaceTime` and self-adjoint - 2×2-complex matrices. -/ -noncomputable def toSelfAdjointMatrix : SpaceTime ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where - toFun := toSelfAdjointMatrix' - invFun := fromSelfAdjointMatrix' - left_inv x := by - simp only [fromSelfAdjointMatrix', one_div, toSelfAdjointMatrix'_coe, of_apply, cons_val', - cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_cons, head_fin_const, - add_add_sub_cancel, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, - sub_self, add_zero, add_im, mul_im, zero_add, add_sub_sub_cancel, half_add_self] - field_simp [SpaceTime] - ext1 x - fin_cases x <;> rfl - right_inv x := by - simp only [toSelfAdjointMatrix', toMatrix, fromSelfAdjointMatrix', one_div, Fin.isValue, add_re, - sub_re, cons_val_zero, ofReal_mul, ofReal_inv, ofReal_ofNat, ofReal_add, cons_val_three, - Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, head_cons, ofReal_div, ofReal_sub, - cons_val_one, cons_val_two, re_add_im] - ext i j - fin_cases i <;> fin_cases j <;> - field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal] - exact conj_eq_iff_re.mp (congrArg (fun M => M 0 0) $ selfAdjoint.mem_iff.mp x.2 ) - have h01 := congrArg (fun M => M 0 1) $ selfAdjoint.mem_iff.mp x.2 - simp only [Fin.isValue, star_apply, RCLike.star_def] at h01 - rw [← h01, RCLike.conj_eq_re_sub_im] - rfl - exact conj_eq_iff_re.mp (congrArg (fun M => M 1 1) $ selfAdjoint.mem_iff.mp x.2 ) - map_add' x y := by - ext i j : 2 - simp only [toSelfAdjointMatrix'_coe, add_apply, ofReal_add, of_apply, cons_val', empty_val', - cons_val_fin_one, AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, Matrix.add_apply] - fin_cases i <;> fin_cases j <;> simp <;> ring - map_smul' r x := by - ext i j : 2 - simp only [toSelfAdjointMatrix', toMatrix, Fin.isValue, smul_apply, ofReal_mul, - RingHom.id_apply] - fin_cases i <;> fin_cases j <;> - field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal, smul_apply] - <;> ring - -lemma det_eq_ηLin (x : SpaceTime) : det (toSelfAdjointMatrix x).1 = ηLin x x := by - simp [toSelfAdjointMatrix, ηLin_expand] - ring_nf - simp only [Fin.isValue, I_sq, mul_neg, mul_one] - ring - -end SpaceTime diff --git a/HepLean/SpaceTime/FourVelocity.lean b/HepLean/SpaceTime/FourVelocity.lean deleted file mode 100644 index e9fb200..0000000 --- a/HepLean/SpaceTime/FourVelocity.lean +++ /dev/null @@ -1,248 +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 -/-! -# 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 - -/-- A `spaceTime` vector for which `ηLin x x = 1`. -/ -@[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 - -/-- 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] - 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] - exact lt_one_add (‖(v.1).space‖ ^ 2) - -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 - -/-- A `PreFourVelocity` is a `FourVelocity` if its time component is non-negative. -/ -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 - exact fun a => le_of_lt a - 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 - exact Iff.symm neg_nonneg - -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 from zero_eq_neg.mpr rfl, 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 - -/-- The set of `PreFourVelocity`'s which are four velocities. -/ -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] - -/-- 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], - 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 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 only [Set.Icc.coe_one, one_pow, space, Fin.isValue, one_mul] - refine SetCoe.ext ?_ - refine SetCoe.ext ?_ - funext i - fin_cases i - simp only [Fin.isValue, Fin.zero_eta, Matrix.cons_val_zero] - exact (time_comp _).symm - all_goals rfl - -lemma isPathConnected_FourVelocity : IsPathConnected (@Set.univ FourVelocity) := by - use zero - apply And.intro trivial ?_ - intro y a - use pathFromZero y - exact fun _ => a - -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/LorentzAlgebra/Basic.lean b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean index 74a3c9b..2375989 100644 --- a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean +++ b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.Basic -import HepLean.SpaceTime.Metric +import HepLean.SpaceTime.MinkowskiMetric import Mathlib.Algebra.Lie.Classical /-! # The Lorentz Algebra @@ -12,7 +12,7 @@ import Mathlib.Algebra.Lie.Classical We define - Define `lorentzAlgebra` via `LieAlgebra.Orthogonal.so'` as a subalgebra of - `Matrix (Fin 4) (Fin 4) ℝ`. + `Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ`. - In `mem_iff` prove that a matrix is in the Lorentz algebra if and only if it satisfies the condition `Aᵀ * η = - η * A`. @@ -23,80 +23,71 @@ namespace SpaceTime open Matrix open TensorProduct -/-- The Lorentz algebra as a subalgebra of `Matrix (Fin 4) (Fin 4) ℝ`. -/ -def lorentzAlgebra : LieSubalgebra ℝ (Matrix (Fin 4) (Fin 4) ℝ) := - LieSubalgebra.map (Matrix.reindexLieEquiv (@finSumFinEquiv 1 3)).toLieHom +/-- The Lorentz algebra as a subalgebra of `Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ`. -/ +def lorentzAlgebra : LieSubalgebra ℝ (Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) := (LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ) namespace lorentzAlgebra +open minkowskiMatrix lemma transpose_eta (A : lorentzAlgebra) : A.1ᵀ * η = - η * A.1 := by - obtain ⟨B, hB1, hB2⟩ := A.2 - apply (Equiv.apply_eq_iff_eq - (Matrix.reindexAlgEquiv ℝ (@finSumFinEquiv 1 3).symm).toEquiv).mp - simp only [Nat.reduceAdd, AlgEquiv.toEquiv_eq_coe, EquivLike.coe_coe, _root_.map_mul, - reindexAlgEquiv_apply, ← transpose_reindex, map_neg] - rw [(Equiv.apply_eq_iff_eq_symm_apply (reindex finSumFinEquiv.symm finSumFinEquiv.symm)).mpr - hB2.symm] - erw [η_reindex] - simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using hB1 + have h1 := A.2 + erw [mem_skewAdjointMatricesLieSubalgebra] at h1 + simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h1 -lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 4) (Fin 4) ℝ} + +lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} (h : Aᵀ * η = - η * A) : A ∈ lorentzAlgebra := by - simp only [lorentzAlgebra, Nat.reduceAdd, LieSubalgebra.mem_map] - use (Matrix.reindexLieEquiv (@finSumFinEquiv 1 3)).symm A - apply And.intro - · have h1 := (Equiv.apply_eq_iff_eq - (Matrix.reindexAlgEquiv ℝ (@finSumFinEquiv 1 3).symm).toEquiv).mpr h - erw [Matrix.reindexAlgEquiv_mul] at h1 - simp only [Nat.reduceAdd, reindexAlgEquiv_apply, Equiv.symm_symm, AlgEquiv.toEquiv_eq_coe, - EquivLike.coe_coe, map_neg, _root_.map_mul] at h1 - erw [η_reindex] at h1 - simpa [Nat.reduceAdd, reindexLieEquiv_symm, reindexLieEquiv_apply, - LieAlgebra.Orthogonal.so', mem_skewAdjointMatricesLieSubalgebra, - mem_skewAdjointMatricesSubmodule, IsSkewAdjoint, IsAdjointPair, mul_neg] using h1 - · exact LieEquiv.apply_symm_apply (reindexLieEquiv finSumFinEquiv) _ + erw [mem_skewAdjointMatricesLieSubalgebra] + simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h - -lemma mem_iff {A : Matrix (Fin 4) (Fin 4) ℝ} : A ∈ lorentzAlgebra ↔ Aᵀ * η = - η * A := +lemma mem_iff {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} : + A ∈ lorentzAlgebra ↔ Aᵀ * η = - η * A := Iff.intro (fun h => transpose_eta ⟨A, h⟩) (fun h => mem_of_transpose_eta_eq_eta_mul_self h) -lemma mem_iff' (A : Matrix (Fin 4) (Fin 4) ℝ) : A ∈ lorentzAlgebra ↔ A = - η * Aᵀ * η := by - apply Iff.intro - intro h - simp_rw [mul_assoc, mem_iff.mp h, neg_mul, mul_neg, ← mul_assoc, η_sq, one_mul, neg_neg] - intro h +lemma mem_iff' (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) : + A ∈ lorentzAlgebra ↔ A = - η * Aᵀ * η := by rw [mem_iff] - nth_rewrite 2 [h] - simp [← mul_assoc, η_sq] + refine Iff.intro (fun h => ?_) (fun h => ?_) + · trans -η * (Aᵀ * η) + rw [h] + trans (η * η) * A + rw [minkowskiMatrix.sq] + all_goals noncomm_ring + · nth_rewrite 2 [h] + trans (η * η) * Aᵀ * η + rw [minkowskiMatrix.sq] + all_goals noncomm_ring -lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 4) : Λ.1 μ μ = 0 := by + +lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 := by have h := congrArg (fun M ↦ M μ μ) $ mem_iff.mp Λ.2 - simp at h - fin_cases μ <;> - rw [η_mul, mul_η, η_explicit] at h - <;> simpa using h + simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal, + transpose_apply, diagonal_neg, diagonal_mul, neg_mul] at h + rcases μ with μ | μ + simpa using h + simpa using h + + + +lemma time_comps (Λ : lorentzAlgebra) (i : Fin 3) : + Λ.1 (Sum.inr i) (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inr i) := by + simpa only [Fin.isValue, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal, + transpose_apply, Sum.elim_inr, mul_neg, mul_one, diagonal_neg, diagonal_mul, Sum.elim_inl, + neg_mul, one_mul, neg_inj] using congrArg (fun M ↦ M (Sum.inl 0) (Sum.inr i)) $ mem_iff.mp Λ.2 -lemma time_comps (Λ : lorentzAlgebra) (i : Fin 3) : Λ.1 i.succ 0 = Λ.1 0 i.succ := by - have h := congrArg (fun M ↦ M 0 i.succ) $ mem_iff.mp Λ.2 - simp at h - fin_cases i <;> - rw [η_mul, mul_η, η_explicit] at h <;> - simpa using h lemma space_comps (Λ : lorentzAlgebra) (i j : Fin 3) : - Λ.1 i.succ j.succ = - Λ.1 j.succ i.succ := by - have h := congrArg (fun M ↦ M i.succ j.succ) $ mem_iff.mp Λ.2 - simp at h - fin_cases i <;> fin_cases j <;> - rw [η_mul, mul_η, η_explicit] at h <;> - simpa using h.symm + Λ.1 (Sum.inr i) (Sum.inr j) = - Λ.1 (Sum.inr j) (Sum.inr i) := by + simpa only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_neg, diagonal_mul, + Sum.elim_inr, neg_neg, one_mul, mul_diagonal, transpose_apply, mul_neg, mul_one] using + (congrArg (fun M ↦ M (Sum.inr i) (Sum.inr j)) $ mem_iff.mp Λ.2).symm end lorentzAlgebra @[simps!] -instance spaceTimeAsLieRingModule : LieRingModule lorentzAlgebra SpaceTime where +instance lorentzVectorAsLieRingModule : LieRingModule lorentzAlgebra (LorentzVector 3) where bracket Λ x := Λ.1.mulVec x add_lie Λ1 Λ2 x := by simp [add_mulVec] @@ -107,7 +98,7 @@ instance spaceTimeAsLieRingModule : LieRingModule lorentzAlgebra SpaceTime where simp [mulVec_add, Bracket.bracket, sub_mulVec] @[simps!] -instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra SpaceTime where +instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra (LorentzVector 3) where smul_lie r Λ x := by simp [Bracket.bracket, smul_mulVec_assoc] lie_smul r Λ x := by diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean index 7b08f25..45f9f44 100644 --- a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean +++ b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean @@ -7,142 +7,11 @@ import HepLean.SpaceTime.LorentzAlgebra.Basic /-! # Basis of the Lorentz Algebra -We define the standard basis of the Lorentz group. +This file is currently a stub. + +Old commits contained code here, however this has not being ported forward. + +This file is waiting for Lorentz Tensors to be done formally, before +it can be completed. -/ - -namespace SpaceTime - -namespace lorentzAlgebra -open Matrix - -/-- The matrices which form the basis of the Lorentz algebra. -/ -@[simp] -def σMat (μ ν : Fin 4) : Matrix (Fin 4) (Fin 4) ℝ := fun ρ δ ↦ - η_[μ]_[δ] * η^[ρ]_[ν] - η^[ρ]_[μ] * η_[ν]_[δ] - -lemma σMat_in_lorentzAlgebra (μ ν : Fin 4) : σMat μ ν ∈ lorentzAlgebra := by - rw [mem_iff] - funext ρ δ - rw [Matrix.neg_mul, Matrix.neg_apply, η_mul, mul_η, transpose_apply] - apply Eq.trans ?_ (by ring : - ((η^[ρ]_[μ] * η_[ρ]_[ρ]) * η_[ν]_[δ] - η_[μ]_[δ] * (η^[ρ]_[ν] * η_[ρ]_[ρ])) = - -(η_[ρ]_[ρ] * (η_[μ]_[δ] * η^[ρ]_[ν] - η^[ρ]_[μ] * η_[ν]_[δ] ))) - apply Eq.trans (by ring : (η_[μ]_[ρ] * η^[δ]_[ν] - η^[δ]_[μ] * η_[ν]_[ρ]) * η_[δ]_[δ] - = (- (η^[δ]_[μ] * η_[δ]_[δ]) * η_[ν]_[ρ] + η_[μ]_[ρ] * (η^[δ]_[ν] * η_[δ]_[δ]))) - rw [η_mul_self, η_mul_self, η_mul_self, η_mul_self] - ring - -/-- Elements of the Lorentz algebra which form a basis thereof. -/ -@[simps!] -def σ (μ ν : Fin 4) : lorentzAlgebra := ⟨σMat μ ν, σMat_in_lorentzAlgebra μ ν⟩ - -lemma σ_anti_symm (μ ν : Fin 4) : σ μ ν = - σ ν μ := by - refine SetCoe.ext ?_ - funext ρ δ - simp only [σ_coe, σMat, NegMemClass.coe_neg, neg_apply, neg_sub] - ring - -lemma σMat_mul (α β γ δ a b: Fin 4) : - (σMat α β * σMat γ δ) a b = - η^[a]_[α] * (η_[δ]_[b] * η_[β]_[γ] - η_[γ]_[b] * η_[β]_[δ]) - - η^[a]_[β] * (η_[δ]_[b] * η_[α]_[γ]- η_[γ]_[b] * η_[α]_[δ]) := by - rw [Matrix.mul_apply] - simp only [σMat] - trans (η^[a]_[α] * η_[δ]_[b]) * ∑ x, η^[x]_[γ] * η_[β]_[x] - - (η^[a]_[α] * η_[γ]_[b]) * ∑ x, η^[x]_[δ] * η_[β]_[x] - - (η^[a]_[β] * η_[δ]_[b]) * ∑ x, η^[x]_[γ] * η_[α]_[x] - + (η^[a]_[β] * η_[γ]_[b]) * ∑ x, η^[x]_[δ] * η_[α]_[x] - repeat rw [Fin.sum_univ_four] - ring - rw [η_contract_self', η_contract_self', η_contract_self', η_contract_self'] - ring - -lemma σ_comm (α β γ δ : Fin 4) : - ⁅σ α β , σ γ δ⁆ = - η_[α]_[δ] • σ γ β + η_[α]_[γ] • σ β δ + η_[β]_[δ] • σ α γ + η_[β]_[γ] • σ δ α := by - refine SetCoe.ext ?_ - change σMat α β * σ γ δ - σ γ δ * σ α β = _ - funext a b - simp only [σ_coe, sub_apply, AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid, - Submodule.coe_smul_of_tower, Matrix.add_apply, Matrix.smul_apply, σMat, smul_eq_mul] - rw [σMat_mul, σMat_mul, η_symmetric α γ, η_symmetric α δ, η_symmetric β γ, η_symmetric β δ] - ring - -lemma eq_span_σ (Λ : lorentzAlgebra) : - Λ = Λ.1 0 1 • σ 0 1 + Λ.1 0 2 • σ 0 2 + Λ.1 0 3 • σ 0 3 + - Λ.1 1 2 • σ 1 2 + Λ.1 1 3 • σ 1 3 + Λ.1 2 3 • σ 2 3 := by - apply SetCoe.ext ?_ - funext a b - fin_cases a <;> fin_cases b <;> - simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, AddSubmonoid.coe_add, - Submodule.coe_smul_of_tower, σ_coe, - Matrix.add_apply, Matrix.smul_apply, σMat, ηUpDown, ne_eq, zero_ne_one, not_false_eq_true, - one_apply_ne, η_explicit, of_apply, cons_val_zero, - mul_zero, one_apply_eq, mul_one, sub_neg_eq_add, - zero_add, smul_eq_mul, Fin.reduceEq, cons_val_one, vecHead, vecTail, - Nat.reduceAdd, Function.comp_apply, Fin.succ_zero_eq_one, sub_self, add_zero, cons_val_two, - cons_val_three, Fin.succ_one_eq_two, mul_neg, neg_zero, sub_zero] - · exact diag_comp Λ 0 - · exact time_comps Λ 0 - · exact diag_comp Λ 1 - · exact time_comps Λ 1 - · exact space_comps Λ 1 0 - · exact diag_comp Λ 2 - · exact time_comps Λ 2 - · exact space_comps Λ 2 0 - · exact space_comps Λ 2 1 - · exact diag_comp Λ 3 - -/-- The coordinate map for the basis formed by the matrices `σ`. -/ -@[simps!] -noncomputable def σCoordinateMap : lorentzAlgebra ≃ₗ[ℝ] Fin 6 →₀ ℝ where - toFun Λ := Finsupp.equivFunOnFinite.invFun - fun i => match i with - | 0 => Λ.1 0 1 - | 1 => Λ.1 0 2 - | 2 => Λ.1 0 3 - | 3 => Λ.1 1 2 - | 4 => Λ.1 1 3 - | 5 => Λ.1 2 3 - map_add' S T := by - ext i - fin_cases i <;> rfl - map_smul' c S := by - ext i - fin_cases i <;> rfl - invFun c := c 0 • σ 0 1 + c 1 • σ 0 2 + c 2 • σ 0 3 + - c 3 • σ 1 2 + c 4 • σ 1 3 + c 5 • σ 2 3 - left_inv Λ := by - simp only [Fin.isValue, Equiv.invFun_as_coe, Finsupp.equivFunOnFinite_symm_apply_toFun] - exact (eq_span_σ Λ).symm - right_inv c := by - ext i - fin_cases i <;> simp only [Fin.isValue, Set.Finite.toFinset_setOf, ne_eq, Finsupp.coe_mk, - Fin.zero_eta, Fin.isValue, Fin.mk_one, Fin.reduceFinMk, AddSubmonoid.coe_add, - Submodule.coe_toAddSubmonoid, Submodule.coe_smul_of_tower, σ_coe, - Matrix.add_apply, Matrix.smul_apply, σMat, ηUpDown, ne_eq, zero_ne_one, not_false_eq_true, - one_apply_ne, η_explicit, of_apply, cons_val', cons_val_zero, empty_val', - cons_val_fin_one, vecCons_const, mul_zero, one_apply_eq, mul_one, sub_neg_eq_add, - zero_add, smul_eq_mul, Fin.reduceEq, cons_val_one, vecHead, vecTail, Nat.succ_eq_add_one, - Nat.reduceAdd, Function.comp_apply, Fin.succ_zero_eq_one, sub_self, add_zero, cons_val_two, - cons_val_three, Fin.succ_one_eq_two, mul_neg, neg_zero, sub_zero, Finsupp.equivFunOnFinite] - -/-- The basis formed by the matrices `σ`. -/ -@[simps! repr_apply_support_val repr_apply_toFun] -noncomputable def σBasis : Basis (Fin 6) ℝ lorentzAlgebra where - repr := σCoordinateMap - -instance : Module.Finite ℝ lorentzAlgebra := - Module.Finite.of_basis σBasis - -/-- The Lorentz algebra is 6-dimensional. -/ -theorem finrank_eq_six : FiniteDimensional.finrank ℝ lorentzAlgebra = 6 := by - have h := Module.mk_finrank_eq_card_basis σBasis - simp only [finrank_eq_rank, Cardinal.mk_fintype, Fintype.card_fin, Nat.cast_ofNat] at h - exact FiniteDimensional.finrank_eq_of_rank_eq h - - -end lorentzAlgebra - -end SpaceTime diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index 446a3b9..9975707 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.MinkowskiMetric -import HepLean.SpaceTime.AsSelfAdjointMatrix +import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix import HepLean.SpaceTime.LorentzVector.NormOne /-! # The Lorentz Group diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean index a11246a..38e46e6 100644 --- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean +++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean @@ -68,7 +68,7 @@ def genBoostAux₂ (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] Lorent /-- An generalised boost. This is a Lorentz transformation which takes the four velocity `u` to `v`. -/ -def genBoost (u v : FourVelocity) : SpaceTime →ₗ[ℝ] SpaceTime := +def genBoost (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] LorentzVector d := LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v namespace genBoost @@ -77,7 +77,7 @@ namespace genBoost This lemma states that for a given four-velocity `u`, the general boost transformation `genBoost u u` is equal to the identity linear map `LinearMap.id`. -/ -lemma self (u : FourVelocity) : genBoost u u = LinearMap.id := by +lemma self (u : FuturePointing d) : genBoost u u = LinearMap.id := by ext x simp [genBoost] rw [add_assoc] @@ -94,84 +94,88 @@ lemma self (u : FourVelocity) : genBoost u u = LinearMap.id := by rfl /-- A generalised boost as a matrix. -/ -def toMatrix (u v : FourVelocity) : Matrix (Fin 4) (Fin 4) ℝ := - LinearMap.toMatrix stdBasis stdBasis (genBoost u v) +def toMatrix (u v : FuturePointing d) : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := + LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (genBoost u v) -lemma toMatrix_mulVec (u v : FourVelocity) (x : SpaceTime) : +lemma toMatrix_mulVec (u v : FuturePointing d) (x : LorentzVector d) : (toMatrix u v).mulVec x = genBoost u v x := - LinearMap.toMatrix_mulVec_repr stdBasis stdBasis (genBoost u v) x + LinearMap.toMatrix_mulVec_repr LorentzVector.stdBasis LorentzVector.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] +open minkowskiMatrix LorentzVector in +@[simp] +lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) : + (toMatrix u v) μ ν = η μ μ * (⟪e μ, e ν⟫ₘ + 2 * ⟪e ν, u⟫ₘ * ⟪e μ, v⟫ₘ + - ⟪e μ, u + v⟫ₘ * ⟪e ν, u + v⟫ₘ / (1 + ⟪u, v.1.1⟫ₘ)) := by + rw [matrix_apply_stdBasis (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 + LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, basis_left, map_smul, smul_eq_mul, map_neg, + mul_eq_mul_left_iff] + have h1 := FuturePointing.one_add_metric_non_zero u v + field_simp + ring_nf + simp -lemma toMatrix_continuous (u : FourVelocity) : Continuous (toMatrix u) := by +open minkowskiMatrix LorentzVector in +lemma toMatrix_continuous (u : FuturePointing d) : 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.comp' (continuous_add_left ⟪e i, e j⟫ₘ) ?_ + refine Continuous.comp' (continuous_mul_left (2 * ⟪e j, u⟫ₘ)) ?_ + exact FuturePointing.metric_continuous _ refine Continuous.mul ?_ ?_ refine Continuous.mul ?_ ?_ - simp only [(ηLin _).map_add] + simp only [(minkowskiMetric _).map_add] refine Continuous.comp' ?_ ?_ - exact continuous_add_left ((ηLin (stdBasis i)) ↑u) - exact η_continuous _ - simp only [(ηLin _).map_add] + exact continuous_add_left ((minkowskiMetric (stdBasis i)) ↑u) + exact FuturePointing.metric_continuous _ + simp only [(minkowskiMetric _).map_add] refine Continuous.comp' ?_ ?_ exact continuous_add_left _ - exact η_continuous _ + exact FuturePointing.metric_continuous _ refine Continuous.inv₀ ?_ ?_ refine Continuous.comp' (continuous_add_left 1) ?_ - exact η_continuous _ - exact fun x => one_plus_ne_zero u x + exact FuturePointing.metric_continuous _ + exact fun x => FuturePointing.one_add_metric_non_zero u x -lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u v) := by +lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ LorentzGroup d:= 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 + have h1 : (1 + (minkowskiMetric ↑u) ↑v.1.1) ≠ 0 := FuturePointing.one_add_metric_non_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] + rw [u.1.2, v.1.2, minkowskiMetric.symm v.1.1 u, minkowskiMetric.symm u y, + minkowskiMetric.symm v y] ring /-- A generalised boost as an element of the Lorentz Group. -/ -def toLorentz (u v : FourVelocity) : LorentzGroup := - ⟨toMatrix u v, toMatrix_PreservesηLin u v⟩ +def toLorentz (u v : FuturePointing d) : LorentzGroup d := + ⟨toMatrix u v, toMatrix_in_lorentzGroup u v⟩ -lemma toLorentz_continuous (u : FourVelocity) : Continuous (toLorentz u) := by - refine Continuous.subtype_mk ?_ (fun x => toMatrix_PreservesηLin u x) +lemma toLorentz_continuous (u : FuturePointing d) : Continuous (toLorentz u) := by + refine Continuous.subtype_mk ?_ (fun x => toMatrix_in_lorentzGroup u x) exact 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 +lemma toLorentz_joined_to_1 (u v : FuturePointing d) : Joined 1 (toLorentz u v) := by + obtain ⟨f, _⟩ := FuturePointing.isPathConnected.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] - simp [PreservesηLin.liftGL, toMatrix, self u] + simp [toMatrix, self u] · simp -lemma toLorentz_in_connected_component_1 (u v : FourVelocity) : +lemma toLorentz_in_connected_component_1 (u v : FuturePointing d) : toLorentz u v ∈ connectedComponent 1 := pathComponent_subset_component _ (toLorentz_joined_to_1 u v) -lemma isProper (u v : FourVelocity) : IsProper (toLorentz u v) := +lemma isProper (u v : FuturePointing d) : IsProper (toLorentz u v) := (isProper_on_connected_component (toLorentz_in_connected_component_1 u v)).mp id_IsProper end genBoost diff --git a/HepLean/SpaceTime/LorentzGroup/Rotations.lean b/HepLean/SpaceTime/LorentzGroup/Rotations.lean index 605d025..5172b3f 100644 --- a/HepLean/SpaceTime/LorentzGroup/Rotations.lean +++ b/HepLean/SpaceTime/LorentzGroup/Rotations.lean @@ -9,50 +9,53 @@ import Mathlib.Topology.Constructions /-! # Rotations +This file describes the embedding of `SO(3)` into `LorentzGroup 3`. + +## TODO + +Generalize to arbitrary dimensions. + -/ noncomputable section -namespace SpaceTime -namespace lorentzGroup +namespace LorentzGroup open GroupTheory /-- Given a element of `SO(3)` the matrix corresponding to a space-time rotation. -/ @[simp] -def SO3ToMatrix (A : SO(3)) : Matrix (Fin 4) (Fin 4) ℝ := - Matrix.reindex finSumFinEquiv finSumFinEquiv (Matrix.fromBlocks 1 0 0 A.1) +def SO3ToMatrix (A : SO(3)) : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ := + (Matrix.fromBlocks 1 0 0 A.1) -lemma SO3ToMatrix_PreservesηLin (A : SO(3)) : PreservesηLin $ SO3ToMatrix A := by - rw [PreservesηLin.iff_matrix] - simp only [η_block, Nat.reduceAdd, Matrix.reindex_apply, SO3ToMatrix, Matrix.transpose_submatrix, +lemma SO3ToMatrix_in_LorentzGroup (A : SO(3)) : SO3ToMatrix A ∈ LorentzGroup 3 := by + rw [LorentzGroup.mem_iff_dual_mul_self] + simp only [minkowskiMetric.dual, minkowskiMatrix.as_block, SO3ToMatrix, Matrix.fromBlocks_transpose, Matrix.transpose_one, Matrix.transpose_zero, - Matrix.submatrix_mul_equiv, Matrix.fromBlocks_multiply, mul_one, Matrix.mul_zero, add_zero, - Matrix.zero_mul, Matrix.mul_one, neg_mul, one_mul, zero_add, Matrix.mul_neg, neg_zero, mul_neg, - neg_neg, Matrix.mul_eq_one_comm.mpr A.2.2, Matrix.fromBlocks_one, Matrix.submatrix_one_equiv] + Matrix.fromBlocks_multiply, mul_one, Matrix.mul_zero, add_zero, Matrix.zero_mul, Matrix.mul_one, + neg_mul, one_mul, zero_add, Matrix.mul_neg, neg_zero, mul_neg, neg_neg, + Matrix.mul_eq_one_comm.mpr A.2.2, Matrix.fromBlocks_one] lemma SO3ToMatrix_injective : Function.Injective SO3ToMatrix := by intro A B h erw [Equiv.apply_eq_iff_eq] at h have h1 := congrArg Matrix.toBlocks₂₂ h - rw [Matrix.toBlocks_fromBlocks₂₂, Matrix.toBlocks_fromBlocks₂₂] at h1 + erw [Matrix.toBlocks_fromBlocks₂₂, Matrix.toBlocks_fromBlocks₂₂] at h1 apply Subtype.eq exact h1 /-- Given a element of `SO(3)` the element of the Lorentz group corresponding to a space-time rotation. -/ -def SO3ToLorentz : SO(3) →* 𝓛 where - toFun A := ⟨SO3ToMatrix A, SO3ToMatrix_PreservesηLin A⟩ +def SO3ToLorentz : SO(3) →* LorentzGroup 3 where + toFun A := ⟨SO3ToMatrix A, SO3ToMatrix_in_LorentzGroup A⟩ map_one' := by apply Subtype.eq simp only [SO3ToMatrix, Nat.reduceAdd, Matrix.reindex_apply, lorentzGroupIsGroup_one_coe] erw [Matrix.fromBlocks_one] - exact Matrix.submatrix_one_equiv finSumFinEquiv.symm map_mul' A B := by apply Subtype.eq simp [Matrix.fromBlocks_multiply] -end lorentzGroup +end LorentzGroup -end SpaceTime end diff --git a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean new file mode 100644 index 0000000..6fbdcb5 --- /dev/null +++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean @@ -0,0 +1,145 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.MinkowskiMetric +import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup +/-! +# Spacetime as a self-adjoint matrix + +There is a linear equivalence between the vector space of space-time points +and the vector space of 2×2-complex self-adjoint matrices. + +In this file we define this linear equivalence in `toSelfAdjointMatrix`. + +## TODO + +If possible generalize to arbitrary dimensions. + +-/ +namespace SpaceTime + +open Matrix +open MatrixGroups +open Complex + +/-- A 2×2-complex matrix formed from a space-time point. -/ +@[simp] +def toMatrix (x : LorentzVector 3) : Matrix (Fin 2) (Fin 2) ℂ := + !![x.time + x.space 2, x.space 0 - x.space 1 * I; x.space 0 + x.space 1 * I, x.time - x.space 2] + +/-- The matrix `x.toMatrix` for `x ∈ spaceTime` is self adjoint. -/ +lemma toMatrix_isSelfAdjoint (x : LorentzVector 3) : IsSelfAdjoint (toMatrix x) := by + rw [isSelfAdjoint_iff, star_eq_conjTranspose, ← Matrix.ext_iff] + intro i j + fin_cases i <;> fin_cases j <;> + simp [toMatrix, conj_ofReal] + rfl + +/-- A self-adjoint matrix formed from a space-time point. -/ +@[simps!] +def toSelfAdjointMatrix' (x : LorentzVector 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) := + ⟨toMatrix x, toMatrix_isSelfAdjoint x⟩ + +/-- A self-adjoint matrix formed from a space-time point. -/ +@[simp] +noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : + LorentzVector 3 := fun i => + match i with + | Sum.inl 0 => 1/2 * (x.1 0 0 + x.1 1 1).re + | Sum.inr 0 => (x.1 1 0).re + | Sum.inr 1 => (x.1 1 0).im + | Sum.inr 2 => 1/2 * (x.1 0 0 - x.1 1 1).re + + +/-- The linear equivalence between the vector-space `spaceTime` and self-adjoint + 2×2-complex matrices. -/ +noncomputable def toSelfAdjointMatrix : + LorentzVector 3 ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where + toFun := toSelfAdjointMatrix' + invFun := fromSelfAdjointMatrix' + left_inv x := by + funext i + match i with + | Sum.inl 0 => + simp [fromSelfAdjointMatrix', toSelfAdjointMatrix', toMatrix, toMatrix_isSelfAdjoint] + ring_nf + | Sum.inr 0 => + simp [fromSelfAdjointMatrix', toSelfAdjointMatrix', toMatrix, toMatrix_isSelfAdjoint] + | Sum.inr 1 => + simp [fromSelfAdjointMatrix', toSelfAdjointMatrix', toMatrix, toMatrix_isSelfAdjoint] + | Sum.inr 2 => + simp [fromSelfAdjointMatrix', toSelfAdjointMatrix', toMatrix, toMatrix_isSelfAdjoint] + ring + right_inv x := by + simp only [toSelfAdjointMatrix', toMatrix, LorentzVector.time, fromSelfAdjointMatrix', one_div, + Fin.isValue, add_re, ofReal_mul, ofReal_inv, ofReal_ofNat, ofReal_add, LorentzVector.space, + Function.comp_apply, sub_re, ofReal_sub, re_add_im] + ext i j + fin_cases i <;> fin_cases j <;> + field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal] + exact conj_eq_iff_re.mp (congrArg (fun M => M 0 0) $ selfAdjoint.mem_iff.mp x.2 ) + have h01 := congrArg (fun M => M 0 1) $ selfAdjoint.mem_iff.mp x.2 + simp only [Fin.isValue, star_apply, RCLike.star_def] at h01 + rw [← h01, RCLike.conj_eq_re_sub_im] + rfl + exact conj_eq_iff_re.mp (congrArg (fun M => M 1 1) $ selfAdjoint.mem_iff.mp x.2 ) + map_add' x y := by + ext i j : 2 + simp only [toSelfAdjointMatrix'_coe, add_apply, ofReal_add, of_apply, cons_val', empty_val', + cons_val_fin_one, AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, Matrix.add_apply] + fin_cases i <;> fin_cases j + · rw [show (x + y) (Sum.inl 0) = x (Sum.inl 0) + y (Sum.inl 0) from rfl] + rw [show (x + y) (Sum.inr 2) = x (Sum.inr 2) + y (Sum.inr 2) from rfl] + simp only [Fin.isValue, ofReal_add, Fin.zero_eta, cons_val_zero] + ring + · rw [show (x + y) (Sum.inr 0) = x (Sum.inr 0) + y (Sum.inr 0) from rfl] + rw [show (x + y) (Sum.inr 1) = x (Sum.inr 1) + y (Sum.inr 1) from rfl] + simp only [Fin.isValue, ofReal_add, Fin.mk_one, cons_val_one, head_cons, Fin.zero_eta, + cons_val_zero] + ring + · rw [show (x + y) (Sum.inr 0) = x (Sum.inr 0) + y (Sum.inr 0) from rfl] + rw [show (x + y) (Sum.inr 1) = x (Sum.inr 1) + y (Sum.inr 1) from rfl] + simp only [Fin.isValue, ofReal_add, Fin.zero_eta, cons_val_zero, Fin.mk_one, cons_val_one, + head_fin_const] + ring + · rw [show (x + y) (Sum.inl 0) = x (Sum.inl 0) + y (Sum.inl 0) from rfl] + rw [show (x + y) (Sum.inr 2) = x (Sum.inr 2) + y (Sum.inr 2) from rfl] + simp only [Fin.isValue, ofReal_add, Fin.mk_one, cons_val_one, head_cons, head_fin_const] + ring + map_smul' r x := by + ext i j : 2 + simp only [toSelfAdjointMatrix'_coe, Fin.isValue, of_apply, cons_val', empty_val', + cons_val_fin_one, RingHom.id_apply, selfAdjoint.val_smul, smul_apply, real_smul] + fin_cases i <;> fin_cases j + · rw [show (r • x) (Sum.inl 0) = r * x (Sum.inl 0) from rfl] + rw [show (r • x) (Sum.inr 2) = r * x (Sum.inr 2) from rfl] + simp only [Fin.isValue, ofReal_mul, Fin.zero_eta, cons_val_zero] + ring + · rw [show (r • x) (Sum.inr 0) = r * x (Sum.inr 0) from rfl] + rw [show (r • x) (Sum.inr 1) = r * x (Sum.inr 1) from rfl] + simp only [Fin.isValue, ofReal_mul, Fin.mk_one, cons_val_one, head_cons, Fin.zero_eta, + cons_val_zero] + ring + · rw [show (r • x) (Sum.inr 0) = r * x (Sum.inr 0) from rfl] + rw [show (r • x) (Sum.inr 1) = r * x (Sum.inr 1) from rfl] + simp only [Fin.isValue, ofReal_mul, Fin.zero_eta, cons_val_zero, Fin.mk_one, cons_val_one, + head_fin_const] + ring + · rw [show (r • x) (Sum.inl 0) = r * x (Sum.inl 0) from rfl] + rw [show (r • x) (Sum.inr 2) = r * x (Sum.inr 2) from rfl] + simp only [Fin.isValue, ofReal_mul, Fin.mk_one, cons_val_one, head_cons, head_fin_const] + ring + +open minkowskiMetric in +lemma det_eq_ηLin (x : LorentzVector 3) : det (toSelfAdjointMatrix x).1 = ⟪x, x⟫ₘ := by + simp only [toSelfAdjointMatrix, LinearEquiv.coe_mk, toSelfAdjointMatrix'_coe, Fin.isValue, + det_fin_two_of, eq_time_minus_inner_prod, LorentzVector.time, LorentzVector.space, + PiLp.inner_apply, Function.comp_apply, RCLike.inner_apply, conj_trivial, Fin.sum_univ_three, + ofReal_sub, ofReal_mul, ofReal_add] + ring_nf + simp only [Fin.isValue, I_sq, mul_neg, mul_one] + ring + +end SpaceTime diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean index 9b58852..72d9a06 100644 --- a/HepLean/SpaceTime/LorentzVector/Basic.lean +++ b/HepLean/SpaceTime/LorentzVector/Basic.lean @@ -33,6 +33,11 @@ noncomputable instance : Module ℝ (LorentzVector d) := Pi.module _ _ _ instance : AddCommGroup (LorentzVector d) := Pi.addCommGroup +/-- The structure of a topological space `LorentzVector d`. -/ +instance : TopologicalSpace (LorentzVector d) := + haveI : NormedAddCommGroup (LorentzVector d) := Pi.normedAddCommGroup + UniformSpace.toTopologicalSpace + namespace LorentzVector variable {d : ℕ} @@ -53,26 +58,29 @@ def time : ℝ := v (Sum.inl 0) -/ -/-- The standard basis of `LorentzVector`. -/ +/-- The standard basis of `LorentzVector` indexed by `Fin 1 ⊕ Fin (d)`. -/ @[simps!] noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin (d)) ℝ (LorentzVector d) := Pi.basisFun ℝ _ +scoped[LorentzVector] notation "e" => stdBasis + +lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : e μ ν = if μ = ν then 1 else 0 := by + rw [stdBasis] + erw [Pi.basisFun_apply] + simp + /-- The standard unit time vector. -/ -@[simp] -noncomputable def timeVec : (LorentzVector d) := stdBasis (Sum.inl 0) +noncomputable abbrev timeVec : (LorentzVector d) := e (Sum.inl 0) @[simp] lemma timeVec_space : (@timeVec d).space = 0 := by funext i - simp [space, stdBasis] - erw [Pi.basisFun_apply] - simp_all only [Fin.isValue, LinearMap.stdBasis_apply', ↓reduceIte] + simp only [space, Function.comp_apply, stdBasis_apply, Fin.isValue, ↓reduceIte, PiLp.zero_apply] @[simp] lemma timeVec_time: (@timeVec d).time = 1 := by - simp [space, stdBasis] - erw [Pi.basisFun_apply] - simp_all only [Fin.isValue, LinearMap.stdBasis_apply', ↓reduceIte] + simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte] + /-! diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean index 588db82..3e96884 100644 --- a/HepLean/SpaceTime/LorentzVector/NormOne.lean +++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean @@ -17,10 +17,13 @@ open minkowskiMetric def NormOneLorentzVector (d : ℕ) : Set (LorentzVector d) := fun x => ⟪x, x⟫ₘ = 1 +instance : TopologicalSpace (NormOneLorentzVector d) := instTopologicalSpaceSubtype + namespace NormOneLorentzVector variable {d : ℕ} +section variable (v w : NormOneLorentzVector d) lemma mem_iff {x : LorentzVector d} : x ∈ NormOneLorentzVector d ↔ ⟪x, x⟫ₘ = 1 := by @@ -91,8 +94,11 @@ lemma time_abs_sub_space_norm : def FuturePointing (d : ℕ) : Set (NormOneLorentzVector d) := fun x => 0 < x.1.time +instance : TopologicalSpace (FuturePointing d) := instTopologicalSpaceSubtype + namespace FuturePointing +section variable (f f' : FuturePointing d) lemma mem_iff : v ∈ FuturePointing d ↔ 0 < v.1.time := by @@ -124,9 +130,30 @@ lemma time_nonneg : 0 ≤ f.1.1.time := le_of_lt f.2 lemma abs_time : |f.1.1.time| = f.1.1.time := abs_of_nonneg (time_nonneg f) +lemma time_eq_sqrt : f.1.1.time = √(1 + ‖f.1.1.space‖ ^ 2) := by + symm + rw [Real.sqrt_eq_cases] + apply Or.inl + rw [← time_sq, sq] + exact ⟨rfl, time_nonneg f⟩ + /-! -# The value sign of ⟪v, w.1.spaceReflection⟫ₘ different v and w +# The sign of ⟪v, w.1⟫ₘ different v and w + +-/ + +lemma metric_nonneg : 0 ≤ ⟪f, f'.1.1⟫ₘ := by + apply le_trans (time_abs_sub_space_norm f f'.1) + rw [abs_time f, abs_time f'] + exact ge_sub_norm f.1.1 f'.1.1 + +lemma one_add_metric_non_zero : 1 + ⟪f, f'.1.1⟫ₘ ≠ 0 := by + linarith [metric_nonneg f f'] + +/-! + +# The sign of ⟪v, w.1.spaceReflection⟫ₘ different v and w -/ @@ -165,6 +192,108 @@ lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw : w ∈ Futur simp [neg] end +end + +end FuturePointing +end + +namespace FuturePointing +/-! + +# Topology + +-/ +open LorentzVector + +/-- The `FuturePointing d` which has all space components zero. -/ +@[simps!] +noncomputable def timeVecNormOneFuture : FuturePointing d := ⟨⟨timeVec, by + rw [NormOneLorentzVector.mem_iff, on_timeVec]⟩, by + rw [mem_iff, timeVec_time]; simp⟩ + + +/-- A continuous path from `timeVecNormOneFuture` to any other. -/ +noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFuture u where + toFun t := ⟨ + ⟨fun i => match i with + | Sum.inl 0 => √(1 + t ^ 2 * ‖u.1.1.space‖ ^ 2) + | Sum.inr i => t * u.1.1.space i, + by + rw [NormOneLorentzVector.mem_iff, minkowskiMetric.eq_time_minus_inner_prod] + simp only [time, space, Function.comp_apply, PiLp.inner_apply, RCLike.inner_apply, map_mul, + conj_trivial] + rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply] + simp only [Function.comp_apply, RCLike.inner_apply, conj_trivial] + have h1 : ∑ x : Fin d, t.1 * u.1.1 (Sum.inr x) * (↑t.1 * u.1.1 (Sum.inr x)) = + t ^ 2 * ∑ x : Fin d, u.1.1 (Sum.inr x) * u.1.1 (Sum.inr x) := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro i _ + ring + rw [h1] + ring + refine Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩, + by + simp only [space, Function.comp_apply, mem_iff_time_nonneg, time, Real.sqrt_pos] + exact Real.sqrt_nonneg _⟩ + continuous_toFun := by + refine Continuous.subtype_mk ?_ _ + refine Continuous.subtype_mk ?_ _ + apply (continuous_pi_iff).mpr + intro i + match i with + | Sum.inl 0 => + continuity + | Sum.inr i => + continuity + source' := by + ext + funext i + match i with + | Sum.inl 0 => + simp only [Set.Icc.coe_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, space, + zero_mul, add_zero, Real.sqrt_one, Fin.isValue, timeVecNormOneFuture_coe_coe] + exact Eq.symm timeVec_time + | Sum.inr i => + simp only [Set.Icc.coe_zero, space, Function.comp_apply, zero_mul, + timeVecNormOneFuture_coe_coe] + change _ = timeVec.space i + rw [timeVec_space] + rfl + target' := by + ext + funext i + match i with + | Sum.inl 0 => + simp only [Set.Icc.coe_one, one_pow, space, one_mul, Fin.isValue] + exact (time_eq_sqrt u).symm + | Sum.inr i => + simp only [Set.Icc.coe_one, one_pow, space, one_mul, Fin.isValue] + exact rfl + + + + +lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by + use timeVecNormOneFuture + apply And.intro trivial ?_ + intro y a + use pathFromTime y + exact fun _ => a + + +lemma metric_continuous (u : LorentzVector d) : + Continuous (fun (a : FuturePointing d) => ⟪u, a.1.1⟫ₘ) := by + simp only [minkowskiMetric.eq_time_minus_inner_prod] + refine Continuous.add ?_ ?_ + · refine Continuous.comp' (continuous_mul_left _) $ Continuous.comp' + (continuous_apply (Sum.inl 0)) + (Continuous.comp' continuous_subtype_val continuous_subtype_val) + · refine Continuous.comp' continuous_neg $ Continuous.inner + (Continuous.comp' (Pi.continuous_precomp Sum.inr) continuous_const) + (Continuous.comp' (Pi.continuous_precomp Sum.inr) (Continuous.comp' + continuous_subtype_val continuous_subtype_val)) + end FuturePointing diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean deleted file mode 100644 index 3c54274..0000000 --- a/HepLean/SpaceTime/Metric.lean +++ /dev/null @@ -1,273 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license. -Authors: Joseph Tooby-Smith --/ -import HepLean.SpaceTime.Basic -import Mathlib.Algebra.Lie.Classical -import Mathlib.LinearAlgebra.QuadraticForm.Basic -/-! -# Spacetime Metric - -This file introduces the metric on spacetime in the (+, -, -, -) signature. - -## TODO - -This file needs refactoring. -- The metric should be defined as a bilinear map on `LorentzVector d`. -- From this definition, we should derive the metric as a matrix. - --/ - -noncomputable section - -namespace SpaceTime - -open Manifold -open Matrix -open Complex -open ComplexConjugate -open TensorProduct - -/-- The metric as a `4×4` real matrix. -/ -def η : Matrix (Fin 4) (Fin 4) ℝ := Matrix.reindex finSumFinEquiv finSumFinEquiv - $ LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ - -/-- The metric with lower indices. -/ -notation "η_[" μ "]_[" ν "]" => η μ ν - -/-- The inverse of `η`. Used for notation. -/ -def ηInv : Matrix (Fin 4) (Fin 4) ℝ := η - -/-- The metric with upper indices. -/ -notation "η^[" μ "]^[" ν "]" => ηInv μ ν - -/-- A matrix with one lower and one upper index. -/ -notation "["Λ"]^[" μ "]_[" ν "]" => (Λ : Matrix (Fin 4) (Fin 4) ℝ) μ ν - -/-- A matrix with both lower indices. -/ -notation "["Λ"]_[" μ "]_[" ν "]" => ∑ ρ, η_[μ]_[ρ] * [Λ]^[ρ]_[ν] - -/-- `η` with $η^μ_ν$ indices. This is equivalent to the identity. This is used for notation. -/ -def ηUpDown : Matrix (Fin 4) (Fin 4) ℝ := 1 - -/-- The metric with one lower and one upper index. -/ -notation "η^[" μ "]_[" ν "]" => ηUpDown μ ν - - -lemma η_block : η = Matrix.reindex finSumFinEquiv finSumFinEquiv ( - Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin 3) (Fin 3) ℝ)) := by - rw [η] - congr - simp [LieAlgebra.Orthogonal.indefiniteDiagonal] - rw [← fromBlocks_diagonal] - refine fromBlocks_inj.mpr ?_ - simp only [diagonal_one, true_and] - funext i j - rw [← diagonal_neg] - rfl - -lemma η_reindex : (Matrix.reindex finSumFinEquiv finSumFinEquiv).symm η = - LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ := - (Equiv.symm_apply_eq (reindex finSumFinEquiv finSumFinEquiv)).mpr rfl - -lemma η_explicit : η = !![(1 : ℝ), 0, 0, 0; 0, -1, 0, 0; 0, 0, -1, 0; 0, 0, 0, -1] := by - rw [η_block] - apply Matrix.ext - intro i j - fin_cases i <;> fin_cases j - <;> simp_all only [Fin.zero_eta, reindex_apply, submatrix_apply] - any_goals rfl - all_goals simp [finSumFinEquiv, Fin.addCases, η, vecHead, vecTail] - any_goals rfl - all_goals split - all_goals simp - all_goals rfl - -@[simp] -lemma η_off_diagonal {μ ν : Fin 4} (h : μ ≠ ν) : η μ ν = 0 := by - fin_cases μ <;> - fin_cases ν <;> - simp_all [η_explicit, Fin.mk_one, Fin.mk_one, vecHead, vecTail] - -lemma η_symmetric (μ ν : Fin 4) : η μ ν = η ν μ := by - by_cases h : μ = ν - rw [h] - rw [η_off_diagonal h] - exact Eq.symm (η_off_diagonal fun a => h (id (Eq.symm a))) - -@[simp] -lemma η_transpose : η.transpose = η := by - funext μ ν - rw [transpose_apply, η_symmetric] - -@[simp] -lemma det_η : η.det = - 1 := by - simp [η_explicit, det_succ_row_zero, Fin.sum_univ_succ] - -@[simp] -lemma η_sq : η * η = 1 := by - funext μ ν - fin_cases μ <;> fin_cases ν <;> - simp [η_explicit, vecHead, vecTail] - -lemma η_diag_mul_self (μ : Fin 4) : η μ μ * η μ μ = 1 := by - fin_cases μ <;> simp [η_explicit] - -lemma η_mulVec (x : SpaceTime) : η *ᵥ x = ![x 0, -x 1, -x 2, -x 3] := by - rw [explicit x, η_explicit] - funext i - fin_cases i <;> - simp [vecHead, vecTail] - -lemma η_as_diagonal : η = diagonal ![1, -1, -1, -1] := by - rw [η_explicit] - apply Matrix.ext - intro μ ν - fin_cases μ <;> fin_cases ν <;> rfl - -lemma η_mul (Λ : Matrix (Fin 4) (Fin 4) ℝ) (μ ρ : Fin 4) : - [η * Λ]^[μ]_[ρ] = [η]^[μ]_[μ] * [Λ]^[μ]_[ρ] := by - rw [η_as_diagonal, @diagonal_mul, diagonal_apply_eq ![1, -1, -1, -1] μ] - -lemma mul_η (Λ : Matrix (Fin 4) (Fin 4) ℝ) (μ ρ : Fin 4) : - [Λ * η]^[μ]_[ρ] = [Λ]^[μ]_[ρ] * [η]^[ρ]_[ρ] := by - rw [η_as_diagonal, @mul_diagonal, diagonal_apply_eq ![1, -1, -1, -1] ρ] - -lemma η_mul_self (μ ν : Fin 4) : η^[ν]_[μ] * η_[ν]_[ν] = η_[μ]_[ν] := by - fin_cases μ <;> fin_cases ν <;> simp [ηUpDown] - -lemma η_contract_self (μ ν : Fin 4) : ∑ x, (η^[x]_[μ] * η_[x]_[ν]) = η_[μ]_[ν] := by - rw [Fin.sum_univ_four] - fin_cases μ <;> fin_cases ν <;> simp [ηUpDown] - -lemma η_contract_self' (μ ν : Fin 4) : ∑ x, (η^[x]_[μ] * η_[ν]_[x]) = η_[ν]_[μ] := by - rw [Fin.sum_univ_four] - fin_cases μ <;> fin_cases ν <;> simp [ηUpDown] - - - -/-- Given a point in spaceTime `x` the linear map `y → x ⬝ᵥ (η *ᵥ y)`. -/ -@[simps!] -def linearMapForSpaceTime (x : SpaceTime) : SpaceTime →ₗ[ℝ] ℝ where - toFun y := x ⬝ᵥ (η *ᵥ y) - map_add' y z := by - simp only - rw [mulVec_add, dotProduct_add] - map_smul' c y := by - simp only [RingHom.id_apply, smul_eq_mul] - rw [mulVec_smul, dotProduct_smul] - rfl - -/-- The metric as a bilinear map from `spaceTime` to `ℝ`. -/ -def ηLin : LinearMap.BilinForm ℝ SpaceTime where - toFun x := linearMapForSpaceTime x - map_add' x y := by - apply LinearMap.ext - intro z - simp only [linearMapForSpaceTime_apply, LinearMap.add_apply] - rw [add_dotProduct] - map_smul' c x := by - apply LinearMap.ext - intro z - simp only [linearMapForSpaceTime_apply, RingHom.id_apply, LinearMap.smul_apply, smul_eq_mul] - rw [smul_dotProduct] - rfl - -lemma ηLin_expand (x y : SpaceTime) : ηLin x y = x 0 * y 0 - x 1 * y 1 - x 2 * y 2 - x 3 * y 3 := by - rw [ηLin] - simp only [LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply, Fin.isValue] - erw [η_mulVec] - nth_rewrite 1 [explicit x] - simp only [dotProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.sum_univ_four, - 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] - noncomm_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] - exact (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] - noncomm_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 - -lemma ηLin_stdBasis_apply (μ : Fin 4) (x : SpaceTime) : ηLin (stdBasis μ) x = η μ μ * x μ := by - rw [ηLin_expand] - fin_cases μ - <;> simp [stdBasis_0, stdBasis_1, stdBasis_2, stdBasis_3, η_explicit] - - -lemma ηLin_η_stdBasis (μ ν : Fin 4) : ηLin (stdBasis μ) (stdBasis ν) = η μ ν := by - rw [ηLin_stdBasis_apply] - by_cases h : μ = ν - · rw [stdBasis_apply] - subst h - simp - · rw [stdBasis_not_eq, η_off_diagonal h] - exact CommMonoidWithZero.mul_zero η_[μ]_[μ] - exact fun a ↦ h (id a.symm) - -set_option maxHeartbeats 0 -lemma ηLin_mulVec_left (x y : SpaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - ηLin (Λ *ᵥ x) y = ηLin x ((η * Λᵀ * η) *ᵥ y) := by - simp [ηLin, LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply, - mulVec_mulVec, (vecMul_transpose Λ x).symm, ← dotProduct_mulVec, mulVec_mulVec, - ← mul_assoc, ← mul_assoc, η_sq, one_mul] - -lemma ηLin_mulVec_right (x y : SpaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - ηLin x (Λ *ᵥ y) = ηLin ((η * Λᵀ * η) *ᵥ x) y := by - rw [ηLin_symm, ηLin_symm ((η * Λᵀ * η) *ᵥ x) _ ] - exact ηLin_mulVec_left y x Λ - -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, one_mulVec, implies_true] - · intro h - funext μ ν - have h1 := h (stdBasis μ) (stdBasis ν) - rw [ηLin_matrix_stdBasis, ηLin_η_stdBasis] at h1 - fin_cases μ <;> fin_cases ν <;> - simp_all [η_explicit, Fin.mk_one, Fin.mk_one, vecHead, vecTail] - -/-- The metric as a quadratic form on `spaceTime`. -/ -def quadraticForm : QuadraticForm ℝ SpaceTime := ηLin.toQuadraticForm - -end SpaceTime - -end diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean index bfc842d..27ad271 100644 --- a/HepLean/SpaceTime/MinkowskiMetric.lean +++ b/HepLean/SpaceTime/MinkowskiMetric.lean @@ -60,6 +60,17 @@ lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] +lemma as_block : @minkowskiMatrix d = ( + Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin d) (Fin d) ℝ)) := by + rw [minkowskiMatrix] + congr + simp [LieAlgebra.Orthogonal.indefiniteDiagonal] + rw [← fromBlocks_diagonal] + refine fromBlocks_inj.mpr ?_ + simp only [diagonal_one, true_and] + funext i j + rw [← diagonal_neg] + rfl end minkowskiMatrix @@ -204,15 +215,6 @@ lemma ge_sub_norm : v.time * w.time - ‖v.space‖ * ‖w.space‖ ≤ ⟪v, w rw [sub_le_sub_iff_left] exact norm_inner_le_norm v.space w.space -/-! - -# The Minkowski metric and the standard basis - --/ - -lemma on_timeVec : ⟪timeVec, @timeVec d⟫ₘ = 1 := by - rw [self_eq_time_minus_norm, timeVec_time, timeVec_space] - simp [LorentzVector.stdBasis, minkowskiMetric] /-! @@ -302,6 +304,51 @@ lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ simp -end matrices +/-! +# The Minkowski metric and the standard basis + +-/ + +@[simp] +lemma basis_left (μ : Fin 1 ⊕ Fin d) : ⟪e μ, v⟫ₘ = η μ μ * v μ := by + rw [as_sum] + rcases μ with μ | μ + · fin_cases μ + simp [stdBasis_apply, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] + · simp [stdBasis_apply, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] + +@[simp] +lemma on_timeVec : ⟪timeVec, @timeVec d⟫ₘ = 1 := by + simp only [timeVec, Fin.isValue, basis_left, minkowskiMatrix, + LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_apply_eq, Sum.elim_inl, stdBasis_apply, + ↓reduceIte, mul_one] + +@[simp] +lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, Λ *ᵥ e ν⟫ₘ = η μ μ * Λ μ ν := by + simp [basis_left, mulVec, dotProduct, stdBasis_apply] + +@[simp] +lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, e ν⟫ₘ = η μ ν := by + rw [basis_left, stdBasis_apply] + by_cases h : μ = ν + · simp [h] + · simp [h, LieAlgebra.Orthogonal.indefiniteDiagonal, minkowskiMatrix] + exact fun a => False.elim (h (id (Eq.symm a))) + +lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d): + Λ ν μ = η ν ν * ⟪e ν, Λ *ᵥ e μ⟫ₘ := by + rw [on_basis_mulVec, ← mul_assoc] + have h1 : η ν ν * η ν ν = 1 := by + simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] + rcases μ + · rcases ν + · simp_all only [Sum.elim_inl, mul_one] + · simp_all only [Sum.elim_inr, mul_neg, mul_one, neg_neg] + · rcases ν + · simp_all only [Sum.elim_inl, mul_one] + · simp_all only [Sum.elim_inr, mul_neg, mul_one, neg_neg] + simp [h1] + +end matrices end minkowskiMetric diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean index 9de6358..34e6ee2 100644 --- a/HepLean/SpaceTime/SL2C/Basic.lean +++ b/HepLean/SpaceTime/SL2C/Basic.lean @@ -64,7 +64,7 @@ def repSelfAdjointMatrix : Representation ℝ SL(2, ℂ) $ selfAdjoint (Matrix ( /-- The representation of `SL(2, ℂ)` on `spaceTime` obtained from `toSelfAdjointMatrix` and `repSelfAdjointMatrix`. -/ -def repSpaceTime : Representation ℝ SL(2, ℂ) SpaceTime where +def repLorentzVector : Representation ℝ SL(2, ℂ) (LorentzVector 3) where toFun M := toSelfAdjointMatrix.symm.comp ((repSelfAdjointMatrix M).comp toSelfAdjointMatrix.toLinearMap) map_one' := by @@ -84,15 +84,28 @@ In the next section we will restrict this homomorphism to the restricted Lorentz -/ +lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ): Λ ∈ LorentzGroup 3 ↔ + ∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)), + det ((toSelfAdjointMatrix ∘ toLin LorentzVector.stdBasis LorentzVector.stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1 + = det x.1 := by + rw [LorentzGroup.mem_iff_norm] + apply Iff.intro + intro h x + have h1 := congrArg ofReal $ h (toSelfAdjointMatrix.symm x) + simpa [← det_eq_ηLin] using h1 + intro h x + have h1 := h (toSelfAdjointMatrix x) + simpa [det_eq_ηLin] using h1 + /-- Given an element `M ∈ SL(2, ℂ)` the corresponding element of the Lorentz group. -/ @[simps!] -def toLorentzGroupElem (M : SL(2, ℂ)) : 𝓛 := - ⟨LinearMap.toMatrix stdBasis stdBasis (repSpaceTime M) , - by simp [repSpaceTime, PreservesηLin.iff_det_selfAdjoint]⟩ +def toLorentzGroupElem (M : SL(2, ℂ)) : LorentzGroup 3 := + ⟨LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (repLorentzVector M) , + by simp [repLorentzVector, iff_det_selfAdjoint]⟩ /-- The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`. -/ @[simps!] -def toLorentzGroup : SL(2, ℂ) →* 𝓛 where +def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where toFun := toLorentzGroupElem map_one' := by simp only [toLorentzGroupElem, _root_.map_one, LinearMap.toMatrix_one] diff --git a/scripts/lint-all.sh b/scripts/lint-all.sh index 6c91394..3abf224 100755 --- a/scripts/lint-all.sh +++ b/scripts/lint-all.sh @@ -1,6 +1,5 @@ #!/usr/bin/env bash -python3 ./scripts/check-file-import.py echo "Running linter for Lean files" From 304c3542b5bf97fab57f8b884e1915420a84bec4 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 2 Jul 2024 10:26:21 -0400 Subject: [PATCH 3/6] refactor: Lint --- HepLean/SpaceTime/LorentzAlgebra/Basic.lean | 3 +-- HepLean/SpaceTime/LorentzGroup/Basic.lean | 5 ----- HepLean/SpaceTime/LorentzGroup/Orthochronous.lean | 1 - HepLean/SpaceTime/LorentzGroup/Proper.lean | 1 - HepLean/SpaceTime/LorentzVector/Basic.lean | 11 +---------- HepLean/SpaceTime/LorentzVector/NormOne.lean | 8 +++----- HepLean/SpaceTime/MinkowskiMetric.lean | 6 ++---- HepLean/SpaceTime/SL2C/Basic.lean | 4 +++- 8 files changed, 10 insertions(+), 29 deletions(-) diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean index 2375989..8f14a5d 100644 --- a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean +++ b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean @@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import HepLean.SpaceTime.Basic import HepLean.SpaceTime.MinkowskiMetric import Mathlib.Algebra.Lie.Classical /-! @@ -42,7 +41,7 @@ lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h lemma mem_iff {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} : - A ∈ lorentzAlgebra ↔ Aᵀ * η = - η * A := + A ∈ lorentzAlgebra ↔ Aᵀ * η = - η * A := Iff.intro (fun h => transpose_eta ⟨A, h⟩) (fun h => mem_of_transpose_eta_eq_eta_mul_self h) lemma mem_iff' (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) : diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index 9975707..30d2b82 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.MinkowskiMetric -import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix import HepLean.SpaceTime.LorentzVector.NormOne /-! # The Lorentz Group @@ -24,11 +23,8 @@ identity. -/ - noncomputable section - -open Manifold open Matrix open Complex open ComplexConjugate @@ -159,7 +155,6 @@ open minkowskiMetric variable {Λ Λ' : LorentzGroup d} -@[simp] lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= by refine (inv_eq_left_inv ?h).symm exact mem_iff_dual_mul_self.mp Λ.2 diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean index 7719ec4..ea7c655 100644 --- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean +++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean @@ -21,7 +21,6 @@ matrices. noncomputable section -open Manifold open Matrix open Complex open ComplexConjugate diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean index 56b1ff7..2457446 100644 --- a/HepLean/SpaceTime/LorentzGroup/Proper.lean +++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean @@ -15,7 +15,6 @@ We define the give a series of lemmas related to the determinant of the lorentz noncomputable section -open Manifold open Matrix open Complex open ComplexConjugate diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean index 72d9a06..45543c2 100644 --- a/HepLean/SpaceTime/LorentzVector/Basic.lean +++ b/HepLean/SpaceTime/LorentzVector/Basic.lean @@ -4,10 +4,7 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import Mathlib.Data.Complex.Exponential -import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners import Mathlib.Analysis.InnerProductSpace.PiL2 -import Mathlib.LinearAlgebra.Matrix.DotProduct -import LeanCopilot /-! # Lorentz vectors @@ -62,6 +59,7 @@ def time : ℝ := v (Sum.inl 0) @[simps!] noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin (d)) ℝ (LorentzVector d) := Pi.basisFun ℝ _ +/-- Notation for `stdBasis`. -/ scoped[LorentzVector] notation "e" => stdBasis lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : e μ ν = if μ = ν then 1 else 0 := by @@ -72,12 +70,10 @@ lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : e μ ν = if μ = ν then 1 els /-- The standard unit time vector. -/ noncomputable abbrev timeVec : (LorentzVector d) := e (Sum.inl 0) -@[simp] lemma timeVec_space : (@timeVec d).space = 0 := by funext i simp only [space, Function.comp_apply, stdBasis_apply, Fin.isValue, ↓reduceIte, PiLp.zero_apply] -@[simp] lemma timeVec_time: (@timeVec d).time = 1 := by simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte] @@ -106,19 +102,14 @@ def spaceReflectionLin : LorentzVector d →ₗ[ℝ] LorentzVector d where apply smul_eq_mul · simp [ HSMul.hSMul, SMul.smul] - /-- The reflection of space. -/ @[simp] def spaceReflection : LorentzVector d := spaceReflectionLin v -@[simp] lemma spaceReflection_space : v.spaceReflection.space = - v.space := by rfl -@[simp] lemma spaceReflection_time : v.spaceReflection.time = v.time := by rfl - - end LorentzVector diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean index 3e96884..532d8dd 100644 --- a/HepLean/SpaceTime/LorentzVector/NormOne.lean +++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean @@ -13,6 +13,7 @@ import HepLean.SpaceTime.MinkowskiMetric open minkowskiMetric +/-- The set of Lorentz vectors with norm 1. -/ @[simp] def NormOneLorentzVector (d : ℕ) : Set (LorentzVector d) := fun x => ⟪x, x⟫ₘ = 1 @@ -105,11 +106,8 @@ lemma mem_iff : v ∈ FuturePointing d ↔ 0 < v.1.time := by rfl lemma mem_iff_time_nonneg : v ∈ FuturePointing d ↔ 0 ≤ v.1.time := by - refine Iff.intro (fun h => ?_) (fun h => ?_) - exact le_of_lt ((mem_iff v).mp h) - have h1 := (mem_iff v).mp - simp at h1 - rw [@time_nonneg_iff] at h + refine Iff.intro (fun h => le_of_lt h) (fun h => ?_) + rw [time_nonneg_iff] at h rw [mem_iff] linarith diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean index 27ad271..aba0497 100644 --- a/HepLean/SpaceTime/MinkowskiMetric.lean +++ b/HepLean/SpaceTime/MinkowskiMetric.lean @@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzVector.Basic import Mathlib.Algebra.Lie.Classical -import Mathlib.LinearAlgebra.QuadraticForm.Basic /-! # The Minkowski Metric @@ -33,6 +32,7 @@ namespace minkowskiMatrix variable {d : ℕ} +/-- Notation for `minkowskiMatrix`. -/ scoped[minkowskiMatrix] notation "η" => minkowskiMatrix @[simp] @@ -116,6 +116,7 @@ open LorentzVector variable {d : ℕ} variable (v w : LorentzVector d) +/-- Notation for `minkowskiMetric`. -/ scoped[minkowskiMetric] notation "⟪" v "," w "⟫ₘ" => minkowskiMetric v w /-! @@ -318,17 +319,14 @@ lemma basis_left (μ : Fin 1 ⊕ Fin d) : ⟪e μ, v⟫ₘ = η μ μ * v μ : simp [stdBasis_apply, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] · simp [stdBasis_apply, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] -@[simp] lemma on_timeVec : ⟪timeVec, @timeVec d⟫ₘ = 1 := by simp only [timeVec, Fin.isValue, basis_left, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_apply_eq, Sum.elim_inl, stdBasis_apply, ↓reduceIte, mul_one] -@[simp] lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, Λ *ᵥ e ν⟫ₘ = η μ μ * Λ μ ν := by simp [basis_left, mulVec, dotProduct, stdBasis_apply] -@[simp] lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, e ν⟫ₘ = η μ ν := by rw [basis_left, stdBasis_apply] by_cases h : μ = ν diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean index 34e6ee2..d24152c 100644 --- a/HepLean/SpaceTime/SL2C/Basic.lean +++ b/HepLean/SpaceTime/SL2C/Basic.lean @@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.LorentzGroup.Basic import Mathlib.RepresentationTheory.Basic +import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix /-! # The group SL(2, ℂ) and it's relation to the Lorentz group @@ -86,7 +87,8 @@ In the next section we will restrict this homomorphism to the restricted Lorentz lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ): Λ ∈ LorentzGroup 3 ↔ ∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)), - det ((toSelfAdjointMatrix ∘ toLin LorentzVector.stdBasis LorentzVector.stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1 + det ((toSelfAdjointMatrix ∘ + toLin LorentzVector.stdBasis LorentzVector.stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1 = det x.1 := by rw [LorentzGroup.mem_iff_norm] apply Iff.intro From a4afeba3cd68c672836f60dd268abaa2a5dc1dc0 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 2 Jul 2024 10:40:35 -0400 Subject: [PATCH 4/6] refactor: Minor golfing --- HepLean/SpaceTime/LorentzGroup/Basic.lean | 6 ------ HepLean/SpaceTime/LorentzVector/Basic.lean | 10 ++++------ HepLean/SpaceTime/LorentzVector/NormOne.lean | 17 +++++++---------- 3 files changed, 11 insertions(+), 22 deletions(-) diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index 30d2b82..5c737b5 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -89,7 +89,6 @@ lemma mem_iff_self_mul_dual : Λ ∈ LorentzGroup d ↔ Λ * dual Λ = 1 := by rw [mem_iff_dual_mul_self] exact mul_eq_one_comm - lemma mem_iff_transpose : Λ ∈ LorentzGroup d ↔ Λᵀ ∈ LorentzGroup d := by apply Iff.intro · intro h @@ -236,7 +235,6 @@ lemma toGL_embedding : Embedding (@toGL d).toFun where rw [isOpen_induced_iff, isOpen_induced_iff] exact exists_exists_and_eq_and - instance : TopologicalGroup (LorentzGroup d) := Inducing.topologicalGroup toGL toGL_embedding.toInducing @@ -276,9 +274,5 @@ lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') = erw [Pi.basisFun_apply, mulVec_stdBasis] simp - - - - end end LorentzGroup diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean index 45543c2..c3d2a5a 100644 --- a/HepLean/SpaceTime/LorentzVector/Basic.lean +++ b/HepLean/SpaceTime/LorentzVector/Basic.lean @@ -65,7 +65,7 @@ scoped[LorentzVector] notation "e" => stdBasis lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : e μ ν = if μ = ν then 1 else 0 := by rw [stdBasis] erw [Pi.basisFun_apply] - simp + exact LinearMap.stdBasis_apply' ℝ μ ν /-- The standard unit time vector. -/ noncomputable abbrev timeVec : (LorentzVector d) := e (Sum.inl 0) @@ -91,16 +91,14 @@ def spaceReflectionLin : LorentzVector d →ₗ[ℝ] LorentzVector d where map_add' x y := by funext i rcases i with i | i - · simp only [Sum.elim_inl] - apply Eq.refl + · rfl · simp only [Sum.elim_inr, Pi.neg_apply] apply neg_add map_smul' c x := by funext i rcases i with i | i - · simp only [Sum.elim_inl, Pi.smul_apply] - apply smul_eq_mul - · simp [ HSMul.hSMul, SMul.smul] + · rfl + · simp [HSMul.hSMul, SMul.smul] /-- The reflection of space. -/ @[simp] diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean index 532d8dd..2866976 100644 --- a/HepLean/SpaceTime/LorentzVector/NormOne.lean +++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean @@ -184,7 +184,7 @@ lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ Future lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw : w ∈ FuturePointing d) : ⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by - rw [show (0 : ℝ) = - 0 by simp, le_neg] + rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg] have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) hw apply le_of_le_of_eq h1 ?_ simp [neg] @@ -207,7 +207,7 @@ open LorentzVector @[simps!] noncomputable def timeVecNormOneFuture : FuturePointing d := ⟨⟨timeVec, by rw [NormOneLorentzVector.mem_iff, on_timeVec]⟩, by - rw [mem_iff, timeVec_time]; simp⟩ + rw [mem_iff, timeVec_time]; exact Real.zero_lt_one⟩ /-- A continuous path from `timeVecNormOneFuture` to any other. -/ @@ -222,15 +222,12 @@ noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFutur conj_trivial] rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply] simp only [Function.comp_apply, RCLike.inner_apply, conj_trivial] - have h1 : ∑ x : Fin d, t.1 * u.1.1 (Sum.inr x) * (↑t.1 * u.1.1 (Sum.inr x)) = - t ^ 2 * ∑ x : Fin d, u.1.1 (Sum.inr x) * u.1.1 (Sum.inr x) := by - rw [Finset.mul_sum] - apply Finset.sum_congr rfl - intro i _ - ring - rw [h1] + refine Eq.symm (eq_sub_of_add_eq (congrArg (HAdd.hAdd 1) ?_)) + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro i _ ring - refine Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩, + exact Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩, by simp only [space, Function.comp_apply, mem_iff_time_nonneg, time, Real.sqrt_pos] exact Real.sqrt_nonneg _⟩ From c2df4753a67ad1766897dc3d8cb7c97cbeaa9d27 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 2 Jul 2024 10:42:33 -0400 Subject: [PATCH 5/6] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 11228be..88b8923 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ -![HepLean](./doc/HepLeanLogo_white.jpeg) +![HepLean](./docs/HepLeanLogo_white.jpeg) [![](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) From 692479fc05987ef1eee15c724bac6da4d50264cb Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 2 Jul 2024 10:43:02 -0400 Subject: [PATCH 6/6] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 88b8923..e0fbd2c 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ [![](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) -[![](https://img.shields.io/badge/Lean-v4.9.0--rc3-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0-rc1) +[![](https://img.shields.io/badge/Lean-v4.9.0--rc3-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0-rc3) A project to digitalize high energy physics.