feat: Add basis of the Lorentz algebra

HepLean/SpaceTime/LorentzAlgebra/Basic.lean

@@ -76,6 +76,28 @@ lemma mem_iff'  (A : Matrix (Fin 4) (Fin 4) ℝ) : A ∈ lorentzAlgebra ↔ A  =
   nth_rewrite 2 [h]
   simp [← mul_assoc, η_sq]
 
+lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 4) : Λ.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
+
+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
+
 
 end lorentzAlgebra
 

HepLean/SpaceTime/LorentzAlgebra/Basis.lean

@@ -19,17 +19,17 @@ 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 : (η^[δ]_[μ] * η_[ν]_[ρ] - η_[μ]_[ρ] * η^[δ]_[ν]) * η_[δ]_[δ]
-    = ((η^[δ]_[μ] * η_[δ]_[δ]) * η_[ν]_[ρ] - η_[μ]_[ρ] * (η^[δ]_[ν]  * η_[δ]_[δ])))
+    ((η^[ρ]_[μ] * η_[ρ]_[ρ]) * η_[ν]_[δ] - η_[μ]_[δ] * (η^[ρ]_[ν] *  η_[ρ]_[ρ])) =
+    -(η_[ρ]_[ρ] * (η_[μ]_[δ] * η^[ρ]_[ν] - η^[ρ]_[μ] * η_[ν]_[δ] )))
+  apply Eq.trans (by ring : (η_[μ]_[ρ] * η^[δ]_[ν] - η^[δ]_[μ] * η_[ν]_[ρ]) * η_[δ]_[δ]
+    = (- (η^[δ]_[μ] * η_[δ]_[δ]) * η_[ν]_[ρ] + η_[μ]_[ρ] * (η^[δ]_[ν]  * η_[δ]_[δ])))
   rw [η_mul_self, η_mul_self, η_mul_self, η_mul_self]
   ring
 
@@ -60,7 +60,7 @@ lemma σMat_mul (α β γ δ  a b: Fin 4) :
 
 lemma σ_comm (α β γ δ : Fin 4) :
     ⁅σ α β , σ γ δ⁆ =
-    η_[α]_[δ] • σ β γ + η_[α]_[γ] • σ δ β + η_[β]_[δ] • σ γ α + η_[β]_[γ] • σ α δ := by
+    η_[α]_[δ] • σ γ β + η_[α]_[γ] • σ β δ + η_[β]_[δ] • σ α γ + η_[β]_[γ] • σ δ α := by
   refine SetCoe.ext ?_
   change σMat α β * σ γ δ -  σ γ δ * σ α β = _
   funext a b
@@ -69,6 +69,79 @@ lemma σ_comm (α β γ δ : Fin 4) :
   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,
+     add_apply, 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
+    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,
+     add_apply, 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!]
+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_all
+  simp [FiniteDimensional.finrank]
+  rw [h]
+  simp only [Cardinal.toNat_ofNat]
 
 end lorentzAlgebra
 

HepLean/SpaceTime/Metric.lean

@@ -73,11 +73,7 @@ lemma η_explicit : η = !![(1 : ℝ), 0, 0, 0; 0, -1, 0, 0; 0, 0, -1, 0; 0, 0,
   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, η, Fin.zero_eta, Matrix.cons_val',
-      Matrix.cons_val_fin_one, Matrix.cons_val_one,
-      Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
-      Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
-      vecHead, vecTail, Function.comp_apply]
+  all_goals simp [finSumFinEquiv, Fin.addCases, η, vecHead, vecTail]
   any_goals rfl
   all_goals split
   all_goals simp
@@ -87,11 +83,7 @@ lemma η_explicit : η = !![(1 : ℝ), 0, 0, 0; 0, -1, 0, 0; 0, 0, -1, 0; 0, 0,
 lemma η_off_diagonal {μ ν : Fin 4} (h : μ ≠ ν) : η μ ν = 0 := by
   fin_cases μ <;>
     fin_cases ν <;>
-      simp_all [η_explicit, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one,
-      Matrix.cons_val_one,
-      Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
-      Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
-      vecHead, vecTail, Function.comp_apply]
+      simp_all [η_explicit, Fin.mk_one, Fin.mk_one, vecHead, vecTail]
 
 lemma η_symmetric (μ ν : Fin 4) : η μ ν = η ν μ := by
   by_cases h : μ = ν
@@ -270,11 +262,7 @@ lemma ηLin_matrix_eq_identity_iff (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
     have h1 := h (stdBasis μ) (stdBasis ν)
     rw [ηLin_matrix_stdBasis, ηLin_η_stdBasis] at h1
     fin_cases μ <;> fin_cases ν <;>
-    simp_all [η_explicit, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one,
-      Matrix.cons_val_one,
-      Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
-      Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
-      vecHead, vecTail, Function.comp_apply]
+    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