diff --git a/HepLean.lean b/HepLean.lean
index 3e318e1..d43e778 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -64,12 +64,19 @@ import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
 import HepLean.Lorentz.Algebra.Basic
 import HepLean.Lorentz.Algebra.Basis
+import HepLean.Lorentz.ComplexVector.Basic
+import HepLean.Lorentz.ComplexVector.Contraction
+import HepLean.Lorentz.ComplexVector.Metric
+import HepLean.Lorentz.ComplexVector.Modules
+import HepLean.Lorentz.ComplexVector.Two
+import HepLean.Lorentz.ComplexVector.Unit
 import HepLean.Lorentz.Group.Basic
 import HepLean.Lorentz.Group.Boosts
 import HepLean.Lorentz.Group.Orthochronous
 import HepLean.Lorentz.Group.Proper
 import HepLean.Lorentz.Group.Restricted
 import HepLean.Lorentz.Group.Rotations
+import HepLean.Lorentz.MinkowskiMatrix
 import HepLean.Lorentz.RealVector.Basic
 import HepLean.Lorentz.RealVector.Contraction
 import HepLean.Lorentz.RealVector.Modules
@@ -88,13 +95,6 @@ import HepLean.Meta.Informal
 import HepLean.Meta.TransverseTactics
 import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.CliffordAlgebra
-import HepLean.SpaceTime.LorentzVector.Complex.Basic
-import HepLean.SpaceTime.LorentzVector.Complex.Contraction
-import HepLean.SpaceTime.LorentzVector.Complex.Metric
-import HepLean.SpaceTime.LorentzVector.Complex.Modules
-import HepLean.SpaceTime.LorentzVector.Complex.Two
-import HepLean.SpaceTime.LorentzVector.Complex.Unit
-import HepLean.SpaceTime.MinkowskiMatrix
 import HepLean.SpaceTime.PauliMatrices.AsTensor
 import HepLean.SpaceTime.PauliMatrices.Basic
 import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
diff --git a/HepLean/Lorentz/Algebra/Basic.lean b/HepLean/Lorentz/Algebra/Basic.lean
index 558ff76..3583e6f 100644
--- a/HepLean/Lorentz/Algebra/Basic.lean
+++ b/HepLean/Lorentz/Algebra/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.MinkowskiMatrix
+import HepLean.Lorentz.MinkowskiMatrix
 import Mathlib.Algebra.Lie.Classical
 import HepLean.Lorentz.RealVector.Basic
 /-!
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean b/HepLean/Lorentz/ComplexVector/Basic.lean
similarity index 99%
rename from HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
rename to HepLean/Lorentz/ComplexVector/Basic.lean
index 8f0c91c..0e151d7 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Basic.lean
+++ b/HepLean/Lorentz/ComplexVector/Basic.lean
@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import HepLean.SpaceTime.SL2C.Basic
-import HepLean.SpaceTime.LorentzVector.Complex.Modules
+import HepLean.Lorentz.ComplexVector.Modules
 import HepLean.Meta.Informal
 import Mathlib.RepresentationTheory.Rep
 import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean b/HepLean/Lorentz/ComplexVector/Contraction.lean
similarity index 99%
rename from HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean
rename to HepLean/Lorentz/ComplexVector/Contraction.lean
index 4435ec9..b4661fe 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Contraction.lean
+++ b/HepLean/Lorentz/ComplexVector/Contraction.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzVector.Complex.Basic
+import HepLean.Lorentz.ComplexVector.Basic
 /-!
 
 # Contraction of Lorentz vectors
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean b/HepLean/Lorentz/ComplexVector/Metric.lean
similarity index 97%
rename from HepLean/SpaceTime/LorentzVector/Complex/Metric.lean
rename to HepLean/Lorentz/ComplexVector/Metric.lean
index 2e7ace3..b7887a7 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean
+++ b/HepLean/Lorentz/ComplexVector/Metric.lean
@@ -3,10 +3,10 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzVector.Complex.Two
-import HepLean.SpaceTime.MinkowskiMatrix
-import HepLean.SpaceTime.LorentzVector.Complex.Contraction
-import HepLean.SpaceTime.LorentzVector.Complex.Unit
+import HepLean.Lorentz.ComplexVector.Two
+import HepLean.Lorentz.MinkowskiMatrix
+import HepLean.Lorentz.ComplexVector.Contraction
+import HepLean.Lorentz.ComplexVector.Unit
 /-!
 
 # Metric for complex Lorentz vectors
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Modules.lean b/HepLean/Lorentz/ComplexVector/Modules.lean
similarity index 100%
rename from HepLean/SpaceTime/LorentzVector/Complex/Modules.lean
rename to HepLean/Lorentz/ComplexVector/Modules.lean
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Two.lean b/HepLean/Lorentz/ComplexVector/Two.lean
similarity index 99%
rename from HepLean/SpaceTime/LorentzVector/Complex/Two.lean
rename to HepLean/Lorentz/ComplexVector/Two.lean
index 05b6f0e..6f2cef4 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Two.lean
+++ b/HepLean/Lorentz/ComplexVector/Two.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzVector.Complex.Basic
+import HepLean.Lorentz.ComplexVector.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Matrix
 /-!
 
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean b/HepLean/Lorentz/ComplexVector/Unit.lean
similarity index 98%
rename from HepLean/SpaceTime/LorentzVector/Complex/Unit.lean
rename to HepLean/Lorentz/ComplexVector/Unit.lean
index 0229513..a1eb6af 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Unit.lean
+++ b/HepLean/Lorentz/ComplexVector/Unit.lean
@@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzVector.Complex.Two
-import HepLean.SpaceTime.LorentzVector.Complex.Contraction
+import HepLean.Lorentz.ComplexVector.Two
+import HepLean.Lorentz.ComplexVector.Contraction
 /-!
 
 # Unit for complex Lorentz vectors
diff --git a/HepLean/Lorentz/Group/Basic.lean b/HepLean/Lorentz/Group/Basic.lean
index c0dfc89..615a998 100644
--- a/HepLean/Lorentz/Group/Basic.lean
+++ b/HepLean/Lorentz/Group/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.MinkowskiMatrix
+import HepLean.Lorentz.MinkowskiMatrix
 /-!
 # The Lorentz Group
 
diff --git a/HepLean/SpaceTime/MinkowskiMatrix.lean b/HepLean/Lorentz/MinkowskiMatrix.lean
similarity index 100%
rename from HepLean/SpaceTime/MinkowskiMatrix.lean
rename to HepLean/Lorentz/MinkowskiMatrix.lean
diff --git a/HepLean/SpaceTime/PauliMatrices/AsTensor.lean b/HepLean/SpaceTime/PauliMatrices/AsTensor.lean
index 3f493ca..126579b 100644
--- a/HepLean/SpaceTime/PauliMatrices/AsTensor.lean
+++ b/HepLean/SpaceTime/PauliMatrices/AsTensor.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.OverColor.Basic
 import HepLean.Mathematics.PiTensorProduct
-import HepLean.SpaceTime.LorentzVector.Complex.Basic
+import HepLean.Lorentz.ComplexVector.Basic
 import HepLean.Lorentz.Weyl.Two
 import HepLean.SpaceTime.PauliMatrices.Basic
 /-!
diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean
index d02a135..c3ed6f2 100644
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@@ -8,9 +8,9 @@ import HepLean.Tensors.Tree.Dot
 import HepLean.Lorentz.Weyl.Contraction
 import HepLean.Lorentz.Weyl.Metric
 import HepLean.Lorentz.Weyl.Unit
-import HepLean.SpaceTime.LorentzVector.Complex.Contraction
-import HepLean.SpaceTime.LorentzVector.Complex.Metric
-import HepLean.SpaceTime.LorentzVector.Complex.Unit
+import HepLean.Lorentz.ComplexVector.Contraction
+import HepLean.Lorentz.ComplexVector.Metric
+import HepLean.Lorentz.ComplexVector.Unit
 import HepLean.Mathematics.PiTensorProduct
 import HepLean.SpaceTime.PauliMatrices.AsTensor
 /-!
diff --git a/HepLean/Tensors/OverColor/Basic.lean b/HepLean/Tensors/OverColor/Basic.lean
index f0a561b..ff40e87 100644
--- a/HepLean/Tensors/OverColor/Basic.lean
+++ b/HepLean/Tensors/OverColor/Basic.lean
@@ -10,7 +10,7 @@ import Mathlib.CategoryTheory.Comma.Over
 import Mathlib.CategoryTheory.Core
 import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import HepLean.Lorentz.Weyl.Basic
-import HepLean.SpaceTime.LorentzVector.Complex.Basic
+import HepLean.Lorentz.ComplexVector.Basic
 /-!
 
 # Over color category.