feat: Representation on Lorentz Vectors

Physlib.lean

@@ -368,6 +368,7 @@ public import Physlib.Relativity.Tensors.OfInt
 public import Physlib.Relativity.Tensors.Product
 public import Physlib.Relativity.Tensors.RealTensor.Basic
 public import Physlib.Relativity.Tensors.RealTensor.CoVector.Basic
+public import Physlib.Relativity.Tensors.RealTensor.CoVector.Representation
 public import Physlib.Relativity.Tensors.RealTensor.CoVector.Tensorial
 public import Physlib.Relativity.Tensors.RealTensor.Matrix.Pre
 public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic
@@ -379,6 +380,7 @@ public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.Basic
 public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike
 public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike
 public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
+public import Physlib.Relativity.Tensors.RealTensor.Vector.Representation
 public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Basic
 public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Contraction
 public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Modules

Physlib/Relativity/Tensors/RealTensor/Basic.lean

@@ -58,6 +58,10 @@ instance modulesModule (d : ℕ) : ∀ c, Module ℝ (modules d c)
 
 end realLorentzTensor
 
+TODO "Replace Lorentz.ContrMod and Lorentz.CoMod in the definition of realLorentzTensor
+  directly with Lorentz.Vector and Lorentz.Covector, and
+  representations defined on them."
+
 noncomputable section
 open realLorentzTensor in
 /-- The tensor structure for complex Lorentz tensors. -/

Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean

@@ -50,6 +50,12 @@ def equivEuclid (d : ℕ) :
     CoVector d ≃ₗ[ℝ] EuclideanSpace ℝ (Fin 1 ⊕ Fin d) :=
   (WithLp.linearEquiv _ _ _).symm
 
+@[ext]
+lemma eq_of_apply_eq {d : ℕ} {v w : CoVector d} (h : ∀ i, v i = w i) : v = w := by
+  apply (equivEuclid d).injective
+  ext i
+  simpa using h i
+
 instance (d : ℕ) : Norm (CoVector d) where
   norm := fun v => ‖equivEuclid d v‖
 
@@ -116,6 +122,10 @@ lemma apply_add {d : ℕ} (v w : CoVector d) (i : Fin 1 ⊕ Fin d) :
 lemma apply_sub {d : ℕ} (v w : CoVector d) (i : Fin 1 ⊕ Fin d) :
     (v - w) i = v i - w i := by rfl
 
+@[simp]
+lemma apply_sum {d : ℕ} {ι : Type} [Fintype ι] (f : ι → CoVector d) (i : Fin 1 ⊕ Fin d) :
+    (∑ j, f j) i = ∑ j, f j i := Finset.sum_apply i Finset.univ f
+
 @[simp]
 lemma neg_apply {d : ℕ} (v : CoVector d) (i : Fin 1 ⊕ Fin d) :
     (-v) i = - v i := rfl

Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Mathlib.RepresentationTheory.Basic
+public import Physlib.Relativity.LorentzGroup.Basic
+public import Physlib.Relativity.Tensors.RealTensor.CoVector.Basic
+/-!
+
+# Representation of the Lorentz group on Lorentz vectors
+
+In this module we define the representation of the Lorentz group on Lorentz covectors.
+This does not define the MulAction on `Lorentz.CoVector`, which is induced
+by its tensor structure.
+
+-/
+
+@[expose] public section
+
+
+open Module
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+
+noncomputable section
+
+namespace Lorentz
+
+namespace CoVector
+attribute [-simp] Fintype.sum_sum_type
+
+/-- The representation of the Lorentz group on Lorentz vectors. -/
+def rep (d : ℕ) : Representation ℝ (LorentzGroup d) (CoVector d) where
+  toFun g := Matrix.toLinAlgEquiv basis (LorentzGroup.transpose g⁻¹)
+  map_one' := by
+    simp only [inv_one, LorentzGroup.transpose_one, lorentzGroupIsGroup_one_coe, _root_.map_one]
+  map_mul' x y := by
+    simp only [_root_.mul_inv_rev, LorentzGroup.inv_eq_dual, LorentzGroup.transpose_mul,
+      lorentzGroupIsGroup_mul_coe, _root_.map_mul]
+
+/-!
+
+## Properties of the representation.
+
+-/
+
+lemma rep_apply_eq_mulVec (d : ℕ) (Λ : LorentzGroup d) (v : CoVector d) :
+    rep d Λ v = (LorentzGroup.transpose Λ⁻¹) *ᵥ v := by rfl
+
+lemma rep_apply_eq_sum (d : ℕ) (Λ : LorentzGroup d) (v : CoVector d) (k : Fin 1 ⊕ Fin d) :
+    rep d Λ v k = ∑ j, (Λ⁻¹).1 j k • v j := rfl
+
+lemma rep_apply_eq_sum_coe (d : ℕ) (Λ : LorentzGroup d) (v : CoVector d) (k : Fin 1 ⊕ Fin d) :
+    rep d Λ v k = ∑ j, Λ.1⁻¹ j k • v j := by
+  rw [rep_apply_eq_sum, LorentzGroup.coe_inv]
+
+lemma rep_apply_basis {d} (μ : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) :
+    rep d Λ (basis μ) = ∑ j, Λ.1⁻¹ μ j • basis j := by
+  ext k
+  simp [rep_apply_eq_sum_coe, apply_sum]
+
+lemma rep_toMatrix (d : ℕ) (Λ : LorentzGroup d) :
+    LinearMap.toMatrix basis basis (rep d Λ) = Λ.1⁻¹ᵀ := by
+  simp only [rep, MonoidHom.coe_mk, OneHom.coe_mk]
+  rw [← LorentzGroup.coe_inv]
+  exact (LinearEquiv.eq_symm_apply (LinearMap.toMatrix basis basis)).mp rfl
+
+lemma rep_injective (d : ℕ) (Λ : LorentzGroup d) : Function.Injective (rep d Λ) := by
+  intro v1 v2 h
+  rw [rep_apply_eq_mulVec, rep_apply_eq_mulVec] at h
+  exact Matrix.mulVec_injective_of_isUnit (isUnit_of_invertible _) h
+
+lemma rep_surjective (d : ℕ) (Λ : LorentzGroup d) : Function.Surjective (rep d Λ) := by
+  intro v
+  use (LorentzGroup.transpose Λ⁻¹)⁻¹ *ᵥ v
+  rw [rep_apply_eq_mulVec]
+  simp
+
+lemma rep_bijective (d : ℕ) (Λ : LorentzGroup d) : Function.Bijective (rep d Λ) :=
+  ⟨rep_injective d Λ, rep_surjective d Λ⟩
+
+end CoVector
+
+end Lorentz

Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean

@@ -54,6 +54,12 @@ def equivEuclid (d : ℕ) :
 lemma equivEuclid_apply (d : ℕ) (v : Vector d) (i : Fin 1 ⊕ Fin d) :
     equivEuclid d v i = v i := rfl
 
+@[ext]
+lemma eq_of_apply_eq {d : ℕ} {v w : Vector d} (h : ∀ i, v i = w i) : v = w := by
+  apply (equivEuclid d).injective
+  ext i
+  simpa using h i
+
 instance (d : ℕ) : Norm (Vector d) where
   norm := fun v => ‖equivEuclid d v‖
 

Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Mathlib.RepresentationTheory.Basic
+public import Physlib.Relativity.LorentzGroup.Basic
+public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic
+/-!
+
+# Representation of the Lorentz group on Lorentz vectors
+
+In this module we define the representation of the Lorentz group on Lorentz vectors.
+This does not define the MulAction on `Lorentz.Vector`, which is induced
+by its tensor structure.
+
+-/
+
+@[expose] public section
+
+
+open Module
+open Matrix
+open MatrixGroups
+open Complex
+open TensorProduct
+
+noncomputable section
+
+namespace Lorentz
+
+namespace Vector
+attribute [-simp] Fintype.sum_sum_type
+
+/-- The representation of the Lorentz group on Lorentz vectors. -/
+def rep (d : ℕ) : Representation ℝ (LorentzGroup d) (Vector d) where
+  toFun g := Matrix.toLinAlgEquiv basis g
+  map_one' := EmbeddingLike.map_eq_one_iff.mpr rfl
+  map_mul' x y := by simp only [lorentzGroupIsGroup_mul_coe, _root_.map_mul]
+
+/-!
+
+## Properties of the representation.
+
+-/
+
+lemma rep_apply_eq_mulVec (d : ℕ) (Λ : LorentzGroup d) (v : Vector d) :
+    rep d Λ v = Λ *ᵥ v := by rfl
+
+lemma rep_apply_eq_sum (d : ℕ) (Λ : LorentzGroup d) (v : Vector d) (k : Fin 1 ⊕ Fin d) :
+    rep d Λ v k = ∑ j, Λ.1 k j • v j := rfl
+
+lemma rep_apply_basis {d} (μ : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) :
+    rep d Λ (basis μ) = ∑ j, Λ.1 j μ • basis j := by
+  ext k
+  simp [rep_apply_eq_sum, apply_sum]
+
+lemma rep_toMatrix (d : ℕ) (Λ : LorentzGroup d) :
+    LinearMap.toMatrix basis basis (rep d Λ) = Λ.1 := by
+  simp only [rep, MonoidHom.coe_mk, OneHom.coe_mk]
+  exact (LinearEquiv.eq_symm_apply (LinearMap.toMatrix basis basis)).mp rfl
+
+lemma rep_injective (d : ℕ) (Λ : LorentzGroup d) : Function.Injective (rep d Λ) := by
+  intro v1 v2 h
+  rw [rep_apply_eq_mulVec, rep_apply_eq_mulVec] at h
+  exact Matrix.mulVec_injective_of_isUnit (isUnit_of_invertible Λ.1) h
+
+lemma rep_surjective (d : ℕ) (Λ : LorentzGroup d) : Function.Surjective (rep d Λ) := by
+  intro v
+  use Λ⁻¹ *ᵥ v
+  rw [rep_apply_eq_mulVec]
+  simp
+
+lemma rep_bijective (d : ℕ) (Λ : LorentzGroup d) : Function.Bijective (rep d Λ) :=
+  ⟨rep_injective d Λ, rep_surjective d Λ⟩
+
+@[fun_prop]
+lemma rep_contDiff (d : ℕ) {n} (Λ : LorentzGroup d) : ContDiff ℝ n (rep d Λ) := by
+  refine (contDiff_apply ⇑((rep d) Λ)).mp ?_
+  intro μ
+  simp only [rep_apply_eq_sum, smul_eq_mul]
+  fun_prop
+
+lemma rep_left_injective (d : ℕ) : Function.Injective (rep d) := by
+  intro Λ Λ' h
+  apply LorentzGroup.eq_of_mulVec_eq
+  intro v
+  rw [← rep_apply_eq_mulVec, ← rep_apply_eq_mulVec]
+  exact LinearMap.congr_fun h v
+
+end Vector
+
+end Lorentz