diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
new file mode 100644
index 0000000..25245fa
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzAlgebra.Basic
+/-!
+# Basis of the Lorentz Algebra
+
+We define the standard basis of the Lorentz group.
+
+-/
+
+
+
+
+
+
+namespace spaceTime
+
+namespace lorentzAlgebra
+open Matrix
+
+
+
+@[simp]
+def σMat (μ ν : Fin 4) : Matrix (Fin 4) (Fin 4) ℝ := fun ρ δ ↦
+  η^[ρ]_[μ] * η_[ν]_[δ] - η_[μ]_[δ] * η^[ρ]_[ν]
+
+
+
+end lorentzAlgebra
+
+end spaceTime
diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean
index 7bb4dce..5d428e0 100644
--- a/HepLean/SpaceTime/Metric.lean
+++ b/HepLean/SpaceTime/Metric.lean
@@ -29,6 +29,21 @@ open TensorProduct
 def η : Matrix (Fin 4) (Fin 4) ℝ := Matrix.reindex finSumFinEquiv finSumFinEquiv
   $ LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ
 
+notation "η_[" μ "]_[" ν "]" => η μ ν
+
+notation "η^[" μ "]^[" ν "]" => η μ ν
+
+notation "η_[" μ "]^[" ν "]" => η_[μ]_[0] * η^[0]^[ν] + η_[μ]_[1] * η^[1]^[ν] + η_[μ]_[2] * η^[2]^[ν]
+  + η_[μ]_[3] * η^[3]^[ν]
+
+notation "η^[" μ "]_[" ν "]" => η^[μ]^[0] * η_[0]_[ν] + η^[μ]^[1] * η_[1]_[ν] + η^[μ]^[2] * η_[2]_[ν]
+  + η^[μ]^[3] * η_[3]_[ν]
+
+notation "["Λ"]^[" μ "]_[" ν "]" => (Λ : Matrix (Fin 4) (Fin 4) ℝ) μ ν
+
+notation "["Λ"]_[" μ "]_[" ν "]" => ∑ ρ, η_[μ]_[ρ] * [Λ]^[ρ]_[ν]
+
+
 lemma η_block : η = Matrix.reindex finSumFinEquiv finSumFinEquiv (
     Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin 3) (Fin 3) ℝ)) := by
   rw [η]
@@ -102,6 +117,13 @@ lemma η_mulVec (x : spaceTime) : η *ᵥ x = ![x 0, -x 1, -x 2, -x 3] := by
   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
+
+
 /-- Given a point in spaceTime `x` the linear map `y → x ⬝ᵥ (η *ᵥ y)`. -/
 @[simps!]
 def linearMapForSpaceTime (x : spaceTime) : spaceTime →ₗ[ℝ] ℝ where