Physlib.Relativity.Tensors.RealTensor.CoVector.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.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 sectionattribute [-simp] Fintype.sum_sum_type

The representation of the Lorentz group on Lorentz vectors.

def rep {d : ℕ} : Representation ℝ (LorentzGroup d) (CoVector d) where
  toFun Λ := Matrix.toLinAlgEquiv basis (LorentzGroup.transpose Λ⁻¹)
  map_one' := byd:ℕ⊢ (toLinAlgEquiv basis) ↑(LorentzGroup.transpose 1⁻¹) = 1
    simp only [inv_one, LorentzGroup.transpose_one, lorentzGroupIsGroup_one_coe, _root_.map_one]All goals completed! 🐙
  map_mul' x y := byd:ℕx:↑(LorentzGroup d)y:↑(LorentzGroup d)⊢ (toLinAlgEquiv basis) ↑(LorentzGroup.transpose (x * y)⁻¹) =
  (toLinAlgEquiv basis) ↑(LorentzGroup.transpose x⁻¹) * (toLinAlgEquiv basis) ↑(LorentzGroup.transpose y⁻¹)
    simp only [_root_.mul_inv_rev, LorentzGroup.inv_eq_dual, LorentzGroup.transpose_mul,
      lorentzGroupIsGroup_mul_coe, _root_.map_mul]All goals completed! 🐙

Properties of the representation.

              lemma rep_apply_eq_mulVec (d : ℕ) (Λ : LorentzGroup d) (v : CoVector d) :
    rep Λ v = (LorentzGroup.transpose Λ⁻¹) *ᵥ v := byd:ℕΛ:↑(LorentzGroup d)v:CoVector d⊢ (rep Λ) v = ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v rflAll goals completed! 🐙lemma rep_apply_eq_sum (d : ℕ) (Λ : LorentzGroup d) (v : CoVector d) (k : Fin 1 ⊕ Fin d) :
    rep Λ 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 Λ v k = ∑ j, Λ.1⁻¹ j k • v j := byd:ℕΛ:↑(LorentzGroup d)v:CoVector dk:Fin 1 ⊕ Fin d⊢ (rep Λ) v k = ∑ j, (↑Λ)⁻¹ j k • v j
  rw [rep_apply_eq_sum,d:ℕΛ:↑(LorentzGroup d)v:CoVector dk:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ⁻¹ j k • v j = ∑ j, (↑Λ)⁻¹ j k • v jAll goals completed! 🐙 LorentzGroup.coe_invd:ℕΛ:↑(LorentzGroup d)v:CoVector dk:Fin 1 ⊕ Fin d⊢ ∑ j, (↑Λ)⁻¹ j k • v j = ∑ j, (↑Λ)⁻¹ j k • v jAll goals completed! 🐙]All goals completed! 🐙lemma 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_coe, apply_sum]All goals completed! 🐙

lemma rep_toMatrix (d : ℕ) (Λ : LorentzGroup d) :
    LinearMap.toMatrix basis basis (rep Λ) = Λ.1⁻¹ᵀ := byd:ℕΛ:↑(LorentzGroup d)⊢ (LinearMap.toMatrix basis basis) (rep Λ) = (↑Λ)⁻¹ᵀ
  simp only [rep, MonoidHom.coe_mk, OneHom.coe_mk]d:ℕΛ:↑(LorentzGroup d)⊢ (LinearMap.toMatrix basis basis) ((toLinAlgEquiv basis) ↑(LorentzGroup.transpose Λ⁻¹)) = (↑Λ)⁻¹ᵀ
  rw [← LorentzGroup.coe_invd:ℕΛ:↑(LorentzGroup d)⊢ (LinearMap.toMatrix basis basis) ((toLinAlgEquiv basis) ↑(LorentzGroup.transpose Λ⁻¹)) = (↑Λ⁻¹)ᵀd:ℕΛ:↑(LorentzGroup d)⊢ (LinearMap.toMatrix basis basis) ((toLinAlgEquiv basis) ↑(LorentzGroup.transpose Λ⁻¹)) = (↑Λ⁻¹)ᵀ]d:ℕΛ:↑(LorentzGroup d)⊢ (LinearMap.toMatrix basis basis) ((toLinAlgEquiv basis) ↑(LorentzGroup.transpose Λ⁻¹)) = (↑Λ⁻¹)ᵀ
  exact (LinearEquiv.eq_symm_apply (LinearMap.toMatrix basis basis)).mp rflAll goals completed! 🐙

lemma rep_injective (d : ℕ) (Λ : LorentzGroup d) : Function.Injective (rep Λ) := byd:ℕΛ:↑(LorentzGroup d)⊢ Function.Injective ⇑(rep Λ)
  intro v1 v2 hd:ℕΛ:↑(LorentzGroup d)v1:CoVector dv2:CoVector dh:(rep Λ) v1 = (rep Λ) v2⊢ v1 = v2
  rw [rep_apply_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)v1:CoVector dv2:CoVector dh:↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v1 = (rep Λ) v2⊢ v1 = v2d:ℕΛ:↑(LorentzGroup d)v1:CoVector dv2:CoVector dh:↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v1 = ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v2⊢ v1 = v2 rep_apply_eq_mulVecd:ℕΛ:↑(LorentzGroup d)v1:CoVector dv2:CoVector dh:↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v1 = ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v2⊢ v1 = v2d:ℕΛ:↑(LorentzGroup d)v1:CoVector dv2:CoVector dh:↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v1 = ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v2⊢ v1 = v2] at hd:ℕΛ:↑(LorentzGroup d)v1:CoVector dv2:CoVector dh:↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v1 = ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ v2⊢ v1 = v2
  exact Matrix.mulVec_injective_of_isUnit (isUnit_of_invertible _) hAll goals completed! 🐙

lemma rep_surjective (d : ℕ) (Λ : LorentzGroup d) : Function.Surjective (rep Λ) := byd:ℕΛ:↑(LorentzGroup d)⊢ Function.Surjective ⇑(rep Λ)
  intro vd:ℕΛ:↑(LorentzGroup d)v:CoVector d⊢ ∃ a, (rep Λ) a = v
  use (LorentzGroup.transpose Λ) *ᵥ vhd:ℕΛ:↑(LorentzGroup d)v:CoVector d⊢ (rep Λ) (↑(LorentzGroup.transpose Λ) *ᵥ v) = v
  rw [rep_apply_eq_mulVechd:ℕΛ:↑(LorentzGroup d)v:CoVector d⊢ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ ↑(LorentzGroup.transpose Λ) *ᵥ v = vhd:ℕΛ:↑(LorentzGroup d)v:CoVector d⊢ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ ↑(LorentzGroup.transpose Λ) *ᵥ v = v]hd:ℕΛ:↑(LorentzGroup d)v:CoVector d⊢ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ ↑(LorentzGroup.transpose Λ) *ᵥ v = v
  simp [← LorentzGroup.transpose_inv, LorentzGroup.coe_inv]All goals completed! 🐙lemma rep_bijective (d : ℕ) (Λ : LorentzGroup d) : Function.Bijective (rep Λ) :=
  ⟨rep_injective d Λ, rep_surjective d Λ⟩