Merge pull request #70 from HEPLean/Tensors

refactor: Lorentz group
2024-07-02 11:07:26 -04:00 · 2024-07-02 11:07:26 -04:00 · 1e5be33ffc
commit 1e5be33ffc
parent 0116994a58 692479fc05
21 changed files with 1307 additions and 1082 deletions
--- 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
--- a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
@ -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
--- 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 _ _ _

--- a/HepLean/SpaceTime/FourVelocity.lean
+++ b/HepLean/SpaceTime/FourVelocity.lean
@ -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
--- a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
@ -3,8 +3,7 @@ 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.Metric
+import HepLean.SpaceTime.MinkowskiMetric
 import Mathlib.Algebra.Lie.Classical
 /-!
 # The Lorentz Algebra
@ -12,7 +11,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 +22,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 +97,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
--- 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
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@ -3,8 +3,8 @@ 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.AsSelfAdjointMatrix
+import HepLean.SpaceTime.MinkowskiMetric
+import HepLean.SpaceTime.LorentzVector.NormOne
 /-!
 # The Lorentz Group

@ -23,157 +23,144 @@ identity.

 -/

-
 noncomputable section

-namespace SpaceTime
-
-open Manifold
 open Matrix
 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}
+
+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 +173,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 +184,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 +193,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 +218,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 +226,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
@ -247,12 +235,44 @@ lemma toGL_embedding : Embedding toGL.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

-instance : TopologicalGroup LorentzGroup := 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
--- 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,23 +48,27 @@ 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

 /-- 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
@ -71,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]
@ -88,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
@ -174,5 +184,4 @@ end genBoost
 end LorentzGroup


-end SpaceTime
 end
--- 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,45 +20,56 @@ matrices.

 noncomputable section

-namespace SpaceTime

-open Manifold
 open Matrix
 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 +89,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 +114,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 +179,4 @@ def orthchroRep : LorentzGroup →* ℤ₂ where

 end LorentzGroup

-end SpaceTime
 end
--- a/HepLean/SpaceTime/LorentzGroup/Proper.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean
@ -14,19 +14,23 @@ We define the give a series of lemmas related to the determinant of the lorentz

 noncomputable section

-namespace SpaceTime

-open Manifold
 open Matrix
 open Complex
 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 +51,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 +60,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 +79,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 +92,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 +103,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
--- 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
--- a/HepLean/SpaceTime/LorentzTensors/Basic.lean
+++ 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]).
+
+-/
--- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
+++ 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
--- a/HepLean/SpaceTime/LorentzVector/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Basic.lean
@ -0,0 +1,113 @@
+/-
+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.Analysis.InnerProductSpace.PiL2
+/-!
+
+# 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
+
+/-- The structure of a topological space `LorentzVector d`. -/
+instance : TopologicalSpace (LorentzVector d) :=
+  haveI : NormedAddCommGroup (LorentzVector d) := Pi.normedAddCommGroup
+  UniformSpace.toTopologicalSpace
+
+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` indexed by `Fin 1 ⊕ Fin (d)`. -/
+@[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
+  rw [stdBasis]
+  erw [Pi.basisFun_apply]
+  exact LinearMap.stdBasis_apply' ℝ μ ν
+
+/-- The standard unit time vector. -/
+noncomputable abbrev timeVec : (LorentzVector d) := e (Sum.inl 0)
+
+lemma timeVec_space : (@timeVec d).space = 0 := by
+  funext i
+  simp only [space, Function.comp_apply, stdBasis_apply, Fin.isValue, ↓reduceIte, PiLp.zero_apply]
+
+lemma timeVec_time: (@timeVec d).time = 1 := by
+  simp only [time, Fin.isValue, 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
+    · rfl
+    · simp only [Sum.elim_inr, Pi.neg_apply]
+      apply neg_add
+  map_smul' c x := by
+    funext i
+    rcases i with i | i
+    · rfl
+    · simp [HSMul.hSMul, SMul.smul]
+
+/-- The reflection of space. -/
+@[simp]
+def spaceReflection : LorentzVector d := spaceReflectionLin v
+
+lemma spaceReflection_space : v.spaceReflection.space = - v.space := by
+  rfl
+
+lemma spaceReflection_time : v.spaceReflection.time = v.time := by
+  rfl
+
+end LorentzVector
--- a/HepLean/SpaceTime/LorentzVector/NormOne.lean
+++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean
@ -0,0 +1,296 @@
+/-
+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
+
+/-- The set of Lorentz vectors with norm 1. -/
+@[simp]
+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
+  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
+
+instance : TopologicalSpace (FuturePointing d) := instTopologicalSpaceSubtype
+
+namespace FuturePointing
+
+section
+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 => le_of_lt h) (fun h => ?_)
+  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)
+
+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 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
+
+-/
+
+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 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]
+
+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]; exact Real.zero_lt_one⟩
+
+
+/-- 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]
+      refine Eq.symm (eq_sub_of_add_eq (congrArg (HAdd.hAdd 1) ?_))
+      rw [Finset.mul_sum]
+      apply Finset.sum_congr rfl
+      intro i _
+      ring
+      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 _⟩
+  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
+
+
+end NormOneLorentzVector
--- a/HepLean/SpaceTime/Metric.lean
+++ b/HepLean/SpaceTime/Metric.lean
@ -1,267 +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.
-
-/
-
-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
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@ -0,0 +1,352 @@
+/-
+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
+/-!
+
+# 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 : ℕ}
+
+/-- Notation for `minkowskiMatrix`. -/
+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]
+
+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
+
+
+/-!
+
+# 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)
+
+/-- Notation for `minkowskiMetric`. -/
+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 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
+
+
+/-!
+
+# 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]
+
+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]
+
+lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, Λ *ᵥ e ν⟫ₘ = η μ μ * Λ μ ν  := by
+  simp [basis_left, mulVec, dotProduct, stdBasis_apply]
+
+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
--- 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

@ -64,7 +65,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 +85,29 @@ 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]
--- a/README.md
+++ b/README.md
@ -1,9 +1,9 @@

-![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)
-[![](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.

--- 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}
+}
--- 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"