Physlib.Relativity.Tensors.RealTensor.Vector.Representation

Imports

/-
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 sectionattribute [-simp] Fintype.sum_sum_type

The representation of the Lorentz group on Lorentz vectors.

def rep {d : ℕ} : Representation ℝ (LorentzGroup d) (Vector d) where
  toFun Λ := Matrix.toLinAlgEquiv basis Λ
  map_one' := EmbeddingLike.map_eq_one_iff.mpr rfl
  map_mul' x y := byd:ℕx:↑(LorentzGroup d)y:↑(LorentzGroup d)⊢ (toLinAlgEquiv basis) ↑(x * y) = (toLinAlgEquiv basis) ↑x * (toLinAlgEquiv basis) ↑y simp only [lorentzGroupIsGroup_mul_coe, _root_.map_mul]All goals completed! 🐙

Properties of the representation.

              lemma rep_apply_eq_mulVec (d : ℕ) (Λ : LorentzGroup d) (v : Vector d) :
    rep Λ v = Λ *ᵥ v := byd:ℕΛ:↑(LorentzGroup d)v:Vector d⊢ (rep Λ) v = ↑Λ *ᵥ v rflAll goals completed! 🐙lemma rep_apply_eq_sum (d : ℕ) (Λ : LorentzGroup d) (v : Vector d) (k : Fin 1 ⊕ Fin d) :
    rep Λ v k = ∑ j, Λ.1 k j • v j := rfllemma rep_apply_basis {d} (μ : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) :
    rep Λ (basis μ) = ∑ j, Λ.1 j μ • basis j := byd:ℕμ:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)⊢ (rep Λ) (basis μ) = ∑ j, ↑Λ j μ • basis j
  ext kd:ℕμ:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)k:Fin 1 ⊕ Fin d⊢ (rep Λ) (basis μ) k = (∑ j, ↑Λ j μ • basis j) k
  simp [rep_apply_eq_sum, apply_sum]All goals completed! 🐙lemma rep_toMatrix (d : ℕ) (Λ : LorentzGroup d) :
    LinearMap.toMatrix basis basis (rep Λ) = Λ.1 :=
  (LinearEquiv.eq_symm_apply (LinearMap.toMatrix basis basis)).mp rfllemma rep_injective (d : ℕ) (Λ : LorentzGroup d) : Function.Injective (rep Λ) :=
  fun _ _ h => Matrix.mulVec_injective_of_isUnit (isUnit_of_invertible Λ.1) hlemma rep_surjective (d : ℕ) (Λ : LorentzGroup d) : Function.Surjective (rep Λ) :=
  fun v => ⟨Λ⁻¹ *ᵥ v, byd:ℕΛ:↑(LorentzGroup d)v:Vector d⊢ (rep Λ) ((↑Λ)⁻¹ *ᵥ v) = v simp [rep_apply_eq_mulVec]All goals completed! 🐙⟩lemma rep_bijective (d : ℕ) (Λ : LorentzGroup d) : Function.Bijective (rep Λ) :=
  ⟨rep_injective d Λ, rep_surjective d Λ⟩@[fun_prop]
lemma rep_contDiff (d : ℕ) {n} (Λ : LorentzGroup d) : ContDiff ℝ n (rep Λ) := byd:ℕn:WithTop ℕ∞Λ:↑(LorentzGroup d)⊢ ContDiff ℝ n ⇑(rep Λ)
  refine (contDiff_apply _).mp fun μ => ?_d:ℕn:WithTop ℕ∞Λ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => (rep Λ) x μ
  simp only [rep_apply_eq_sum, smul_eq_mul]d:ℕn:WithTop ℕ∞Λ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => ∑ x_1, ↑Λ μ x_1 * x x_1
  fun_propAll goals completed! 🐙lemma rep_left_injective (d : ℕ) : Function.Injective (rep (d := d)) :=
  fun _ _ h => LorentzGroup.eq_of_mulVec_eq (LinearMap.congr_fun h)