diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean
index c625e93..fae801a 100644
--- a/HepLean/SpaceTime/Basic.lean
+++ b/HepLean/SpaceTime/Basic.lean
@@ -22,7 +22,6 @@ def SpaceTime : Type := Fin 4 → ℝ
 /-- Give spacetime the structure of an additive commutative monoid. -/
 instance : AddCommMonoid SpaceTime := Pi.addCommMonoid
 
-
 /-- Give spacetime the structure of a module over the reals. -/
 instance : Module ℝ SpaceTime := Pi.module _ _ _
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 9eaa8dc..446a3b9 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -3,8 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.Metric
+import HepLean.SpaceTime.MinkowskiMetric
 import HepLean.SpaceTime.AsSelfAdjointMatrix
+import HepLean.SpaceTime.LorentzVector.NormOne
 /-!
 # The Lorentz Group
 
@@ -26,7 +27,6 @@ identity.
 
 noncomputable section
 
-namespace SpaceTime
 
 open Manifold
 open Matrix
@@ -34,146 +34,139 @@ open Complex
 open ComplexConjugate
 
 /-!
-## Matrices which preserve `ηLin`
+## Matrices which preserves the Minkowski metric
 
 We start studying the properties of matrices which preserve `ηLin`.
 These matrices form the Lorentz group, which we will define in the next section at `lorentzGroup`.
 
 -/
+variable  {d : ℕ}
 
-/-- We say a matrix `Λ` preserves `ηLin` if for all `x` and `y`,
-  `ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y`.  -/
-def PreservesηLin (Λ : Matrix (Fin 4) (Fin 4) ℝ) : Prop :=
-  ∀ (x y : SpaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y
+open minkowskiMetric in
+/-- The Lorentz group is the subset of matrices which preserve the minkowski metric. -/
+def LorentzGroup (d : ℕ) : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :=
+    {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ |
+     ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ}
 
-namespace PreservesηLin
 
-variable  (Λ : Matrix (Fin 4) (Fin 4) ℝ)
+namespace LorentzGroup
+/-- Notation for the Lorentz group. -/
+scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup
 
-lemma iff_norm : PreservesηLin Λ ↔
-    ∀ (x : SpaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ x) = ηLin x x := by
+open minkowskiMetric
+
+variable  {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ}
+
+/-!
+
+# Membership conditions
+
+-/
+
+lemma mem_iff_norm :  Λ ∈ LorentzGroup d ↔
+    ∀ (x : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ x⟫ₘ = ⟪x, x⟫ₘ := by
   refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
   have hp := h (x + y)
   have hn := h (x - y)
   rw [mulVec_add] at hp
   rw [mulVec_sub] at hn
   simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn
-  rw [ηLin_symm (Λ *ᵥ y) (Λ *ᵥ x), ηLin_symm y x] at hp hn
+  rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn
   linear_combination hp / 4 + -1 * hn / 4
 
-lemma iff_det_selfAdjoint : PreservesηLin Λ ↔
-    ∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)),
-    det ((toSelfAdjointMatrix ∘ toLin stdBasis stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1
-    = det x.1 := by
-  rw [iff_norm]
-  apply Iff.intro
-  intro h x
-  have h1 := congrArg ofReal $ h (toSelfAdjointMatrix.symm x)
-  simpa [← det_eq_ηLin] using h1
-  intro h x
-  have h1 := h (toSelfAdjointMatrix x)
-  simpa [det_eq_ηLin] using h1
-
-lemma iff_on_right : PreservesηLin Λ ↔
-    ∀ (x y : SpaceTime), ηLin x ((η * Λᵀ * η * Λ) *ᵥ y) = ηLin x y := by
+lemma mem_iff_on_right : Λ ∈ LorentzGroup d ↔
+    ∀ (x y : LorentzVector d), ⟪x, (dual Λ * Λ) *ᵥ y⟫ₘ = ⟪x, y⟫ₘ := by
   apply Iff.intro
   intro h x y
   have h1 := h x y
-  rw [ηLin_mulVec_left, mulVec_mulVec] at h1
+  rw [← dual_mulVec_right, mulVec_mulVec] at h1
   exact h1
   intro h x y
-  rw [ηLin_mulVec_left, mulVec_mulVec]
+  rw [← dual_mulVec_right, mulVec_mulVec]
   exact h x y
 
-lemma iff_matrix : PreservesηLin Λ ↔ η * Λᵀ * η * Λ = 1  := by
-  rw [iff_on_right, ηLin_matrix_eq_identity_iff (η * Λᵀ * η * Λ)]
-  apply Iff.intro
-  · simp_all  [ηLin, implies_true, iff_true, one_mulVec]
-  · exact fun a x y => Eq.symm (Real.ext_cauchy (congrArg Real.cauchy (a x y)))
+lemma mem_iff_dual_mul_self : Λ ∈ LorentzGroup d ↔ dual Λ * Λ = 1  := by
+  rw [mem_iff_on_right, matrix_eq_id_iff]
+  exact forall_comm
 
-lemma iff_matrix' : PreservesηLin Λ ↔ Λ * (η * Λᵀ * η) = 1  := by
-  rw [iff_matrix]
+lemma mem_iff_self_mul_dual :  Λ ∈ LorentzGroup d ↔ Λ * dual Λ = 1  := by
+  rw [mem_iff_dual_mul_self]
   exact mul_eq_one_comm
 
 
-lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by
+lemma mem_iff_transpose : Λ ∈ LorentzGroup d ↔ Λᵀ ∈ LorentzGroup d := by
   apply Iff.intro
-  intro h
-  have h1 := congrArg transpose ((iff_matrix Λ).mp h)
-  rw [transpose_mul, transpose_mul, transpose_mul, η_transpose,
-    ← mul_assoc, transpose_one] at h1
-  rw [iff_matrix' Λ.transpose, ← h1]
-  noncomm_ring
-  intro h
-  have h1 := congrArg transpose ((iff_matrix Λ.transpose).mp h)
-  rw [transpose_mul, transpose_mul, transpose_mul, η_transpose,
-    ← mul_assoc, transpose_one, transpose_transpose] at h1
-  rw [iff_matrix', ← h1]
+  · intro h
+    have h1 := congrArg transpose ((mem_iff_dual_mul_self).mp h)
+    rw [dual, transpose_mul, transpose_mul, transpose_mul, minkowskiMatrix.eq_transpose,
+      ← mul_assoc, transpose_one] at h1
+    rw [mem_iff_self_mul_dual, ← h1, dual]
+    noncomm_ring
+  · intro h
+    have h1 := congrArg transpose ((mem_iff_dual_mul_self).mp h)
+    rw [dual, transpose_mul, transpose_mul, transpose_mul, minkowskiMatrix.eq_transpose,
+      ← mul_assoc, transpose_one, transpose_transpose] at h1
+    rw [mem_iff_self_mul_dual, ← h1, dual]
+    noncomm_ring
+
+lemma mem_mul (hΛ : Λ ∈ LorentzGroup d) (hΛ' : Λ' ∈ LorentzGroup d) : Λ * Λ' ∈ LorentzGroup d := by
+  rw [mem_iff_dual_mul_self, dual_mul]
+  trans dual Λ' * (dual Λ * Λ) * Λ'
   noncomm_ring
+  rw [(mem_iff_dual_mul_self).mp hΛ]
+  simp [(mem_iff_dual_mul_self).mp hΛ']
 
-/-- The lift of a matrix which preserves `ηLin` to an invertible matrix. -/
-def liftGL {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) : GL (Fin 4) ℝ :=
-  ⟨Λ, η * Λᵀ * η , (iff_matrix' Λ).mp h , (iff_matrix Λ).mp h⟩
-
-lemma mul {Λ Λ' : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) (h' : PreservesηLin Λ') :
-    PreservesηLin (Λ * Λ') := by
-  intro x y
-  rw [← mulVec_mulVec, ← mulVec_mulVec, h, h']
-
-lemma one : PreservesηLin 1 := by
-  intro x y
+lemma one_mem : 1 ∈ LorentzGroup d := by
+  rw [mem_iff_dual_mul_self]
   simp
 
-lemma η : PreservesηLin η := by
-  simp [iff_matrix, η_transpose, η_sq]
+lemma dual_mem (h : Λ ∈ LorentzGroup d) : dual Λ ∈ LorentzGroup d := by
+  rw [mem_iff_dual_mul_self, dual_dual]
+  exact mem_iff_self_mul_dual.mp h
 
-end PreservesηLin
+end LorentzGroup
 
 /-!
-## The Lorentz group
 
-We define the Lorentz group as the set of matrices which preserve `ηLin`.
-We show that the Lorentz group is indeed a group.
+# The Lorentz group as a group
 
 -/
 
-/-- The Lorentz group is the subset of matrices which preserve ηLin. -/
-def LorentzGroup : Type := {Λ : Matrix (Fin 4) (Fin 4) ℝ // PreservesηLin Λ}
-
 @[simps mul_coe one_coe inv div]
-instance lorentzGroupIsGroup : Group LorentzGroup where
-  mul A B := ⟨A.1 * B.1, PreservesηLin.mul A.2 B.2⟩
+instance lorentzGroupIsGroup : Group (LorentzGroup d) where
+  mul A B := ⟨A.1 * B.1, LorentzGroup.mem_mul A.2 B.2⟩
   mul_assoc A B C := by
     apply Subtype.eq
     exact Matrix.mul_assoc A.1 B.1 C.1
-  one := ⟨1, PreservesηLin.one⟩
+  one := ⟨1, LorentzGroup.one_mem⟩
   one_mul A := by
     apply Subtype.eq
     exact Matrix.one_mul A.1
   mul_one A := by
     apply Subtype.eq
     exact Matrix.mul_one A.1
-  inv A := ⟨η * A.1ᵀ * η , PreservesηLin.mul (PreservesηLin.mul PreservesηLin.η
-    ((PreservesηLin.iff_transpose A.1).mp A.2)) PreservesηLin.η⟩
+  inv A := ⟨minkowskiMetric.dual A.1, LorentzGroup.dual_mem A.2⟩
   mul_left_inv A := by
     apply Subtype.eq
-    exact (PreservesηLin.iff_matrix A.1).mp A.2
+    exact LorentzGroup.mem_iff_dual_mul_self.mp A.2
 
-/-- Notation for the Lorentz group. -/
-scoped[SpaceTime] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup
-
-
-/-- `lorentzGroup` has the subtype topology. -/
-instance : TopologicalSpace LorentzGroup := instTopologicalSpaceSubtype
+/-- `LorentzGroup` has the subtype topology. -/
+instance : TopologicalSpace (LorentzGroup d) := instTopologicalSpaceSubtype
 
 namespace LorentzGroup
 
-lemma coe_inv (A : LorentzGroup) : (A⁻¹).1 = A.1⁻¹:= by
+open minkowskiMetric
+
+variable  {Λ Λ' : LorentzGroup d}
+
+@[simp]
+lemma coe_inv  : (Λ⁻¹).1 = Λ.1⁻¹:= by
   refine (inv_eq_left_inv ?h).symm
-  exact (PreservesηLin.iff_matrix A.1).mp A.2
+  exact mem_iff_dual_mul_self.mp Λ.2
 
 /-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
-def transpose (Λ : LorentzGroup) : LorentzGroup := ⟨Λ.1ᵀ, (PreservesηLin.iff_transpose Λ.1).mp Λ.2⟩
+def transpose (Λ : LorentzGroup d) : LorentzGroup d :=
+  ⟨Λ.1ᵀ, mem_iff_transpose.mp Λ.2⟩
 
 /-!
 
@@ -186,9 +179,9 @@ embedding.
 -/
 
 /-- The homomorphism of the Lorentz group into `GL (Fin 4) ℝ`. -/
-def toGL : LorentzGroup →* GL (Fin 4) ℝ where
-  toFun A := ⟨A.1, (A⁻¹).1, mul_eq_one_comm.mpr $ (PreservesηLin.iff_matrix A.1).mp A.2,
-    (PreservesηLin.iff_matrix A.1).mp A.2⟩
+def toGL : LorentzGroup d →* GL (Fin 1 ⊕ Fin d) ℝ where
+  toFun A := ⟨A.1, (A⁻¹).1, mul_eq_one_comm.mpr $ mem_iff_dual_mul_self.mp A.2,
+    mem_iff_dual_mul_self.mp A.2⟩
   map_one' := by
     simp
     rfl
@@ -197,7 +190,7 @@ def toGL : LorentzGroup →* GL (Fin 4) ℝ where
     ext
     rfl
 
-lemma toGL_injective : Function.Injective toGL := by
+lemma toGL_injective : Function.Injective (@toGL d) := by
   intro A B h
   apply Subtype.eq
   rw [@Units.ext_iff] at h
@@ -206,20 +199,21 @@ lemma toGL_injective : Function.Injective toGL := by
 /-- The homomorphism from the Lorentz Group into the monoid of matrices times the opposite of
   the monoid of matrices. -/
 @[simps!]
-def toProd : LorentzGroup →* (Matrix (Fin 4) (Fin 4) ℝ) × (Matrix (Fin 4) (Fin 4) ℝ)ᵐᵒᵖ :=
+def toProd : LorentzGroup d →* (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) ×
+    (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)ᵐᵒᵖ :=
   MonoidHom.comp (Units.embedProduct _) toGL
 
-lemma toProd_eq_transpose_η  : toProd A = (A.1, ⟨η * A.1ᵀ * η⟩) := rfl
+lemma toProd_eq_transpose_η  : toProd Λ = (Λ.1, MulOpposite.op $ minkowskiMetric.dual Λ.1) := rfl
 
-lemma toProd_injective : Function.Injective toProd := by
+lemma toProd_injective : Function.Injective (@toProd d) := by
   intro A B h
   rw [toProd_eq_transpose_η, toProd_eq_transpose_η] at h
   rw [@Prod.mk.inj_iff] at h
   apply Subtype.eq
   exact h.1
 
-lemma toProd_continuous : Continuous toProd := by
-  change Continuous (fun A => (A.1, ⟨η * A.1ᵀ * η⟩))
+lemma toProd_continuous : Continuous (@toProd d) := by
+  change Continuous (fun A => (A.1, ⟨dual A.1⟩))
   refine continuous_prod_mk.mpr (And.intro ?_ ?_)
   exact continuous_iff_le_induced.mpr fun U a => a
   refine Continuous.comp' ?_ ?_
@@ -230,7 +224,7 @@ lemma toProd_continuous : Continuous toProd := by
 
 /-- The embedding from the Lorentz Group into the monoid of matrices times the opposite of
   the monoid of matrices. -/
-lemma toProd_embedding : Embedding toProd where
+lemma toProd_embedding : Embedding (@toProd d) where
   inj := toProd_injective
   induced := by
     refine (inducing_iff ⇑toProd).mp ?_
@@ -238,7 +232,7 @@ lemma toProd_embedding : Embedding toProd where
     exact (inducing_iff (Prod.fst ∘ ⇑toProd)).mpr rfl
 
 /-- The embedding from the Lorentz Group into `GL (Fin 4) ℝ`. -/
-lemma toGL_embedding : Embedding toGL.toFun where
+lemma toGL_embedding : Embedding (@toGL d).toFun where
   inj := toGL_injective
   induced := by
     refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm
@@ -248,11 +242,48 @@ lemma toGL_embedding : Embedding toGL.toFun where
     exact exists_exists_and_eq_and
 
 
-instance : TopologicalGroup LorentzGroup := Inducing.topologicalGroup toGL toGL_embedding.toInducing
+instance : TopologicalGroup (LorentzGroup d) :=
+Inducing.topologicalGroup toGL toGL_embedding.toInducing
+
+section
+open LorentzVector
+/-!
+
+# To a norm one Lorentz vector
+
+-/
+
+/-- The first column of a lorentz matrix as a `NormOneLorentzVector`. -/
+@[simps!]
+def toNormOneLorentzVector (Λ : LorentzGroup d) : NormOneLorentzVector d :=
+  ⟨Λ.1 *ᵥ timeVec, by rw [NormOneLorentzVector.mem_iff, Λ.2, minkowskiMetric.on_timeVec]⟩
+
+/-!
+
+# The time like element
+
+-/
+
+/-- The time like element of a Lorentz matrix. -/
+@[simp]
+def timeComp (Λ : LorentzGroup d) : ℝ := Λ.1 (Sum.inl 0) (Sum.inl 0)
+
+lemma timeComp_eq_toNormOneLorentzVector : timeComp Λ = (toNormOneLorentzVector Λ).1.time := by
+  simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue, timeComp]
+  erw [Pi.basisFun_apply, mulVec_stdBasis]
+
+lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') =
+    ⟪toNormOneLorentzVector (transpose Λ), (toNormOneLorentzVector Λ').1.spaceReflection⟫ₘ := by
+  simp only [timeComp, Fin.isValue, lorentzGroupIsGroup_mul_coe, mul_apply, Fintype.sum_sum_type,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, toNormOneLorentzVector,
+    transpose, timeVec, right_spaceReflection, time, space, PiLp.inner_apply, Function.comp_apply,
+    RCLike.inner_apply, conj_trivial]
+  erw [Pi.basisFun_apply, mulVec_stdBasis]
+  simp
 
 
 
+
+
+end
 end LorentzGroup
-
-
-end SpaceTime
diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
index 1d49d9e..a11246a 100644
--- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzGroup.Proper
 import Mathlib.Topology.Constructions
-import HepLean.SpaceTime.FourVelocity
+import HepLean.SpaceTime.LorentzVector.NormOne
 /-!
 # Boosts
 
@@ -28,15 +28,17 @@ A boost is the special case of a generalised boost when `u = stdBasis 0`.
 
 -/
 noncomputable section
-namespace SpaceTime
 
 namespace LorentzGroup
 
-open FourVelocity
+open NormOneLorentzVector
+open minkowskiMetric
+
+variable {d : ℕ}
 
 /-- An auxillary linear map used in the definition of a generalised boost. -/
-def genBoostAux₁ (u v : FourVelocity) : SpaceTime →ₗ[ℝ] SpaceTime where
-  toFun x := (2 * ηLin x u) • v.1.1
+def genBoostAux₁ (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] LorentzVector d where
+  toFun x := (2 * ⟪x, u⟫ₘ) • v.1.1
   map_add' x y := by
     simp only [map_add, LinearMap.add_apply]
     rw [mul_add, add_smul]
@@ -46,17 +48,21 @@ def genBoostAux₁ (u v : FourVelocity) : SpaceTime →ₗ[ℝ] SpaceTime where
     rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul]
 
 /-- An auxillary linear map used in the definition of a genearlised boost. -/
-def genBoostAux₂ (u v : FourVelocity) : SpaceTime →ₗ[ℝ] SpaceTime where
-  toFun x := - (ηLin x (u + v) / (1 + ηLin u v)) • (u + v)
+def genBoostAux₂ (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] LorentzVector d where
+  toFun x := - (⟪x, u.1.1 + v⟫ₘ / (1 + ⟪u.1.1, v⟫ₘ)) • (u.1.1 + v)
   map_add' x y := by
     simp only
-    rw [ηLin.map_add, div_eq_mul_one_div]
-    rw [show (ηLin x + ηLin y) (↑u + ↑v) = ηLin x (u+v) + ηLin y (u+v) from rfl]
-    rw [add_mul, neg_add, add_smul, ← div_eq_mul_one_div, ← div_eq_mul_one_div]
+    rw [← add_smul]
+    apply congrFun
+    apply congrArg
+    field_simp
+    apply congrFun
+    apply congrArg
+    ring
   map_smul' c x := by
     simp only
-    rw [ηLin.map_smul]
-    rw [show (c • ηLin x) (↑u + ↑v) = c * ηLin x (u+v) from rfl]
+    rw [map_smul]
+    rw [show (c • minkowskiMetric x) (↑u + ↑v) = c * minkowskiMetric x (u+v) from rfl]
     rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul]
     rfl
 
@@ -174,5 +180,4 @@ end genBoost
 end LorentzGroup
 
 
-end SpaceTime
 end
diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
index 3f26bc2..7719ec4 100644
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.FourVelocity
+import HepLean.SpaceTime.LorentzVector.NormOne
 import HepLean.SpaceTime.LorentzGroup.Proper
 /-!
 # The Orthochronous Lorentz Group
@@ -20,7 +20,6 @@ matrices.
 
 noncomputable section
 
-namespace SpaceTime
 
 open Manifold
 open Matrix
@@ -28,37 +27,50 @@ open Complex
 open ComplexConjugate
 
 namespace LorentzGroup
-open PreFourVelocity
 
-/-- The first column of a lorentz matrix as a `PreFourVelocity`. -/
-@[simp]
-def fstCol (Λ : LorentzGroup) : PreFourVelocity := ⟨Λ.1 *ᵥ stdBasis 0, by
-  rw [mem_PreFourVelocity_iff, ηLin_expand]
-  simp only [Fin.isValue, stdBasis_mulVec]
-  have h00 := congrFun (congrFun ((PreservesηLin.iff_matrix Λ.1).mp  Λ.2) 0) 0
-  simp only [Fin.isValue, mul_apply, transpose_apply, Fin.sum_univ_four, ne_eq, zero_ne_one,
-    not_false_eq_true, η_off_diagonal, zero_mul, add_zero, Fin.reduceEq, one_ne_zero, mul_zero,
-    zero_add, one_apply_eq] at h00
-  simp only [η_explicit, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val',
-    cons_val_fin_one, vecCons_const, one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul,
-    cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, cons_val_three,
-     head_fin_const] at h00
-  exact h00⟩
+variable {d : ℕ}
+variable (Λ : LorentzGroup d)
+open LorentzVector
+open minkowskiMetric
 
 /-- A Lorentz transformation is  `orthochronous` if its `0 0` element is non-negative. -/
-def IsOrthochronous (Λ : LorentzGroup) : Prop := 0 ≤ Λ.1 0 0
+def IsOrthochronous : Prop := 0 ≤ timeComp Λ
 
-lemma IsOrthochronous_iff_transpose (Λ : LorentzGroup) :
+lemma IsOrthochronous_iff_futurePointing :
+    IsOrthochronous Λ ↔ (toNormOneLorentzVector Λ) ∈ NormOneLorentzVector.FuturePointing d := by
+  simp only [IsOrthochronous, timeComp_eq_toNormOneLorentzVector]
+  rw [NormOneLorentzVector.FuturePointing.mem_iff_time_nonneg]
+
+lemma IsOrthochronous_iff_transpose :
     IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by rfl
 
-lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : LorentzGroup) :
-    IsOrthochronous Λ ↔ IsFourVelocity (fstCol Λ) := by
-  simp [IsOrthochronous, IsFourVelocity]
-  rw [stdBasis_mulVec]
+lemma IsOrthochronous_iff_ge_one :
+    IsOrthochronous Λ ↔ 1 ≤ timeComp Λ  := by
+  rw [IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.mem_iff,
+    NormOneLorentzVector.time_pos_iff]
+  simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue]
+  erw [Pi.basisFun_apply, mulVec_stdBasis]
+  rfl
+
+lemma not_orthochronous_iff_le_neg_one :
+    ¬ IsOrthochronous Λ ↔ timeComp Λ ≤ -1 := by
+  rw [timeComp, IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.not_mem_iff,
+    NormOneLorentzVector.time_nonpos_iff]
+  simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue]
+  erw [Pi.basisFun_apply, mulVec_stdBasis]
+
+lemma not_orthochronous_iff_le_zero :
+    ¬ IsOrthochronous Λ ↔ timeComp Λ ≤ 0 := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  rw [not_orthochronous_iff_le_neg_one] at h
+  linarith
+  rw [IsOrthochronous_iff_ge_one]
+  linarith
+
 
 /-- The continuous map taking a Lorentz transformation to its `0 0` element. -/
-def mapZeroZeroComp : C(LorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0,
-   Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) 0 0⟩
+def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => timeComp Λ  ,
+   Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩
 
 /-- An auxillary function used in the definition of `orthchroMapReal`. -/
 def stepFunction : ℝ → ℝ := fun t =>
@@ -78,29 +90,23 @@ lemma stepFunction_continuous : Continuous stepFunction := by
 
 /-- The continuous map from `lorentzGroup` to `ℝ` wh
 taking Orthochronous elements to `1` and non-orthochronous to `-1`. -/
-def orthchroMapReal : C(LorentzGroup, ℝ) := ContinuousMap.comp
-  ⟨stepFunction, stepFunction_continuous⟩ mapZeroZeroComp
+def orthchroMapReal : C(LorentzGroup d, ℝ) := ContinuousMap.comp
+  ⟨stepFunction, stepFunction_continuous⟩ timeCompCont
 
-lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup} (h : IsOrthochronous Λ) :
+lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ) :
     orthchroMapReal Λ = 1 := by
-  rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h
-  simp only [IsFourVelocity] at h
-  rw [zero_nonneg_iff] at h
-  simp [stdBasis_mulVec] at h
-  have h1 : ¬  Λ.1 0 0 ≤  (-1 : ℝ) := by linarith
-  change stepFunction (Λ.1 0 0) = 1
-  rw [stepFunction, if_neg h1, if_pos h]
+  rw [IsOrthochronous_iff_ge_one, timeComp] at h
+  change stepFunction (Λ.1 _ _) = 1
+  rw [stepFunction, if_pos h, if_neg]
+  linarith
 
-
-lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup} (h : ¬ IsOrthochronous Λ) :
+lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) :
     orthchroMapReal Λ = - 1 := by
-  rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h
-  rw [not_IsFourVelocity_iff, zero_nonpos_iff] at h
-  simp only [fstCol, Fin.isValue, stdBasis_mulVec] at h
-  change stepFunction (Λ.1 0 0) = - 1
+  rw [not_orthochronous_iff_le_neg_one] at h
+  change stepFunction (timeComp _)= - 1
   rw [stepFunction, if_pos h]
 
-lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup) :
+lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup d) :
     orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 := by
   by_cases h : IsOrthochronous Λ
   apply Or.inr $ orthchroMapReal_on_IsOrthochronous h
@@ -109,65 +115,50 @@ lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup) :
 local notation  "ℤ₂" => Multiplicative (ZMod 2)
 
 /-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
-def orthchroMap : C(LorentzGroup, ℤ₂) :=
+def orthchroMap : C(LorentzGroup d, ℤ₂) :=
   ContinuousMap.comp coeForℤ₂ {
     toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
     continuous_toFun :=  Continuous.subtype_mk (ContinuousMap.continuous orthchroMapReal) _}
 
-lemma orthchroMap_IsOrthochronous {Λ : LorentzGroup} (h : IsOrthochronous Λ) :
+lemma orthchroMap_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ) :
     orthchroMap Λ = 1 := by
   simp [orthchroMap, orthchroMapReal_on_IsOrthochronous h]
 
-lemma orthchroMap_not_IsOrthochronous {Λ : LorentzGroup} (h : ¬ IsOrthochronous Λ) :
+lemma orthchroMap_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) :
     orthchroMap Λ =  Additive.toMul (1 : ZMod 2) := by
   simp [orthchroMap, orthchroMapReal_on_not_IsOrthochronous h]
   rfl
 
-lemma zero_zero_mul (Λ Λ' : LorentzGroup) :
-    (Λ * Λ').1 0 0 =  (fstCol (transpose Λ)).1 0 * (fstCol Λ').1 0 +
-    ⟪(fstCol (transpose Λ)).1.space, (fstCol Λ').1.space⟫_ℝ := by
-  simp only [Fin.isValue, lorentzGroupIsGroup_mul_coe, mul_apply, Fin.sum_univ_four, fstCol,
-    transpose, stdBasis_mulVec, transpose_apply, space, PiLp.inner_apply, Nat.succ_eq_add_one,
-    Nat.reduceAdd, RCLike.inner_apply, conj_trivial, Fin.sum_univ_three, cons_val_zero,
-    cons_val_one, head_cons, cons_val_two, tail_cons]
-  ring
-
-lemma mul_othchron_of_othchron_othchron {Λ Λ' : LorentzGroup} (h : IsOrthochronous Λ)
+lemma mul_othchron_of_othchron_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ)
     (h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
   rw [IsOrthochronous_iff_transpose] at h
-  rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h'
-  rw [IsOrthochronous, zero_zero_mul]
-  exact euclid_norm_IsFourVelocity_IsFourVelocity h h'
+  rw [IsOrthochronous_iff_futurePointing] at h h'
+  rw [IsOrthochronous, timeComp_mul]
+  exact NormOneLorentzVector.FuturePointing.metric_reflect_mem_mem h h'
 
-lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup} (h : ¬  IsOrthochronous Λ)
+lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : ¬ IsOrthochronous Λ)
     (h' : ¬ IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
   rw [IsOrthochronous_iff_transpose] at h
-  rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h'
-  rw [IsOrthochronous, zero_zero_mul]
-  exact euclid_norm_not_IsFourVelocity_not_IsFourVelocity h h'
+  rw [IsOrthochronous_iff_futurePointing] at h h'
+  rw [IsOrthochronous, timeComp_mul]
+  exact NormOneLorentzVector.FuturePointing.metric_reflect_not_mem_not_mem h h'
 
-lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup} (h :  IsOrthochronous Λ)
+lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h :  IsOrthochronous Λ)
     (h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
+  rw [not_orthochronous_iff_le_zero, timeComp_mul]
   rw [IsOrthochronous_iff_transpose] at h
-  rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h'
-  rw [IsOrthochronous_iff_fstCol_IsFourVelocity, not_IsFourVelocity_iff]
-  simp [stdBasis_mulVec]
-  change (Λ * Λ').1 0 0  ≤ _
-  rw [zero_zero_mul]
-  exact euclid_norm_IsFourVelocity_not_IsFourVelocity h h'
+  rw [IsOrthochronous_iff_futurePointing] at h h'
+  exact NormOneLorentzVector.FuturePointing.metric_reflect_mem_not_mem h h'
 
-lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : LorentzGroup} (h : ¬ IsOrthochronous Λ)
+lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : LorentzGroup d} (h : ¬ IsOrthochronous Λ)
     (h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
+  rw [not_orthochronous_iff_le_zero, timeComp_mul]
   rw [IsOrthochronous_iff_transpose] at h
-  rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h'
-  rw [IsOrthochronous_iff_fstCol_IsFourVelocity, not_IsFourVelocity_iff]
-  simp [stdBasis_mulVec]
-  change (Λ * Λ').1 0 0  ≤ _
-  rw [zero_zero_mul]
-  exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h'
+  rw [IsOrthochronous_iff_futurePointing] at h h'
+  exact NormOneLorentzVector.FuturePointing.metric_reflect_not_mem_mem h h'
 
 /-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
-def orthchroRep : LorentzGroup →* ℤ₂ where
+def orthchroRep : LorentzGroup d →* ℤ₂ where
   toFun := orthchroMap
   map_one' := orthchroMap_IsOrthochronous (by simp [IsOrthochronous])
   map_mul' Λ Λ' := by
@@ -189,5 +180,4 @@ def orthchroRep : LorentzGroup →* ℤ₂ where
 
 end LorentzGroup
 
-end SpaceTime
 end
diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean
index 67d4a1d..56b1ff7 100644
--- a/HepLean/SpaceTime/LorentzGroup/Proper.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean
@@ -14,7 +14,6 @@ We define the give a series of lemmas related to the determinant of the lorentz
 
 noncomputable section
 
-namespace SpaceTime
 
 open Manifold
 open Matrix
@@ -23,10 +22,16 @@ open ComplexConjugate
 
 namespace LorentzGroup
 
+open minkowskiMetric
+
+variable {d : ℕ}
+
 /-- The determinant of a member of the lorentz group is `1` or `-1`. -/
-lemma det_eq_one_or_neg_one (Λ : 𝓛) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by
-  simpa [← sq, det_one, det_mul, det_mul, det_mul, det_transpose, det_η] using
-    (congrArg det ((PreservesηLin.iff_matrix' Λ.1).mp Λ.2))
+lemma det_eq_one_or_neg_one (Λ : 𝓛 d) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by
+  have h1 := (congrArg det ((mem_iff_self_mul_dual).mp Λ.2))
+  simp [det_mul, det_dual] at h1
+  exact mul_self_eq_one_iff.mp h1
+
 
 local notation  "ℤ₂" => Multiplicative (ZMod 2)
 
@@ -47,7 +52,7 @@ def coeForℤ₂ :  C(({-1, 1} : Set ℝ), ℤ₂) where
     exact continuous_of_discreteTopology
 
 /-- The continuous map taking a lorentz matrix to its determinant. -/
-def detContinuous :  C(𝓛, ℤ₂) :=
+def detContinuous :  C(𝓛 d, ℤ₂) :=
   ContinuousMap.comp  coeForℤ₂ {
     toFun := fun Λ => ⟨Λ.1.det, Or.symm (LorentzGroup.det_eq_one_or_neg_one _)⟩,
     continuous_toFun := by
@@ -56,7 +61,7 @@ def detContinuous :  C(𝓛, ℤ₂) :=
         Continuous.comp' (continuous_iff_le_induced.mpr fun U a => a) continuous_id'
       }
 
-lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup) :
+lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
     detContinuous Λ = detContinuous Λ' ↔ Λ.1.det = Λ'.1.det := by
   apply Iff.intro
   intro h
@@ -75,7 +80,7 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup) :
 
 /-- The representation taking a lorentz matrix to its determinant. -/
 @[simps!]
-def detRep : 𝓛 →* ℤ₂ where
+def detRep : 𝓛 d →* ℤ₂ where
   toFun Λ := detContinuous Λ
   map_one' := by
     simp [detContinuous, lorentzGroupIsGroup]
@@ -88,9 +93,9 @@ def detRep : 𝓛 →* ℤ₂ where
       <;> simp [h1, h2, detContinuous]
     rfl
 
-lemma detRep_continuous : Continuous detRep := detContinuous.2
+lemma detRep_continuous : Continuous (@detRep d) := detContinuous.2
 
-lemma det_on_connected_component {Λ Λ'  : LorentzGroup} (h : Λ' ∈ connectedComponent Λ) :
+lemma det_on_connected_component {Λ Λ'  : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
     Λ.1.det = Λ'.1.det := by
   obtain ⟨s, hs, hΛ'⟩ := h
   let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s detContinuous
@@ -99,36 +104,35 @@ lemma det_on_connected_component {Λ Λ'  : LorentzGroup} (h : Λ' ∈ connected
     (@IsPreconnected.subsingleton ℤ₂ _ _ _ (isPreconnected_range f.2))
     (Set.mem_range_self ⟨Λ, hs.2⟩)  (Set.mem_range_self ⟨Λ', hΛ'⟩)
 
-lemma detRep_on_connected_component {Λ Λ'  : LorentzGroup} (h : Λ' ∈ connectedComponent Λ) :
+lemma detRep_on_connected_component {Λ Λ'  : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
     detRep Λ = detRep Λ' := by
   simp [detRep_apply, detRep_apply, detContinuous]
   rw [det_on_connected_component h]
 
-lemma det_of_joined {Λ Λ' : LorentzGroup} (h : Joined Λ Λ') : Λ.1.det = Λ'.1.det :=
+lemma det_of_joined {Λ Λ' : LorentzGroup d} (h : Joined Λ Λ') : Λ.1.det = Λ'.1.det :=
   det_on_connected_component $ pathComponent_subset_component _ h
 
 /-- A Lorentz Matrix is proper if its determinant is 1. -/
 @[simp]
-def IsProper (Λ : LorentzGroup) : Prop := Λ.1.det = 1
+def IsProper (Λ : LorentzGroup d) : Prop := Λ.1.det = 1
 
-instance : DecidablePred IsProper := by
+instance : DecidablePred (@IsProper d) := by
   intro Λ
   apply Real.decidableEq
 
-lemma IsProper_iff (Λ : LorentzGroup) : IsProper Λ ↔ detRep Λ = 1 := by
+lemma IsProper_iff (Λ : LorentzGroup d) : IsProper Λ ↔ detRep Λ = 1 := by
   rw [show 1 = detRep 1 from Eq.symm (MonoidHom.map_one detRep)]
   rw [detRep_apply, detRep_apply, detContinuous_eq_iff_det_eq]
   simp only [IsProper, lorentzGroupIsGroup_one_coe, det_one]
 
-lemma id_IsProper : IsProper 1 := by
+lemma id_IsProper : (@IsProper d) 1 := by
   simp [IsProper]
 
-lemma isProper_on_connected_component {Λ Λ'  : LorentzGroup} (h : Λ' ∈ connectedComponent Λ) :
+lemma isProper_on_connected_component {Λ Λ'  : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
     IsProper Λ ↔ IsProper Λ' := by
   simp [detRep_apply, detRep_apply, detContinuous]
   rw [det_on_connected_component h]
 
 end LorentzGroup
 
-end SpaceTime
 end
diff --git a/HepLean/SpaceTime/LorentzTensors/Basic.lean b/HepLean/SpaceTime/LorentzTensors/Basic.lean
new file mode 100644
index 0000000..dac4a95
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzTensors/Basic.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+/-!
+
+# Lorentz Tensors
+
+This file is currently a stub.
+
+The aim is to define Lorentz tensors, and devlop a systematic way to manipulate them.
+
+To manipulate them we will use the theory of modular operads
+(see e.g. [Raynor][raynor2021graphical]).
+
+-/
diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean
new file mode 100644
index 0000000..9b58852
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzVector/Basic.lean
@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.Data.Complex.Exponential
+import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.LinearAlgebra.Matrix.DotProduct
+import LeanCopilot
+/-!
+
+# Lorentz vectors
+
+(aka 4-vectors)
+
+In this file we define a Lorentz vector (in 4d, this is more often called a 4-vector).
+
+One of the most important example of a Lorentz vector is SpaceTime.
+-/
+
+/- The number of space dimensions . -/
+variable (d : ℕ)
+
+/-- The type of Lorentz Vectors in `d`-space dimensions. -/
+def LorentzVector : Type := (Fin 1 ⊕ Fin d) → ℝ
+
+/-- An instance of a additive commutative monoid on `LorentzVector`. -/
+instance : AddCommMonoid (LorentzVector d) := Pi.addCommMonoid
+
+/-- An instance of a module on `LorentzVector`. -/
+noncomputable instance : Module ℝ (LorentzVector d) := Pi.module _ _ _
+
+instance : AddCommGroup (LorentzVector d) := Pi.addCommGroup
+
+namespace LorentzVector
+
+variable {d : ℕ}
+
+variable (v : LorentzVector d)
+
+/-- The space components. -/
+@[simp]
+def space  : EuclideanSpace ℝ (Fin d) := v ∘ Sum.inr
+
+/-- The time component. -/
+@[simp]
+def time : ℝ := v (Sum.inl 0)
+
+/-!
+
+# The standard basis
+
+-/
+
+/-- The standard basis of `LorentzVector`. -/
+@[simps!]
+noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin (d)) ℝ (LorentzVector d) := Pi.basisFun ℝ _
+
+/-- The standard unit time vector. -/
+@[simp]
+noncomputable def timeVec : (LorentzVector d) := stdBasis (Sum.inl 0)
+
+@[simp]
+lemma timeVec_space : (@timeVec d).space = 0 := by
+  funext i
+  simp [space, stdBasis]
+  erw [Pi.basisFun_apply]
+  simp_all only [Fin.isValue, LinearMap.stdBasis_apply', ↓reduceIte]
+
+@[simp]
+lemma timeVec_time: (@timeVec d).time = 1 := by
+  simp [space, stdBasis]
+  erw [Pi.basisFun_apply]
+  simp_all only [Fin.isValue, LinearMap.stdBasis_apply', ↓reduceIte]
+
+/-!
+
+# Reflection of space
+
+-/
+
+/-- The reflection of space as a linear map. -/
+@[simps!]
+def spaceReflectionLin : LorentzVector d →ₗ[ℝ] LorentzVector d where
+  toFun x := Sum.elim (x ∘ Sum.inl) (- x ∘ Sum.inr)
+  map_add' x y := by
+    funext i
+    rcases i with i | i
+    · simp only [Sum.elim_inl]
+      apply Eq.refl
+    · simp only [Sum.elim_inr, Pi.neg_apply]
+      apply neg_add
+  map_smul' c x := by
+    funext i
+    rcases i with i | i
+    · simp only [Sum.elim_inl, Pi.smul_apply]
+      apply smul_eq_mul
+    · simp [ HSMul.hSMul, SMul.smul]
+
+
+/-- The reflection of space. -/
+@[simp]
+def spaceReflection : LorentzVector d := spaceReflectionLin v
+
+@[simp]
+lemma spaceReflection_space : v.spaceReflection.space = - v.space := by
+  rfl
+
+@[simp]
+lemma spaceReflection_time : v.spaceReflection.time = v.time := by
+  rfl
+
+
+
+end LorentzVector
diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean
new file mode 100644
index 0000000..588db82
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean
@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzVector.Basic
+import HepLean.SpaceTime.MinkowskiMetric
+/-!
+
+# Lorentz vectors with norm one
+
+-/
+
+open minkowskiMetric
+
+@[simp]
+def NormOneLorentzVector (d : ℕ) : Set (LorentzVector d) :=
+  fun x => ⟪x, x⟫ₘ = 1
+
+namespace NormOneLorentzVector
+
+variable {d : ℕ}
+
+variable (v w : NormOneLorentzVector d)
+
+lemma mem_iff {x : LorentzVector d} : x ∈ NormOneLorentzVector d ↔ ⟪x, x⟫ₘ = 1 := by
+  rfl
+
+/-- The negative of a `NormOneLorentzVector` as a `NormOneLorentzVector`. -/
+def neg : NormOneLorentzVector d := ⟨- v, by
+  rw [mem_iff]
+  simp only [map_neg, LinearMap.neg_apply, neg_neg]
+  exact v.2⟩
+
+lemma time_sq  : v.1.time ^ 2 = 1 + ‖v.1.space‖ ^ 2  := by
+  rw [time_sq_eq_metric_add_space, v.2]
+
+lemma abs_time_ge_one : 1 ≤ |v.1.time| := by
+  have h1 := leq_time_sq v.1
+  rw [v.2] at h1
+  exact (one_le_sq_iff_one_le_abs _).mp h1
+
+lemma norm_space_le_abs_time : ‖v.1.space‖ < |v.1.time| := by
+  rw [(abs_norm _).symm, ← @sq_lt_sq, time_sq]
+  exact lt_one_add (‖(v.1).space‖ ^ 2)
+
+lemma norm_space_leq_abs_time  : ‖v.1.space‖ ≤ |v.1.time| :=
+  le_of_lt (norm_space_le_abs_time v)
+
+lemma time_le_minus_one_or_ge_one : v.1.time ≤ -1 ∨ 1 ≤ v.1.time :=
+  le_abs'.mp (abs_time_ge_one v)
+
+lemma time_nonpos_iff : v.1.time ≤ 0 ↔ v.1.time ≤ - 1 := by
+  apply Iff.intro
+  · intro h
+    cases' time_le_minus_one_or_ge_one v with h1 h1
+    exact h1
+    linarith
+  · intro h
+    linarith
+
+
+lemma time_nonneg_iff : 0 ≤ v.1.time ↔ 1 ≤ v.1.time := by
+  apply Iff.intro
+  · intro h
+    cases' time_le_minus_one_or_ge_one v with h1 h1
+    linarith
+    exact h1
+  · intro h
+    linarith
+
+lemma time_pos_iff : 0 < v.1.time ↔ 1 ≤ v.1.time := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · exact (time_nonneg_iff v).mp (le_of_lt h)
+  · linarith
+
+lemma time_abs_sub_space_norm  :
+    0 ≤ |v.1.time| * |w.1.time| - ‖v.1.space‖ * ‖w.1.space‖ := by
+  apply sub_nonneg.mpr
+  apply mul_le_mul (norm_space_leq_abs_time v) (norm_space_leq_abs_time w) ?_ ?_
+  exact norm_nonneg w.1.space
+  exact abs_nonneg (v.1 _)
+
+/-!
+
+# Future pointing norm one Lorentz vectors
+
+-/
+
+/-- The future pointing Lorentz vectors with Norm one. -/
+def FuturePointing (d : ℕ) : Set (NormOneLorentzVector d) :=
+  fun x => 0 < x.1.time
+
+namespace FuturePointing
+
+variable (f f' : FuturePointing d)
+
+lemma mem_iff : v ∈ FuturePointing d ↔ 0 < v.1.time := by
+  rfl
+
+lemma mem_iff_time_nonneg : v ∈ FuturePointing d ↔ 0 ≤ v.1.time := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  exact le_of_lt ((mem_iff v).mp h)
+  have h1 := (mem_iff v).mp
+  simp at h1
+  rw [@time_nonneg_iff] at h
+  rw [mem_iff]
+  linarith
+
+lemma not_mem_iff : v ∉ FuturePointing d ↔ v.1.time ≤ 0 := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  exact le_of_not_lt ((mem_iff v).mp.mt h)
+  have h1 := (mem_iff v).mp.mt
+  simp at h1
+  exact h1 h
+
+lemma not_mem_iff_neg : v ∉ FuturePointing d ↔ neg v ∈ FuturePointing d := by
+  rw [not_mem_iff, mem_iff_time_nonneg]
+  simp only [Fin.isValue, neg]
+  change _ ↔ 0 ≤ - v.1 _
+  exact Iff.symm neg_nonneg
+
+lemma time_nonneg : 0 ≤ f.1.1.time := le_of_lt f.2
+
+lemma abs_time : |f.1.1.time| = f.1.1.time := abs_of_nonneg (time_nonneg f)
+
+/-!
+
+# The value sign of ⟪v, w.1.spaceReflection⟫ₘ different v and w
+
+-/
+
+section
+variable {v w : NormOneLorentzVector d}
+
+lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) :
+    0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
+  apply le_trans (time_abs_sub_space_norm v w)
+  rw [abs_time ⟨v, h⟩, abs_time ⟨w, hw⟩ , sub_eq_add_neg, right_spaceReflection]
+  apply (add_le_add_iff_left _).mpr
+  rw [neg_le]
+  apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (w.1).space⟫_ℝ|) ?_
+  exact abs_real_inner_le_norm (v.1).space (w.1).space
+
+
+lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) :
+    0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ  := by
+  have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) ((not_mem_iff_neg w).mp hw)
+  apply le_of_le_of_eq h1 ?_
+  simp [neg]
+
+
+lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) :
+    ⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by
+  rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
+  have h1 := metric_reflect_mem_mem h ((not_mem_iff_neg w).mp hw)
+  apply le_of_le_of_eq h1 ?_
+  simp [neg]
+
+lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw :  w ∈ FuturePointing d) :
+    ⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by
+  rw [show (0 : ℝ) = - 0 by simp, le_neg]
+  have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h)  hw
+  apply le_of_le_of_eq h1 ?_
+  simp [neg]
+
+end
+
+end FuturePointing
+
+
+end NormOneLorentzVector
diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean
index 3a7ca46..3c54274 100644
--- a/HepLean/SpaceTime/Metric.lean
+++ b/HepLean/SpaceTime/Metric.lean
@@ -11,6 +11,12 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic
 
 This file introduces the metric on spacetime in the (+, -, -, -) signature.
 
+## TODO
+
+This file needs refactoring.
+- The metric should be defined as a bilinear map on `LorentzVector d`.
+- From this definition, we should derive the metric as a matrix.
+
 -/
 
 noncomputable section
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
new file mode 100644
index 0000000..bfc842d
--- /dev/null
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -0,0 +1,307 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzVector.Basic
+import Mathlib.Algebra.Lie.Classical
+import Mathlib.LinearAlgebra.QuadraticForm.Basic
+/-!
+
+# The Minkowski Metric
+
+This file introduces the Minkowski metric on spacetime in the mainly-minus signature.
+
+We define the minkowski metric as a bilinear map on the vector space
+of Lorentz vectors in d dimensions.
+
+-/
+
+
+open Matrix
+
+/-!
+
+# The definition of the Minkowski Matrix
+
+-/
+/-- The `d.succ`-dimensional real of the form `diag(1, -1, -1, -1, ...)`. -/
+def minkowskiMatrix {d : ℕ} : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
+  LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin d) ℝ
+
+namespace minkowskiMatrix
+
+variable {d : ℕ}
+
+scoped[minkowskiMatrix] notation "η" => minkowskiMatrix
+
+@[simp]
+lemma sq : @minkowskiMatrix d * minkowskiMatrix  = 1 := by
+  simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
+  ext1 i j
+  rcases i with i | i <;> rcases j with j | j
+  · simp only [diagonal, of_apply, Sum.inl.injEq, Sum.elim_inl, mul_one]
+    split
+    · simp_all only [one_apply_eq]
+    · simp_all only [ne_eq, Sum.inl.injEq, not_false_eq_true, one_apply_ne]
+  · simp only [ne_eq, not_false_eq_true, diagonal_apply_ne, one_apply_ne]
+  · simp only [ne_eq, not_false_eq_true, diagonal_apply_ne, one_apply_ne]
+  · simp only [diagonal, of_apply, Sum.inr.injEq, Sum.elim_inr, mul_neg, mul_one, neg_neg]
+    split
+    · simp_all only [one_apply_eq]
+    · simp_all only [ne_eq, Sum.inr.injEq, not_false_eq_true, one_apply_ne]
+
+@[simp]
+lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
+  simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose]
+
+
+@[simp]
+lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
+  simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
+
+
+
+end minkowskiMatrix
+
+
+/-!
+
+# The definition of the Minkowski Metric
+
+-/
+
+/-- Given a Lorentz vector `v` we define the the linear map `w ↦ v * η * w  -/
+@[simps!]
+def minkowskiLinearForm {d : ℕ} (v : LorentzVector d) : LorentzVector d →ₗ[ℝ] ℝ where
+  toFun w := v ⬝ᵥ (minkowskiMatrix *ᵥ w)
+  map_add' y z := by
+    noncomm_ring
+    rw [mulVec_add, dotProduct_add]
+  map_smul' c y := by
+    simp only [RingHom.id_apply, smul_eq_mul]
+    rw [mulVec_smul, dotProduct_smul]
+    rfl
+
+/-- The Minkowski metric as a bilinear map. -/
+def minkowskiMetric {d : ℕ} :  LorentzVector d →ₗ[ℝ] LorentzVector d →ₗ[ℝ] ℝ where
+  toFun v := minkowskiLinearForm v
+  map_add' y z := by
+    ext1 x
+    simp only [minkowskiLinearForm_apply, LinearMap.add_apply]
+    apply add_dotProduct
+  map_smul' c y := by
+    ext1 x
+    simp only [minkowskiLinearForm_apply, RingHom.id_apply, LinearMap.smul_apply, smul_eq_mul]
+    rw [smul_dotProduct]
+    rfl
+
+namespace minkowskiMetric
+
+open minkowskiMatrix
+
+open LorentzVector
+
+variable {d : ℕ}
+variable (v w : LorentzVector d)
+
+scoped[minkowskiMetric] notation "⟪" v "," w "⟫ₘ" => minkowskiMetric v w
+/-!
+
+# Equalitites involving the Minkowski metric
+
+-/
+
+/-- The Minkowski metric expressed as a sum. -/
+lemma as_sum :
+    ⟪v, w⟫ₘ = v.time * w.time - ∑ i, v.space i * w.space i := by
+  simp only [minkowskiMetric, LinearMap.coe_mk, AddHom.coe_mk, minkowskiLinearForm_apply,
+    dotProduct, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal, Fintype.sum_sum_type,
+    Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Sum.elim_inl, one_mul,
+    Finset.sum_singleton, Sum.elim_inr, neg_mul, mul_neg, Finset.sum_neg_distrib, time, space,
+    Function.comp_apply, minkowskiMatrix]
+  ring
+
+
+/-- The Minkowski metric expressed as a sum for a single vector. -/
+lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
+  rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
+  noncomm_ring
+
+lemma eq_time_minus_inner_prod : ⟪v, w⟫ₘ = v.time * w.time - ⟪v.space, w.space⟫_ℝ  := by
+  rw [as_sum, @PiLp.inner_apply]
+  noncomm_ring
+
+lemma self_eq_time_minus_norm : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
+  rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
+  noncomm_ring
+
+/-- The Minkowski metric is symmetric. -/
+lemma symm : ⟪v, w⟫ₘ = ⟪w, v⟫ₘ := by
+  simp only [as_sum]
+  ac_rfl
+
+lemma time_sq_eq_metric_add_space : v.time ^ 2 = ⟪v, v⟫ₘ + ‖v.space‖ ^ 2 := by
+  rw [self_eq_time_minus_norm]
+  exact Eq.symm (sub_add_cancel (v.time ^ 2) (‖v.space‖ ^ 2))
+
+/-!
+
+#  Minkowski metric and space reflections
+
+-/
+
+lemma right_spaceReflection : ⟪v, w.spaceReflection⟫ₘ = v.time * w.time + ⟪v.space, w.space⟫_ℝ := by
+  rw [eq_time_minus_inner_prod, spaceReflection_space, spaceReflection_time]
+  simp only [time, Fin.isValue, space, inner_neg_right, PiLp.inner_apply, Function.comp_apply,
+    RCLike.inner_apply, conj_trivial, sub_neg_eq_add]
+
+
+lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v = 0 := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · rw [right_spaceReflection] at h
+    have h2 : 0 ≤ ⟪v.space, v.space⟫_ℝ := real_inner_self_nonneg
+    have h3 : v.time * v.time = 0 := by linarith [mul_self_nonneg v.time]
+    have h4 : ⟪v.space, v.space⟫_ℝ = 0 := by linarith
+    simp only [time, Fin.isValue, mul_eq_zero, or_self] at h3
+    rw [@inner_self_eq_zero] at h4
+    funext i
+    rcases i with i | i
+    · fin_cases i
+      exact h3
+    · simpa using congrFun h4 i
+  · rw [h]
+    simp only [map_zero, LinearMap.zero_apply]
+/-!
+
+# Non degeneracy of the Minkowski metric
+
+-/
+
+/-- The metric tensor is non-degenerate. -/
+lemma nondegenerate : (∀ w, ⟪w, v⟫ₘ = 0) ↔ v = 0 := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · exact (self_spaceReflection_eq_zero_iff _ ).mp ((symm _ _).trans $ h v.spaceReflection)
+  · simp [h]
+
+
+/-!
+
+# Inequalitites involving the Minkowski metric
+
+-/
+
+lemma leq_time_sq  : ⟪v, v⟫ₘ ≤ v.time ^ 2 := by
+  rw [time_sq_eq_metric_add_space]
+  exact (le_add_iff_nonneg_right _).mpr $ sq_nonneg ‖v.space‖
+
+lemma ge_abs_inner_product : v.time * w.time - ‖⟪v.space, w.space⟫_ℝ‖ ≤ ⟪v, w⟫ₘ := by
+  rw [eq_time_minus_inner_prod, sub_le_sub_iff_left]
+  exact Real.le_norm_self ⟪v.space, w.space⟫_ℝ
+
+lemma ge_sub_norm : v.time * w.time - ‖v.space‖ * ‖w.space‖ ≤ ⟪v, w⟫ₘ := by
+  apply le_trans ?_ (ge_abs_inner_product v w)
+  rw [sub_le_sub_iff_left]
+  exact norm_inner_le_norm v.space w.space
+
+/-!
+
+# The Minkowski metric and the standard basis
+
+-/
+
+lemma on_timeVec : ⟪timeVec, @timeVec d⟫ₘ = 1 := by
+  rw [self_eq_time_minus_norm, timeVec_time, timeVec_space]
+  simp [LorentzVector.stdBasis, minkowskiMetric]
+
+/-!
+
+# The Minkowski metric and matrices
+
+-/
+section matrices
+
+variable (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
+
+/-- The dual of a matrix with respect to the Minkowski metric. -/
+def dual : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := η * Λᵀ * η
+
+@[simp]
+lemma dual_id : @dual d 1 = 1 := by
+  simpa only [dual, transpose_one, mul_one] using minkowskiMatrix.sq
+
+@[simp]
+lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
+  simp only [dual, transpose_mul]
+  trans  η * Λ'ᵀ * (η * η) * Λᵀ * η
+  noncomm_ring [minkowskiMatrix.sq]
+  noncomm_ring
+
+@[simp]
+lemma dual_dual : dual (dual Λ) = Λ := by
+  simp only [dual, transpose_mul, transpose_transpose, eq_transpose]
+  trans (η * η) * Λ * (η * η)
+  noncomm_ring
+  noncomm_ring [minkowskiMatrix.sq]
+
+@[simp]
+lemma dual_eta : @dual d η = η := by
+  simp only [dual, eq_transpose]
+  noncomm_ring [minkowskiMatrix.sq]
+
+@[simp]
+lemma dual_transpose : dual Λᵀ = (dual Λ)ᵀ := by
+  simp only [dual, transpose_transpose, transpose_mul, eq_transpose]
+  noncomm_ring
+
+@[simp]
+lemma det_dual : (dual Λ).det = Λ.det := by
+  simp only [dual, det_mul, minkowskiMatrix.det_eq_neg_one_pow_d, det_transpose]
+  group
+  norm_cast
+  simp
+
+@[simp]
+lemma dual_mulVec_right : ⟪x, (dual Λ) *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ  := by
+  simp only [minkowskiMetric, LinearMap.coe_mk, AddHom.coe_mk, dual, minkowskiLinearForm_apply,
+    mulVec_mulVec, ← mul_assoc, minkowskiMatrix.sq, one_mul, (vecMul_transpose Λ x).symm, ←
+    dotProduct_mulVec]
+
+@[simp]
+lemma dual_mulVec_left : ⟪(dual Λ) *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ := by
+  rw [symm, dual_mulVec_right, symm]
+
+lemma matrix_apply_eq_iff_sub  : ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ ↔  ⟪v, (Λ - Λ') *ᵥ w⟫ₘ = 0 := by
+  rw [← sub_eq_zero, ← LinearMap.map_sub, sub_mulVec]
+
+lemma matrix_eq_iff_eq_forall' : (∀ v, Λ *ᵥ v= Λ' *ᵥ v) ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · intro w v
+    rw [h w]
+  · simp only [matrix_apply_eq_iff_sub] at h
+    intro v
+    refine sub_eq_zero.1 ?_
+    have h1 := h v
+    rw [nondegenerate] at h1
+    simp [sub_mulVec] at h1
+    exact  h1
+
+lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
+  rw [← matrix_eq_iff_eq_forall']
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · rw [h]
+    simp
+  · rw [← (LinearMap.toMatrix stdBasis stdBasis).toEquiv.symm.apply_eq_iff_eq]
+    ext1 x
+    simp only [LinearEquiv.coe_toEquiv_symm, LinearMap.toMatrix_symm, EquivLike.coe_coe,
+      toLin_apply, h, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
+      Finset.sum_singleton]
+
+lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
+  rw [matrix_eq_iff_eq_forall]
+  simp
+
+
+end matrices
+
+end minkowskiMetric
diff --git a/docs/references.bib b/docs/references.bib
index c99cd7f..6022c68 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -1,3 +1,4 @@
+
 # To normalize:
 # bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i docs/references.bib -o docs/references.bib
 
@@ -5,7 +6,6 @@
 
 # To link to an entry in `references.bib`, use the following formats:
 #   [Author, *Title* (optional location)][bibkey]
-
 @Article{         Allanach:2021yjy,
   author        = "Allanach, B. C. and Madigan, Maeve and Tooby-Smith,
                   Joseph",
@@ -33,3 +33,14 @@
   pages         = "009",
   year          = "2020"
 }
+
+@Article{         raynor2021graphical,
+  title         = {Graphical combinatorics and a distributive law for modular
+                  operads},
+  author        = {Raynor, Sophie},
+  journal       = {Advances in Mathematics},
+  volume        = {392},
+  pages         = {108011},
+  year          = {2021},
+  publisher     = {Elsevier}
+}