feat: Some Lorentz group lemmas

HepLean/SpaceTime/LorentzGroup/Basic.lean

@@ -184,6 +184,32 @@ lemma transpose_one : @transpose d 1 = 1 := Subtype.eq Matrix.transpose_one
 lemma transpose_mul : transpose (Λ * Λ') = transpose Λ' * transpose Λ :=
   Subtype.eq (Matrix.transpose_mul Λ.1 Λ'.1)
 
+lemma transpose_val : (transpose Λ).1 = Λ.1ᵀ := rfl
+
+lemma transpose_inv : (transpose Λ)⁻¹ = transpose Λ⁻¹ := by
+  refine Subtype.eq ?_
+  rw [transpose_val, coe_inv, transpose_val, coe_inv, Matrix.transpose_nonsing_inv]
+
+lemma comm_minkowskiMatrix : Λ.1 * minkowskiMatrix = minkowskiMatrix * (transpose Λ⁻¹).1 := by
+  conv_rhs => rw [← @mul_minkowskiMatrix_mul_transpose d Λ]
+  rw [← transpose_inv, coe_inv, transpose_val]
+  rw [mul_assoc]
+  have h1 : ((Λ.1)ᵀ * (Λ.1)ᵀ⁻¹) = 1 := by
+    rw [← transpose_val]
+    simp only [subtype_mul_inv]
+  rw [h1]
+  simp
+
+lemma minkowskiMatrix_comm : minkowskiMatrix *  Λ.1  = (transpose Λ⁻¹).1 * minkowskiMatrix := by
+  conv_rhs => rw [← @transpose_mul_minkowskiMatrix_mul_self d Λ]
+  rw [← transpose_inv, coe_inv, transpose_val]
+  rw [← mul_assoc, ← mul_assoc]
+  have h1 : ((Λ.1)ᵀ⁻¹ * (Λ.1)ᵀ) = 1 := by
+    rw [← transpose_val]
+    simp only [subtype_inv_mul]
+  rw [h1]
+  simp
+
 /-!
 
 ## Lorentz group as a topological group

HepLean/SpaceTime/LorentzVector/Real/Contraction.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzVector.Real.Basic
+/-!
+
+# Contraction of Real Lorentz vectors
+
+-/
+
+noncomputable section
+
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+open SpaceTime
+open CategoryTheory.MonoidalCategory
+namespace Lorentz
+
+end Lorentz
+end

HepLean/SpaceTime/LorentzVector/Real/Modules.lean

@@ -74,10 +74,51 @@ def toFin1dℝEquiv : ContrMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
   through the linear equivalence `toFin1dℝEquiv`. -/
 abbrev toFin1dℝ (ψ : ContrMod d) := toFin1dℝEquiv ψ
 
+/-!
+
+## The standard basis.
+
+-/
+
 /-- The standard basis of `ContrℝModule` indexed by `Fin 1 ⊕ Fin d`. -/
 @[simps!]
 def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d) := Basis.ofEquivFun toFin1dℝEquiv
 
+
+@[simp]
+lemma stdBasis_toFin1dℝEquiv_apply_same (μ : Fin 1 ⊕ Fin d) :
+    toFin1dℝEquiv (stdBasis μ) μ = 1 := by
+  simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
+    LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
+  rw [@LinearEquiv.apply_symm_apply]
+  exact Pi.single_eq_same μ 1
+
+lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) :
+    toFin1dℝEquiv (stdBasis μ) ν = 0 := by
+  simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
+    LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
+  rw [@LinearEquiv.apply_symm_apply]
+  exact Pi.single_eq_of_ne' h 1
+
+/-- Decomposition of a contrvariant Lorentz vector into the standard basis. -/
+lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
+  apply toFin1dℝEquiv.injective
+  simp only  [map_sum, _root_.map_smul]
+  funext μ
+  rw [Fintype.sum_apply μ fun c => toFin1dℝEquiv v c • toFin1dℝEquiv (stdBasis c)]
+  change _ = ∑ x : Fin 1 ⊕ Fin d, toFin1dℝEquiv v x • (toFin1dℝEquiv (stdBasis x) μ)
+  rw [Finset.sum_eq_single_of_mem μ (Finset.mem_univ μ)]
+  · simp only [stdBasis_toFin1dℝEquiv_apply_same, smul_eq_mul, mul_one]
+  · intro b _ hbμ
+    rw [stdBasis_toFin1dℝEquiv_apply_ne hbμ]
+    simp only [smul_eq_mul, mul_zero]
+
+/-!
+
+## The representation.
+
+-/
+
 /-- The representation of the Lorentz group acting on `ContrℝModule d`. -/
 def rep : Representation ℝ (LorentzGroup d) (ContrMod d) where
   toFun g := Matrix.toLinAlgEquiv stdBasis g
@@ -85,6 +126,10 @@ def rep : Representation ℝ (LorentzGroup d) (ContrMod d) where
   map_mul' x y := by
     simp only [lorentzGroupIsGroup_mul_coe, _root_.map_mul]
 
+lemma rep_apply_toFin1dℝ (g : LorentzGroup d) (ψ : ContrMod d) :
+    (rep g ψ).toFin1dℝ = g.1 *ᵥ ψ.toFin1dℝ := by
+  rfl
+
 end ContrMod
 
 /-- The module for covariant (up-index) complex Lorentz vectors. -/
@@ -123,20 +168,26 @@ def toFin1dℝEquiv : CoMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
   through the linear equivalence `toFin1dℝEquiv`. -/
 abbrev toFin1dℝ (ψ : CoMod d) := toFin1dℝEquiv ψ
 
+/-!
+
+## The standard basis.
+
+-/
+
 /-- The standard basis of `CoℝModule` indexed by `Fin 1 ⊕ Fin d`. -/
 @[simps!]
 def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (CoMod d) := Basis.ofEquivFun toFin1dℝEquiv
 
 @[simp]
-lemma stdBasis_toFin1dℝEquiv_apply_self (μ : Fin 1 ⊕ Fin d) :
-  toFin1dℝEquiv (stdBasis μ) μ = 1 := by
+lemma stdBasis_toFin1dℝEquiv_apply_same (μ : Fin 1 ⊕ Fin d) :
+    toFin1dℝEquiv (stdBasis μ) μ = 1 := by
   simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
     LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
   rw [@LinearEquiv.apply_symm_apply]
   exact Pi.single_eq_same μ 1
 
 lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) :
-  toFin1dℝEquiv (stdBasis μ) ν = 0 := by
+    toFin1dℝEquiv (stdBasis μ) ν = 0 := by
   simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
     LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
   rw [@LinearEquiv.apply_symm_apply]
@@ -150,11 +201,17 @@ lemma stdBasis_decomp (v : CoMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i :
   rw [Fintype.sum_apply μ fun c => toFin1dℝEquiv v c • toFin1dℝEquiv (stdBasis c)]
   change _ = ∑ x : Fin 1 ⊕ Fin d, toFin1dℝEquiv v x • (toFin1dℝEquiv (stdBasis x) μ)
   rw [Finset.sum_eq_single_of_mem μ (Finset.mem_univ μ)]
-  · simp only [stdBasis_toFin1dℝEquiv_apply_self, smul_eq_mul, mul_one]
+  · simp only [stdBasis_toFin1dℝEquiv_apply_same, smul_eq_mul, mul_one]
   · intro b _ hbμ
     rw [stdBasis_toFin1dℝEquiv_apply_ne hbμ]
     simp only [smul_eq_mul, mul_zero]
 
+/-!
+
+## The representation
+
+-/
+
 /-- The representation of the Lorentz group acting on `CoℝModule d`. -/
 def rep : Representation ℝ (LorentzGroup d) (CoMod d) where
   toFun g := Matrix.toLinAlgEquiv stdBasis (LorentzGroup.transpose g⁻¹)