Merge pull request #49 from HEPLean/LorentzAlgebra

Some minor adjustments to Lorentz algebra/group

HepLean.lean

@@ -60,6 +60,7 @@ import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.CliffordAlgebra
 import HepLean.SpaceTime.FourVelocity
 import HepLean.SpaceTime.LorentzAlgebra.Basic
+import HepLean.SpaceTime.LorentzAlgebra.Basis
 import HepLean.SpaceTime.LorentzGroup.Basic
 import HepLean.SpaceTime.LorentzGroup.Boosts
 import HepLean.SpaceTime.LorentzGroup.Orthochronous

HepLean/SpaceTime/LorentzAlgebra/Basic.lean

@@ -13,6 +13,12 @@ import Mathlib.Analysis.InnerProductSpace.Adjoint
 /-!
 # The Lorentz Algebra
 
+We define
+
+- Define `lorentzAlgebra` via `LieAlgebra.Orthogonal.so'` as a subalgebra of
+  `Matrix (Fin 4) (Fin 4) ℝ`.
+- In `mem_iff` prove that a matrix is in the Lorentz algebra if and only if it satisfies the
+  condition `Aᵀ * η  = - η * A`.
 
 -/
 
@@ -26,61 +32,45 @@ def lorentzAlgebra : LieSubalgebra ℝ (Matrix (Fin 4) (Fin 4) ℝ) :=
   LieSubalgebra.map (Matrix.reindexLieEquiv (@finSumFinEquiv 1 3)).toLieHom
   (LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)
 
-
 namespace lorentzAlgebra
 
 lemma transpose_eta (A : lorentzAlgebra) :  A.1ᵀ * η  = - η * A.1  := by
-  have h := A.2
-  simp [lorentzAlgebra] at h
-  obtain ⟨B, hB1, hB2⟩ := h
-  simp [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] at hB1
+  obtain ⟨B, hB1, hB2⟩ := A.2
   apply (Equiv.apply_eq_iff_eq
     (Matrix.reindexAlgEquiv ℝ (@finSumFinEquiv 1 3).symm).toEquiv).mp
-  erw [Matrix.reindexAlgEquiv_mul]
-  simp only [Nat.reduceAdd, reindexAlgEquiv_apply, Equiv.symm_symm, AlgEquiv.toEquiv_eq_coe,
-    EquivLike.coe_coe, map_neg, _root_.map_mul]
-  rw [← Matrix.transpose_reindex]
-  have h1 : (reindex finSumFinEquiv.symm finSumFinEquiv.symm) A = B :=
-    (Equiv.apply_eq_iff_eq_symm_apply (reindex finSumFinEquiv.symm finSumFinEquiv.symm)).mpr
-    (id hB2.symm)
-  rw [h1]
+  simp only [Nat.reduceAdd, AlgEquiv.toEquiv_eq_coe, EquivLike.coe_coe, _root_.map_mul,
+    reindexAlgEquiv_apply, ← transpose_reindex, map_neg]
+  rw [(Equiv.apply_eq_iff_eq_symm_apply (reindex finSumFinEquiv.symm finSumFinEquiv.symm)).mpr
+    hB2.symm]
   erw [η_reindex]
-  simpa using hB1
+  simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using hB1
 
 lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 4) (Fin 4) ℝ}
     (h :  Aᵀ * η  = - η * A) : A ∈ lorentzAlgebra := by
-  simp [lorentzAlgebra]
+  simp only [lorentzAlgebra, Nat.reduceAdd, LieSubalgebra.mem_map]
   use (Matrix.reindexLieEquiv (@finSumFinEquiv 1 3)).symm A
   apply And.intro
-  swap
-  change (reindexLieEquiv finSumFinEquiv) _ = _
-  simp only [Nat.reduceAdd, reindexLieEquiv_symm, reindexLieEquiv_apply, reindex_apply,
+  · have h1 := (Equiv.apply_eq_iff_eq
+      (Matrix.reindexAlgEquiv ℝ (@finSumFinEquiv 1 3).symm).toEquiv).mpr h
+    erw [Matrix.reindexAlgEquiv_mul] at h1
+    simp only [Nat.reduceAdd, reindexAlgEquiv_apply, Equiv.symm_symm, AlgEquiv.toEquiv_eq_coe,
+      EquivLike.coe_coe, map_neg, _root_.map_mul] at h1
+    erw [η_reindex] at h1
+    simpa  [Nat.reduceAdd, reindexLieEquiv_symm, reindexLieEquiv_apply,
+      LieAlgebra.Orthogonal.so', mem_skewAdjointMatricesLieSubalgebra,
+      mem_skewAdjointMatricesSubmodule, IsSkewAdjoint, IsAdjointPair, mul_neg] using h1
+  · change (reindexLieEquiv finSumFinEquiv) _ = _
+    simp only [Nat.reduceAdd, reindexLieEquiv_symm, reindexLieEquiv_apply, reindex_apply,
     Equiv.symm_symm, submatrix_submatrix, Equiv.self_comp_symm, submatrix_id_id]
-  simp only [Nat.reduceAdd, reindexLieEquiv_symm, reindexLieEquiv_apply,
-    LieAlgebra.Orthogonal.so', mem_skewAdjointMatricesLieSubalgebra,
-    mem_skewAdjointMatricesSubmodule, IsSkewAdjoint, IsAdjointPair, mul_neg]
-  have h1 :=  (Equiv.apply_eq_iff_eq
-    (Matrix.reindexAlgEquiv ℝ (@finSumFinEquiv 1 3).symm).toEquiv).mpr h
-  erw [Matrix.reindexAlgEquiv_mul] at h1
-  simp only [Nat.reduceAdd, reindexAlgEquiv_apply, Equiv.symm_symm, AlgEquiv.toEquiv_eq_coe,
-    EquivLike.coe_coe, map_neg, _root_.map_mul] at h1
-  erw [η_reindex] at h1
-  simpa using h1
 
 
-lemma mem_iff {A : Matrix (Fin 4) (Fin 4) ℝ} : A ∈ lorentzAlgebra ↔
-    Aᵀ * η  = - η * A := by
-  apply Iff.intro
-  · intro h
-    exact transpose_eta ⟨A, h⟩
-  · intro h
-    exact mem_of_transpose_eta_eq_eta_mul_self h
+lemma mem_iff {A : Matrix (Fin 4) (Fin 4) ℝ} : A ∈ lorentzAlgebra ↔ Aᵀ * η  = - η * A :=
+  Iff.intro (fun h => transpose_eta ⟨A, h⟩) (fun h => mem_of_transpose_eta_eq_eta_mul_self h)
 
 lemma mem_iff'  (A : Matrix (Fin 4) (Fin 4) ℝ) : A ∈ lorentzAlgebra ↔ A  = - η * Aᵀ * η := by
   apply Iff.intro
   intro h
-  rw [mul_assoc, mem_iff.mp h]
-  simp only [neg_mul, mul_neg, ← mul_assoc, η_sq, one_mul, neg_neg]
+  simp_rw [mul_assoc, mem_iff.mp h, neg_mul, mul_neg, ← mul_assoc, η_sq, one_mul, neg_neg]
   intro h
   rw [mem_iff]
   nth_rewrite 2 [h]
@@ -109,7 +99,4 @@ instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra spaceTime where
     rw [mulVec_smul]
 
 
-
-
-
 end spaceTime

HepLean/SpaceTime/LorentzAlgebra/Basis.lean

@@ -0,0 +1,26 @@
+/-
+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
+
+/-- The matrices which form the basis of the Lorentz algebra. -/
+@[simp]
+def σMat (μ ν : Fin 4) : Matrix (Fin 4) (Fin 4) ℝ := fun ρ δ ↦
+  η^[ρ]_[μ] * η_[ν]_[δ] - η_[μ]_[δ] * η^[ρ]_[ν]
+
+end lorentzAlgebra
+
+end spaceTime

HepLean/SpaceTime/Metric.lean

@@ -29,6 +29,27 @@ open TensorProduct
 def η : Matrix (Fin 4) (Fin 4) ℝ := Matrix.reindex finSumFinEquiv finSumFinEquiv
   $ LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ
 
+/-- The metric with lower indices. -/
+notation "η_[" μ "]_[" ν "]" => η μ ν
+
+/-- 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]_[ν]
+
+/-- A matrix with one lower and one upper index. -/
+notation "["Λ"]^[" μ "]_[" ν "]" => (Λ : Matrix (Fin 4) (Fin 4) ℝ) μ ν
+
+/-- A matrix with both lower indices. -/
+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 +123,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