From 804ddea3561b9513daec67e7877b9f299e63d409 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 19 Jun 2026 15:28:25 +0100 Subject: [PATCH 1/2] feat: Representation on Lorentz Vectors --- Physlib.lean | 1 + .../Relativity/Tensors/RealTensor/Basic.lean | 4 + .../Tensors/RealTensor/Vector/Basic.lean | 6 ++ .../RealTensor/Vector/Representation.lean | 95 +++++++++++++++++++ 4 files changed, 106 insertions(+) create mode 100644 Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean diff --git a/Physlib.lean b/Physlib.lean index 2e4dc7a14..cdcb1ac03 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -379,6 +379,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 diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean index 1ae166f48..42a195154 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean +++ b/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. -/ diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean index e81e382d1..59fc7a4f3 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean +++ b/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‖ diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean new file mode 100644 index 000000000..c5bd15d73 --- /dev/null +++ b/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 From 3092745a10d2ab97c0a4c448681a79f2a11cf375 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 19 Jun 2026 15:41:29 +0100 Subject: [PATCH 2/2] feat: Add representation for CoVector --- Physlib.lean | 1 + .../Tensors/RealTensor/CoVector/Basic.lean | 10 +++ .../RealTensor/CoVector/Representation.lean | 89 +++++++++++++++++++ 3 files changed, 100 insertions(+) create mode 100644 Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean diff --git a/Physlib.lean b/Physlib.lean index cdcb1ac03..ab4f3ecc6 100644 --- a/Physlib.lean +++ b/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 diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean index ba2ae034a..83c685320 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean +++ b/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 diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean new file mode 100644 index 000000000..3c110704b --- /dev/null +++ b/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