feat: Add properties of the Lorentz basis

HepLean/SpaceTime/LorentzAlgebra/Basis.lean

@@ -21,6 +21,55 @@ open Matrix
 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, add_apply, smul_apply, σMat, smul_eq_mul]
+  rw [σMat_mul, σMat_mul, η_symmetric α γ, η_symmetric α δ, η_symmetric β γ, η_symmetric β δ]
+  ring
+
+
 end lorentzAlgebra
 
 end spaceTime

HepLean/SpaceTime/Metric.lean

@@ -32,16 +32,11 @@ def η : Matrix (Fin 4) (Fin 4) ℝ := Matrix.reindex finSumFinEquiv finSumFinEq
 /-- 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 "η^[" μ "]^[" ν "]" => η μ ν
-
-/-- The metric with one lower and one upper index. -/
-notation "η_[" μ "]^[" ν "]" => η_[μ]_[0] * η^[0]^[ν] + η_[μ]_[1] * η^[1]^[ν] +
-  η_[μ]_[2] * η^[2]^[ν] + η_[μ]_[3] * η^[3]^[ν]
-
-/-- The metric with one lower and one upper index. -/
-notation "η^[" μ "]_[" ν "]" => η^[μ]^[0] * η_[0]_[ν] + η^[μ]^[1] * η_[1]_[ν]
-  + η^[μ]^[2] * η_[2]_[ν] + η^[μ]^[3] * η_[3]_[ν]
+notation "η^[" μ "]^[" ν "]" => ηInv μ ν
 
 /-- A matrix with one lower and one upper index. -/
 notation "["Λ"]^[" μ "]_[" ν "]" => (Λ : Matrix (Fin 4) (Fin 4) ℝ) μ ν
@@ -49,6 +44,12 @@ 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
@@ -129,6 +130,26 @@ lemma η_as_diagonal : η = diagonal ![1, -1, -1, -1] := by
   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!]