refactor: Change namespace of SL2C

HepLean/Lorentz/Algebra/Basic.lean

@@ -18,7 +18,6 @@ We define
 
 -/
 
-namespace SpaceTime
 open Matrix
 open TensorProduct
 
@@ -84,5 +83,3 @@ lemma space_comps (Λ : lorentzAlgebra) (i j : Fin 3) :
     (congrArg (fun M ↦ M (Sum.inr i) (Sum.inr j)) $ mem_iff.mp Λ.2).symm
 
 end lorentzAlgebra
-
-end SpaceTime

HepLean/Lorentz/ComplexVector/Basic.lean

@@ -24,7 +24,6 @@ open Matrix
 open MatrixGroups
 open Complex
 open TensorProduct
-open SpaceTime
 
 namespace Lorentz
 

HepLean/Lorentz/ComplexVector/Contraction.lean

@@ -16,7 +16,6 @@ open Matrix
 open MatrixGroups
 open Complex
 open TensorProduct
-open SpaceTime
 open CategoryTheory.MonoidalCategory
 namespace Lorentz
 

HepLean/Lorentz/ComplexVector/Metric.lean

@@ -18,7 +18,6 @@ open Matrix
 open MatrixGroups
 open Complex
 open TensorProduct
-open SpaceTime
 open CategoryTheory.MonoidalCategory
 namespace Lorentz
 

HepLean/Lorentz/ComplexVector/Modules.lean

@@ -92,7 +92,7 @@ def lorentzGroupRep : Representation ℂ (LorentzGroup 3) ContrℂModule where
 /-- The representation of the SL(2, ℂ) on `ContrℂModule` induced by the representation of the
   Lorentz group. -/
 def SL2CRep : Representation ℂ SL(2, ℂ) ContrℂModule :=
-  MonoidHom.comp lorentzGroupRep SpaceTime.SL2C.toLorentzGroup
+  MonoidHom.comp lorentzGroupRep Lorentz.SL2C.toLorentzGroup
 
 end ContrℂModule
 
@@ -156,7 +156,7 @@ def lorentzGroupRep : Representation ℂ (LorentzGroup 3) CoℂModule where
 /-- The representation of the SL(2, ℂ) on `ContrℂModule` induced by the representation of the
   Lorentz group. -/
 def SL2CRep : Representation ℂ SL(2, ℂ) CoℂModule :=
-  MonoidHom.comp lorentzGroupRep SpaceTime.SL2C.toLorentzGroup
+  MonoidHom.comp lorentzGroupRep Lorentz.SL2C.toLorentzGroup
 
 end CoℂModule
 

HepLean/Lorentz/ComplexVector/Two.lean

@@ -16,7 +16,6 @@ open Matrix
 open MatrixGroups
 open Complex
 open TensorProduct
-open SpaceTime
 open CategoryTheory.MonoidalCategory
 namespace Lorentz
 

HepLean/Lorentz/ComplexVector/Unit.lean

@@ -16,7 +16,6 @@ open Matrix
 open MatrixGroups
 open Complex
 open TensorProduct
-open SpaceTime
 open CategoryTheory.MonoidalCategory
 namespace Lorentz
 

HepLean/Lorentz/PauliMatrices/AsTensor.lean

@@ -28,7 +28,6 @@ open Matrix
 open MatrixGroups
 open Complex
 open TensorProduct
-open SpaceTime
 
 /-- The tensor `σ^μ^a^{dot a}` based on the Pauli-matrices as an element of
   `complexContr ⊗ leftHanded ⊗ rightHanded`. -/

HepLean/Lorentz/SL2C/Basic.lean

@@ -15,7 +15,7 @@ import HepLean.Meta.Informal
 The aim of this file is to give the relationship between `SL(2, ℂ)` and the Lorentz group.
 
 -/
-namespace SpaceTime
+namespace Lorentz
 
 open Matrix
 open MatrixGroups
@@ -23,8 +23,6 @@ open Complex
 
 namespace SL2C
 
-open SpaceTime
-
 noncomputable section
 
 /-!
@@ -189,4 +187,4 @@ informal_lemma toRestrictedLorentzGroup where
 end
 end SL2C
 
-end SpaceTime
+end Lorentz

HepLean/Lorentz/Weyl/Basic.lean

@@ -207,7 +207,7 @@ def leftHandedToAlt : leftHanded ⟶ altLeftHanded where
     change AltLeftHandedModule.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ M.1 *ᵥ ψ.val) =
       AltLeftHandedModule.toFin2ℂEquiv.symm ((M.1⁻¹)ᵀ *ᵥ !![0, 1; -1, 0] *ᵥ ψ.val)
     apply congrArg
-    rw [mulVec_mulVec, mulVec_mulVec, SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
+    rw [mulVec_mulVec, mulVec_mulVec, Lorentz.SL2C.inverse_coe, eta_fin_two M.1]
     refine congrFun (congrArg _ ?_) _
     rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
       Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
@@ -238,7 +238,7 @@ def leftHandedAltTo : altLeftHanded ⟶ leftHanded where
     refine LinearMap.ext (fun ψ => ?_)
     change LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ (M.1⁻¹)ᵀ *ᵥ ψ.val) =
       LeftHandedModule.toFin2ℂEquiv.symm (M.1 *ᵥ !![0, -1; 1, 0] *ᵥ ψ.val)
-    rw [EquivLike.apply_eq_iff_eq, mulVec_mulVec, mulVec_mulVec, SpaceTime.SL2C.inverse_coe,
+    rw [EquivLike.apply_eq_iff_eq, mulVec_mulVec, mulVec_mulVec, Lorentz.SL2C.inverse_coe,
       eta_fin_two M.1]
     refine congrFun (congrArg _ ?_) _
     rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,

HepLean/Lorentz/Weyl/Metric.lean

@@ -32,7 +32,7 @@ def metricRaw : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; -1, 0]
 
 lemma comm_metricRaw (M : SL(2,ℂ)) : M.1 * metricRaw = metricRaw * (M.1⁻¹)ᵀ := by
   rw [metricRaw]
-  rw [SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
+  rw [Lorentz.SL2C.inverse_coe, eta_fin_two M.1]
   rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
       Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
   simp only [Fin.isValue, mul_zero, mul_neg, mul_one, zero_add, add_zero, transpose_apply, of_apply,
@@ -42,7 +42,7 @@ lemma comm_metricRaw (M : SL(2,ℂ)) : M.1 * metricRaw = metricRaw * (M.1⁻¹)
 
 lemma metricRaw_comm (M : SL(2,ℂ)) : metricRaw * M.1 = (M.1⁻¹)ᵀ * metricRaw := by
   rw [metricRaw]
-  rw [SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
+  rw [Lorentz.SL2C.inverse_coe, eta_fin_two M.1]
   rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
       Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
   simp only [Fin.isValue, zero_mul, one_mul, zero_add, neg_mul, add_zero, transpose_apply, of_apply,
@@ -53,7 +53,7 @@ lemma metricRaw_comm (M : SL(2,ℂ)) : metricRaw * M.1 = (M.1⁻¹)ᵀ * metricR
 
 lemma star_comm_metricRaw (M : SL(2,ℂ)) : M.1.map star * metricRaw = metricRaw * ((M.1)⁻¹)ᴴ := by
   rw [metricRaw]
-  rw [SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
+  rw [Lorentz.SL2C.inverse_coe, eta_fin_two M.1]
   rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
       eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᴴ]
   rw [eta_fin_two (!![M.1 0 0, M.1 0 1; M.1 1 0, M.1 1 1].map star)]
@@ -61,7 +61,7 @@ lemma star_comm_metricRaw (M : SL(2,ℂ)) : M.1.map star * metricRaw = metricRaw
 
 lemma metricRaw_comm_star (M : SL(2,ℂ)) : metricRaw * M.1.map star = ((M.1)⁻¹)ᴴ * metricRaw := by
   rw [metricRaw]
-  rw [SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
+  rw [Lorentz.SL2C.inverse_coe, eta_fin_two M.1]
   rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
       eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᴴ]
   rw [eta_fin_two (!![M.1 0 0, M.1 0 1; M.1 1 0, M.1 1 1].map star)]

HepLean/Lorentz/Weyl/Two.lean

@@ -713,7 +713,7 @@ lemma leftRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ))
   rw [← h1]
   simp
 
-open SpaceTime
+open Lorentz
 
 lemma altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
     (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :