Merge pull request #35 from HEPLean/SpaceTime/LorentzGroup

Rotations in Lorentz group

.github/workflows/build.yml

@@ -28,11 +28,12 @@ jobs:
       - name: check ls 
         run: |
           ls -a
+          
       
       - name: build cache
         run: |
           lake exe cache get
-
+ 
       - name: build HepLean
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3

.gitignore

@@ -1,5 +1,4 @@
 /build
 /lake-packages/*
 .lake/packages/*
-.lake/build
-paper
+.lake/build

HepLean.lean

@@ -54,6 +54,7 @@ import HepLean.FlavorPhysics.CKMMatrix.Relations
 import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
+import HepLean.GroupTheory.SO3.Basic
 import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.CliffordAlgebra
 import HepLean.SpaceTime.FourVelocity
@@ -61,6 +62,7 @@ import HepLean.SpaceTime.LorentzGroup.Basic
 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.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.Basic

HepLean/GroupTheory/SO3/Basic.lean

@@ -0,0 +1,234 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.LinearAlgebra.UnitaryGroup
+import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
+import Mathlib.Data.Complex.Exponential
+import Mathlib.Geometry.Manifold.VectorBundle.Basic
+import Mathlib.LinearAlgebra.Eigenspace.Basic
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Analysis.InnerProductSpace.Adjoint
+/-!
+# The group SO(3)
+
+
+-/
+
+namespace GroupTheory
+open Matrix
+
+/-- The group of `3×3` real matrices with determinant 1 and `A * Aᵀ = 1`. -/
+def SO3 : Type := {A : Matrix (Fin 3) (Fin 3) ℝ // A.det = 1 ∧ A * Aᵀ = 1}
+
+@[simps mul_coe one_coe inv div]
+instance SO3Group : Group SO3 where
+  mul A B := ⟨A.1 * B.1,
+    by
+      simp only [det_mul, A.2.1, B.2.1, mul_one],
+    by
+      simp [A.2.2, B.2.2, ← Matrix.mul_assoc, Matrix.mul_assoc]⟩
+  mul_assoc A B C := by
+    apply Subtype.eq
+    exact Matrix.mul_assoc A.1 B.1 C.1
+  one := ⟨1, by simp, by simp⟩
+  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ᵀ, by simp [A.2], by simp [mul_eq_one_comm.mpr A.2.2]⟩
+  mul_left_inv A := by
+    apply Subtype.eq
+    exact mul_eq_one_comm.mpr A.2.2
+
+/-- Notation for the group `SO3`. -/
+scoped[GroupTheory] notation (name := SO3_notation) "SO(3)" => SO3
+
+/-- SO3 has the subtype topology. -/
+instance : TopologicalSpace SO3 := instTopologicalSpaceSubtype
+
+namespace SO3
+
+lemma coe_inv (A : SO3) : (A⁻¹).1 = A.1⁻¹:= by
+  refine (inv_eq_left_inv ?h).symm
+  exact mul_eq_one_comm.mpr A.2.2
+
+/-- The inclusion of `SO(3)` into `GL (Fin 3) ℝ`. -/
+def toGL : SO(3) →* GL (Fin 3) ℝ where
+  toFun A := ⟨A.1, (A⁻¹).1, A.2.2, mul_eq_one_comm.mpr A.2.2⟩
+  map_one' := by
+    simp
+    rfl
+  map_mul' x y  := by
+    simp only [_root_.mul_inv_rev, coe_inv]
+    ext
+    rfl
+
+lemma subtype_val_eq_toGL : (Subtype.val : SO3 → Matrix (Fin 3) (Fin 3) ℝ) =
+    Units.val ∘ toGL.toFun := by
+  ext A
+  rfl
+
+lemma toGL_injective : Function.Injective toGL := by
+  intro A B h
+  apply Subtype.eq
+  rw [@Units.ext_iff] at h
+  simpa using h
+
+/-- The inclusion of `SO(3)` into the monoid of matrices times the opposite of
+  the monoid of matrices. -/
+@[simps!]
+def toProd : SO(3) →* (Matrix (Fin 3) (Fin 3) ℝ) × (Matrix (Fin 3) (Fin 3) ℝ)ᵐᵒᵖ :=
+  MonoidHom.comp (Units.embedProduct _) toGL
+
+lemma toProd_eq_transpose  : toProd A = (A.1, ⟨A.1ᵀ⟩) := by
+  simp only [toProd, Units.embedProduct, coe_units_inv, MulOpposite.op_inv, toGL, coe_inv,
+    MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, Prod.mk.injEq,
+    true_and]
+  refine MulOpposite.unop_inj.mp ?_
+  simp only [MulOpposite.unop_inv, MulOpposite.unop_op]
+  rw [← coe_inv]
+  rfl
+
+lemma toProd_injective : Function.Injective toProd := 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ᵀ⟩))
+  refine continuous_prod_mk.mpr (And.intro ?_ ?_)
+  exact continuous_iff_le_induced.mpr fun U a => a
+  refine Continuous.comp' ?_ ?_
+  exact MulOpposite.continuous_op
+  refine Continuous.matrix_transpose ?_
+  exact continuous_iff_le_induced.mpr fun U a => a
+
+
+/-- The embedding of `SO(3)` into the monoid of matrices times the opposite of
+  the monoid of matrices. -/
+lemma toProd_embedding : Embedding toProd where
+  inj := toProd_injective
+  induced := by
+    refine (inducing_iff ⇑toProd).mp ?_
+    refine inducing_of_inducing_compose toProd_continuous continuous_fst ?hgf
+    exact (inducing_iff (Prod.fst ∘ ⇑toProd)).mpr rfl
+
+/-- The embedding of `SO(3)` into `GL (Fin 3) ℝ`. -/
+lemma toGL_embedding : Embedding toGL.toFun where
+  inj := toGL_injective
+  induced := by
+    refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm
+    intro s
+    rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s ]
+    rw [isOpen_induced_iff, isOpen_induced_iff]
+    apply Iff.intro ?_ ?_
+    · intro h
+      obtain ⟨U, hU1, hU2⟩ := h
+      rw [isOpen_induced_iff] at hU1
+      obtain ⟨V, hV1, hV2⟩ := hU1
+      use V
+      simp [hV1]
+      rw [← hU2, ← hV2]
+      rfl
+    · intro h
+      obtain ⟨U, hU1, hU2⟩ := h
+      let t := (Units.embedProduct _) ⁻¹' U
+      use t
+      apply And.intro (isOpen_induced hU1)
+      exact hU2
+
+instance : TopologicalGroup SO(3) :=
+  Inducing.topologicalGroup toGL toGL_embedding.toInducing
+
+lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by
+  have h1 : det (A.1 - 1) = - det (A.1 - 1)  :=
+    calc
+      det (A.1 - 1) = det (A.1 - A.1 *  A.1ᵀ)  := by simp [A.2.2]
+      _ = det A.1 * det (1 -  A.1ᵀ) :=  by rw [← det_mul, mul_sub, mul_one]
+      _ = det (1 - A.1ᵀ):= by simp [A.2.1]
+      _ = det (1 - A.1ᵀ)ᵀ := by rw [det_transpose]
+      _ = det (1 - A.1) := by simp
+      _ = det (- (A.1 - 1)) := by simp
+      _ = (- 1) ^ 3  * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
+      _ = -  det (A.1 - 1)  := by simp [pow_three]
+  simpa using h1
+
+@[simp]
+lemma det_id_minus (A : SO(3)) : det (1 - A.1) = 0 := by
+  have h1 : det (1 - A.1) = - det (A.1 - 1) := by
+    calc
+      det (1 - A.1) = det (- (A.1 - 1)) := by simp
+      _ = (- 1) ^ 3  *  det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
+      _ = -  det (A.1 - 1) := by simp [pow_three]
+  rw [h1, det_minus_id]
+  simp only [neg_zero]
+
+@[simp]
+lemma one_in_spectrum (A : SO(3)) : 1 ∈ spectrum ℝ (A.1) := by
+  rw [spectrum.mem_iff]
+  simp only [_root_.map_one]
+  rw [Matrix.isUnit_iff_isUnit_det]
+  simp
+
+noncomputable section action
+open Module
+
+/-- The endomorphism of `EuclideanSpace ℝ (Fin 3)` associated to a element of `SO(3)`. -/
+@[simps!]
+def toEnd (A : SO(3)) : End ℝ (EuclideanSpace ℝ (Fin 3)) :=
+  Matrix.toLin (EuclideanSpace.basisFun (Fin 3) ℝ).toBasis
+  (EuclideanSpace.basisFun (Fin 3) ℝ).toBasis A.1
+
+lemma one_is_eigenvalue (A : SO(3)) : A.toEnd.HasEigenvalue 1 := by
+  rw [End.hasEigenvalue_iff_mem_spectrum]
+  erw [AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv (EuclideanSpace.basisFun (Fin 3) ℝ).toBasis ) A.1]
+  exact one_in_spectrum A
+
+lemma exists_stationary_vec (A : SO(3)) :
+    ∃ (v : EuclideanSpace ℝ (Fin 3)),
+    Orthonormal ℝ (({0} : Set (Fin 3)).restrict (fun _ => v ))
+    ∧ A.toEnd v = v := by
+  obtain ⟨v, hv⟩ := End.HasEigenvalue.exists_hasEigenvector $ one_is_eigenvalue A
+  have hvn : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv.2
+  use (1/‖v‖) • v
+  apply And.intro
+  rw [@orthonormal_iff_ite]
+  intro v1 v2
+  have hv1 := v1.2
+  have hv2 := v2.2
+  simp_all only [one_div, Set.mem_singleton_iff]
+  have hveq : v1 = v2 := by
+    rw [@Subtype.ext_iff]
+    simp_all only
+  subst hveq
+  simp only [Set.restrict_apply, PiLp.smul_apply, smul_eq_mul,
+    _root_.map_mul, map_inv₀, conj_trivial, ↓reduceIte]
+  rw [inner_smul_right, inner_smul_left, real_inner_self_eq_norm_sq v]
+  field_simp
+  ring
+  rw [_root_.map_smul, End.mem_eigenspace_iff.mp hv.1 ]
+  simp
+
+lemma exists_basis_preserved (A : SO(3)) :
+    ∃ (b : OrthonormalBasis (Fin 3) ℝ (EuclideanSpace ℝ (Fin 3))), A.toEnd (b 0) = b 0 := by
+  obtain ⟨v, hv⟩ := exists_stationary_vec A
+  have h3 : FiniteDimensional.finrank ℝ (EuclideanSpace ℝ (Fin 3)) = Fintype.card (Fin 3) := by
+    simp_all only [toEnd_apply, finrank_euclideanSpace, Fintype.card_fin]
+  obtain ⟨b, hb⟩ :=  Orthonormal.exists_orthonormalBasis_extension_of_card_eq h3 hv.1
+  simp at hb
+  use b
+  rw [hb, hv.2]
+
+
+
+end action
+end SO3
+
+
+end GroupTheory

HepLean/SpaceTime/LorentzGroup/Basic.lean

@@ -90,62 +90,138 @@ lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by
 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
+  simp
+
+lemma η : PreservesηLin η := by
+  simp [iff_matrix, η_transpose, η_sq]
+
 end PreservesηLin
 
-/-- The Lorentz group as a subgroup of the general linear group over the reals. -/
-def lorentzGroup : Subgroup (GL (Fin 4) ℝ) where
-  carrier := {Λ | PreservesηLin Λ}
-  mul_mem' {a b} := by
-    intros ha hb x y
-    simp only [Units.val_mul, mulVec_mulVec]
-    rw [← mulVec_mulVec, ← mulVec_mulVec, ha, hb]
-  one_mem' := by
-    intros x y
-    simp
-  inv_mem' {a} := by
-    intros ha x y
-    simp only [coe_units_inv, ← ha ((a.1⁻¹) *ᵥ x) ((a.1⁻¹) *ᵥ y), mulVec_mulVec]
-    have hx : (a.1 * (a.1)⁻¹) = 1 := by
-      simp only [@Units.mul_eq_one_iff_inv_eq, coe_units_inv]
-    simp [hx]
+/-- The Lorentz group is the subset of matrices which preserve ηLin. -/
+def lorentzGroup : Type := {Λ : Matrix (Fin 4) (Fin 4) ℝ // PreservesηLin Λ}
 
-/-- The Lorentz group is a topological group with the subset topology. -/
-instance : TopologicalGroup lorentzGroup :=
-  Subgroup.instTopologicalGroupSubtypeMem lorentzGroup
+@[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⟩
+  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_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.η⟩
+  mul_left_inv A := by
+    apply Subtype.eq
+    exact (PreservesηLin.iff_matrix A.1).mp A.2
 
-/-- The lift of a matrix preserving `ηLin` to a Lorentz Group element. -/
-def PreservesηLin.liftLor {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) :
-    lorentzGroup := ⟨liftGL h, h⟩
+/-- Notation for the Lorentz group. -/
+scoped[spaceTime] notation (name := lorentzGroup_notation) "𝓛" => lorentzGroup
+
+
+/-- `lorentzGroup` has the subtype topology. -/
+instance : TopologicalSpace lorentzGroup := instTopologicalSpaceSubtype
 
 namespace lorentzGroup
 
-lemma mem_iff (Λ : GL (Fin 4) ℝ): Λ ∈ lorentzGroup ↔ PreservesηLin Λ := by
-  rfl
+lemma coe_inv (A : 𝓛) : (A⁻¹).1 = A.1⁻¹:= by
+  refine (inv_eq_left_inv ?h).symm
+  exact (PreservesηLin.iff_matrix A.1).mp A.2
+
+/-- The homomorphism of the Lorentz group into `GL (Fin 4) ℝ`. -/
+def toGL : 𝓛 →* 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⟩
+  map_one' := by
+    simp
+    rfl
+  map_mul' x y  := by
+    simp only [lorentzGroupIsGroup, _root_.mul_inv_rev, coe_inv]
+    ext
+    rfl
+
+lemma toGL_injective : Function.Injective toGL := by
+  intro A B h
+  apply Subtype.eq
+  rw [@Units.ext_iff] at h
+  simpa using h
+
+/-- The homomorphism from the Lorentz Group into the monoid of matrices times the opposite of
+  the monoid of matrices. -/
+@[simps!]
+def toProd : 𝓛 →* (Matrix (Fin 4) (Fin 4) ℝ) × (Matrix (Fin 4) (Fin 4) ℝ)ᵐᵒᵖ :=
+  MonoidHom.comp (Units.embedProduct _) toGL
+
+lemma toProd_eq_transpose_η  : toProd A = (A.1, ⟨η * A.1ᵀ * η⟩) := rfl
+
+lemma toProd_injective : Function.Injective toProd := 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ᵀ * η⟩))
+  refine continuous_prod_mk.mpr (And.intro ?_ ?_)
+  exact continuous_iff_le_induced.mpr fun U a => a
+  refine Continuous.comp' ?_ ?_
+  exact MulOpposite.continuous_op
+  refine Continuous.matrix_mul (Continuous.matrix_mul continuous_const ?_) continuous_const
+  refine Continuous.matrix_transpose ?_
+  exact continuous_iff_le_induced.mpr fun U a => a
+
+/-- 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
+  inj := toProd_injective
+  induced := by
+    refine (inducing_iff ⇑toProd).mp ?_
+    refine inducing_of_inducing_compose toProd_continuous continuous_fst ?hgf
+    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
+  inj := toGL_injective
+  induced := by
+    refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm
+    intro s
+    rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s ]
+    rw [isOpen_induced_iff, isOpen_induced_iff]
+    apply Iff.intro ?_ ?_
+    · intro h
+      obtain ⟨U, hU1, hU2⟩ := h
+      rw [isOpen_induced_iff] at hU1
+      obtain ⟨V, hV1, hV2⟩ := hU1
+      use V
+      simp [hV1]
+      rw [← hU2, ← hV2]
+      rfl
+    · intro h
+      obtain ⟨U, hU1, hU2⟩ := h
+      let t := (Units.embedProduct _) ⁻¹' U
+      use t
+      apply And.intro (isOpen_induced hU1)
+      exact hU2
+
+instance : TopologicalGroup 𝓛 := Inducing.topologicalGroup toGL toGL_embedding.toInducing
 
 /-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
-def transpose (Λ : lorentzGroup) : lorentzGroup :=
-  PreservesηLin.liftLor ((PreservesηLin.iff_transpose Λ.1).mp Λ.2)
+def transpose (Λ : lorentzGroup) : lorentzGroup := ⟨Λ.1ᵀ, (PreservesηLin.iff_transpose Λ.1).mp Λ.2⟩
 
 
-/-- The continuous map from `GL (Fin 4) ℝ` to `Matrix (Fin 4) (Fin 4) ℝ` whose kernel is
-the Lorentz group. -/
-def kernelMap : C(GL (Fin 4) ℝ, Matrix (Fin 4) (Fin 4) ℝ) where
-  toFun Λ := η * Λ.1ᵀ * η * Λ.1
-  continuous_toFun := by
-    apply Continuous.mul _ Units.continuous_val
-    apply Continuous.mul _ continuous_const
-    exact Continuous.mul continuous_const (Continuous.matrix_transpose (Units.continuous_val))
-
-lemma kernelMap_kernel_eq_lorentzGroup : lorentzGroup = kernelMap ⁻¹' {1} := by
-  ext Λ
-  erw [mem_iff Λ, PreservesηLin.iff_matrix]
-  rfl
-
-/-- The Lorentz Group is a closed subset of `GL (Fin 4) ℝ`. -/
-theorem isClosed_of_GL4 : IsClosed (lorentzGroup : Set (GL (Fin 4) ℝ)) := by
-  rw [kernelMap_kernel_eq_lorentzGroup]
-  exact continuous_iff_isClosed.mp kernelMap.2 {1} isClosed_singleton
-
 end lorentzGroup
 
+
 end spaceTime

HepLean/SpaceTime/LorentzGroup/Boosts.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzGroup.Orthochronous
+import HepLean.SpaceTime.LorentzGroup.Proper
 import Mathlib.GroupTheory.SpecificGroups.KleinFour
 import Mathlib.Topology.Constructions
 /-!
@@ -140,16 +141,12 @@ lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u
 
 /-- A generalised boost as an element of the Lorentz Group. -/
 def toLorentz (u v : FourVelocity) : lorentzGroup :=
-  PreservesηLin.liftLor (toMatrix_PreservesηLin u v)
+  ⟨toMatrix u v, toMatrix_PreservesηLin u v⟩
 
 lemma toLorentz_continuous (u : FourVelocity) : Continuous (toLorentz u) := by
-  refine Continuous.subtype_mk ?_ fun x => (PreservesηLin.liftLor (toMatrix_PreservesηLin u x)).2
-  refine Units.continuous_iff.mpr (And.intro ?_ ?_)
+  refine Continuous.subtype_mk ?_ (fun x => toMatrix_PreservesηLin u x)
   exact toMatrix_continuous u
-  change Continuous fun x => (η * (toMatrix u x).transpose * η)
-  refine Continuous.matrix_mul ?_ continuous_const
-  refine Continuous.matrix_mul continuous_const ?_
-  exact Continuous.matrix_transpose (toMatrix_continuous u)
+
 
 
 lemma toLorentz_joined_to_1 (u v : FourVelocity) : Joined 1 (toLorentz u v) := by
@@ -157,11 +154,16 @@ lemma toLorentz_joined_to_1 (u v : FourVelocity) : Joined 1 (toLorentz u v) := b
   use ContinuousMap.comp ⟨toLorentz u, toLorentz_continuous u⟩ f
   · simp only [ContinuousMap.toFun_eq_coe, ContinuousMap.comp_apply, ContinuousMap.coe_coe,
     Path.source, ContinuousMap.coe_mk]
-    rw [@Subtype.ext_iff, toLorentz, PreservesηLin.liftLor]
-    refine Units.val_eq_one.mp ?_
+    rw [@Subtype.ext_iff, toLorentz]
     simp [PreservesηLin.liftGL, toMatrix, self u]
   · simp
 
+lemma toLorentz_in_connected_component_1 (u v : FourVelocity) :
+    toLorentz u v ∈ connectedComponent 1 :=
+  pathComponent_subset_component _ (toLorentz_joined_to_1 u v)
+
+lemma isProper (u v : FourVelocity) : IsProper (toLorentz u v) :=
+  (isProper_on_connected_component (toLorentz_in_connected_component_1 u v)).mp id_IsProper
 
 end genBoost
 

HepLean/SpaceTime/LorentzGroup/Orthochronous.lean

@@ -36,7 +36,7 @@ open PreFourVelocity
 def fstCol (Λ : lorentzGroup) : PreFourVelocity := ⟨Λ.1 *ᵥ stdBasis 0, by
   rw [mem_PreFourVelocity_iff, ηLin_expand]
   simp only [Fin.isValue, stdBasis_mulVec]
-  have h00 := congrFun (congrFun ((PreservesηLin.iff_matrix Λ.1).mp ((mem_iff Λ.1).mp Λ.2)) 0) 0
+  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
@@ -51,7 +51,7 @@ def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0
 
 lemma IsOrthochronous_iff_transpose (Λ : lorentzGroup) :
     IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by
-  simp only [IsOrthochronous, Fin.isValue, transpose, PreservesηLin.liftLor, PreservesηLin.liftGL,
+  simp only [IsOrthochronous, Fin.isValue, transpose, PreservesηLin.liftGL,
     transpose_transpose, transpose_apply]
 
 lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) :
@@ -62,7 +62,7 @@ lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) :
 /-- The continuous map taking a Lorentz transformation to its `0 0` element. -/
 def mapZeroZeroComp : C(lorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0, by
   refine Continuous.matrix_elem ?_ 0 0
-  refine Continuous.comp' Units.continuous_val continuous_subtype_val⟩
+  refine Continuous.comp' (continuous_iff_le_induced.mpr fun U a => a) continuous_id'⟩
 
 /-- An auxillary function used in the definition of `orthchroMapReal`. -/
 def stepFunction : ℝ → ℝ := fun t =>
@@ -112,7 +112,7 @@ lemma orthchroMapReal_minus_one_or_one (Λ : lorentzGroup) :
 
 local notation  "ℤ₂" => Multiplicative (ZMod 2)
 
-/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
+/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
 def orthchroMap : C(lorentzGroup, ℤ₂) :=
   ContinuousMap.comp coeForℤ₂ {
     toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
@@ -130,9 +130,10 @@ lemma orthchroMap_not_IsOrthochronous {Λ : lorentzGroup} (h : ¬ IsOrthochronou
 lemma zero_zero_mul (Λ Λ' : lorentzGroup) :
     (Λ * Λ').1 0 0 =  (fstCol (transpose Λ)).1 0 * (fstCol Λ').1 0 +
     ⟪(fstCol (transpose Λ)).1.space, (fstCol Λ').1.space⟫_ℝ := by
-  rw [@Subgroup.coe_mul, @GeneralLinearGroup.coe_mul, mul_apply, Fin.sum_univ_four]
-  rw [@PiLp.inner_apply, Fin.sum_univ_three]
-  simp [transpose, stdBasis_mulVec, PreservesηLin.liftLor, PreservesηLin.liftGL]
+  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 Λ)
@@ -169,7 +170,7 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬
   rw [zero_zero_mul]
   exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h'
 
-/-- The representation from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
+/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
 def orthchroRep : lorentzGroup →* ℤ₂ where
   toFun := orthchroMap
   map_one' := by

HepLean/SpaceTime/LorentzGroup/Proper.lean

@@ -25,9 +25,9 @@ open ComplexConjugate
 namespace lorentzGroup
 
 /-- The determinant of a member of the lorentz group is `1` or `-1`. -/
-lemma det_eq_one_or_neg_one (Λ : lorentzGroup) : Λ.1.1.det = 1 ∨ Λ.1.1.det = -1 := by
+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 ((mem_iff Λ.1).mp Λ.2)))
+    (congrArg det ((PreservesηLin.iff_matrix' Λ.1).mp Λ.2))
 
 local notation  "ℤ₂" => Multiplicative (ZMod 2)
 
@@ -47,16 +47,17 @@ def coeForℤ₂ :  C(({-1, 1} : Set ℝ), ℤ₂) where
     exact continuous_of_discreteTopology
 
 /-- The continuous map taking a lorentz matrix to its determinant. -/
-def detContinuous :  C(lorentzGroup, ℤ₂) :=
+def detContinuous :  C(𝓛, ℤ₂) :=
   ContinuousMap.comp  coeForℤ₂ {
-    toFun := fun Λ => ⟨Λ.1.1.det, Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩,
+    toFun := fun Λ => ⟨Λ.1.det, Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩,
     continuous_toFun := by
       refine Continuous.subtype_mk ?_ _
-      exact Continuous.matrix_det $
-        Continuous.comp' Units.continuous_val continuous_subtype_val}
+      apply Continuous.matrix_det $
+        Continuous.comp' (continuous_iff_le_induced.mpr fun U a => a) continuous_id'
+      }
 
 lemma detContinuous_eq_iff_det_eq (Λ Λ' : lorentzGroup) :
-    detContinuous Λ = detContinuous Λ' ↔ Λ.1.1.det = Λ'.1.1.det := by
+    detContinuous Λ = detContinuous Λ' ↔ Λ.1.det = Λ'.1.det := by
   apply Iff.intro
   intro h
   simp [detContinuous] at h
@@ -76,10 +77,10 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : lorentzGroup) :
 
 /-- The representation taking a lorentz matrix to its determinant. -/
 @[simps!]
-def detRep : lorentzGroup →* ℤ₂ where
+def detRep : 𝓛 →* ℤ₂ where
   toFun Λ := detContinuous Λ
   map_one' := by
-    simp [detContinuous]
+    simp [detContinuous, lorentzGroupIsGroup]
   map_mul' := by
     intro Λ1 Λ2
     simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero,
@@ -92,7 +93,7 @@ def detRep : lorentzGroup →* ℤ₂ where
 lemma detRep_continuous : Continuous detRep := detContinuous.2
 
 lemma det_on_connected_component {Λ Λ'  : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) :
-    Λ.1.1.det = Λ'.1.1.det := by
+    Λ.1.det = Λ'.1.det := by
   obtain ⟨s, hs, hΛ'⟩ := h
   let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s detContinuous
   haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1
@@ -100,12 +101,17 @@ 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 det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.1.det = Λ'.1.1.det :=
+lemma detRep_on_connected_component {Λ Λ'  : lorentzGroup} (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 :=
   det_on_connected_component $ pathComponent_subset_component _ h
 
 /-- A Lorentz Matrix is proper if its determinant is 1. -/
 @[simp]
-def IsProper (Λ : lorentzGroup) : Prop := Λ.1.1.det = 1
+def IsProper (Λ : lorentzGroup) : Prop := Λ.1.det = 1
 
 instance : DecidablePred IsProper := by
   intro Λ
@@ -114,8 +120,15 @@ instance : DecidablePred IsProper := by
 lemma IsProper_iff (Λ : lorentzGroup) : IsProper Λ ↔ detRep Λ = 1 := by
   rw [show 1 = detRep 1 by simp]
   rw [detRep_apply, detRep_apply, detContinuous_eq_iff_det_eq]
-  simp only [IsProper, OneMemClass.coe_one, Units.val_one, det_one]
+  simp only [IsProper, lorentzGroupIsGroup_one_coe, det_one]
 
+lemma id_IsProper : IsProper 1 := by
+  simp [IsProper]
+
+lemma isProper_on_connected_component {Λ Λ'  : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) :
+    IsProper Λ ↔ IsProper Λ' := by
+  simp [detRep_apply, detRep_apply, detContinuous]
+  rw [det_on_connected_component h]
 
 end lorentzGroup
 

HepLean/SpaceTime/LorentzGroup/Rotations.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzGroup.Orthochronous
+import HepLean.SpaceTime.LorentzGroup.Proper
+import HepLean.GroupTheory.SO3.Basic
+import Mathlib.GroupTheory.SpecificGroups.KleinFour
+import Mathlib.Topology.Constructions
+/-!
+# Rotations
+
+-/
+noncomputable section
+namespace spaceTime
+
+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)
+
+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,
+    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]
+
+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
+  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⟩
+  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 spaceTime
+end

HepLean/SpaceTime/Metric.lean

@@ -66,6 +66,24 @@ lemma η_sq : η * η = 1 := by
       Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
       vecHead, vecTail, Function.comp_apply]
 
+lemma η_block : η = Matrix.reindex finSumFinEquiv finSumFinEquiv (
+    Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin 3) (Fin 3) ℝ)) := by
+  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, η, Fin.zero_eta, Matrix.cons_val',
+      Matrix.cons_val_fin_one, Matrix.cons_val_one,
+      Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
+      Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
+      vecHead, vecTail, Function.comp_apply]
+  any_goals rfl
+  all_goals split
+  all_goals simp
+  all_goals rfl
+
+
 
 lemma η_diag_mul_self (μ : Fin 4) : η μ μ * η μ μ  = 1 := by
   fin_cases μ

HepLean/StandardModel/Basic.lean

@@ -32,7 +32,6 @@ open Matrix
 open Complex
 open ComplexConjugate
 
-
 /-- The global gauge group of the standard model. TODO: Generalize to quotient. -/
 abbrev gaugeGroup : Type :=
   specialUnitaryGroup (Fin 3) ℂ × specialUnitaryGroup (Fin 2) ℂ × unitary ℂ

README.md

@@ -57,4 +57,33 @@ The installation instructions for Lean 4 are given here: https://leanprover-comm
 - Run `lake exe cache get`. The command `lake` should have been installed when you installed Lean.
 - Run `lake build`.
 - Open the directory (not a single file) in Visual Studio Code (or another Lean compatible code editor).
-  
+
+### Adding Lean Copilot (optional)
+
+[Lean Copilot](https://github.com/lean-dojo/LeanCopilot) allows the use of large language models in Lean. Using Lean Copilot with HepLean can be done in the following way:
+
+Either: 
+
+- Run the script `./scripts/add-copilot.sh` 
+
+Or: 
+
+- Copy the file `./scripts/copilot_lakefile.txt` over to `lakefile.lean`,
+- Run `lake update LeanCopilot`,
+- Run `lake exe LeanCopilot/download`,
+- Run `lake build`.
+
+To use LeanCopilot add `import LeanCopilot` to the top of the lean file you are working in. 
+The following commands should then become available to you:
+- `suggest_tactics`,
+- `search_proofs`,
+- `select_premises`.
+
+Adding Lean Copilot will modify a number of files. If you have added Lean Copilot, please do not push changes to the following files:
+
+- `lakefile.lean`,
+- `.lake/lakefile.olean`,
+- `.lake/lakefile.olean.trace`,
+- `lake-manifest.json`.
+
+Please also ensure that there are not any `import LeanCopilot` statements in the lean files.

scripts/add-copilot.sh

@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+
+
+cp ./scripts/copilot_lakefile.txt lakefile.lean
+
+lake update LeanCopilot 
+
+lake exe LeanCopilot/download
+
+lake build 
+
+echo ".........................................................................."
+echo "Please do not push changes to the following files: 
+     - lakefile.lean
+     - .lake/lakefile.olean
+     - .lake/lakefile.olean.trace
+     - lake-manifest.json
+Please ensure that there are no 'import LeanCopilot' statements in the lean files."

scripts/copilot_lakefile.txt

@@ -0,0 +1,23 @@
+import Lake
+open Lake DSL
+
+package «hep_lean» {
+  -- add any package configuration options here
+}
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+
+@[default_target]
+lean_lib «HepLean» {
+  -- add any library configuration options here
+  moreLinkArgs := #[
+    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
+    "-lctranslate2"
+  ]
+}
+
+meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+
+require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.2.1"