Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial

Imports

/-
Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina, Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.Tensors.RealTensor.Basic
public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic

Tensorial nature of Lorentz vectors

We define the tensorial instance on Lorentz.Vector, and show prove properties related to the Lorentz group action and the basis.

@[expose] public section

Tensorial

The equivalence between the type of indices of a Lorentz vector and Fin 1 ⊕ Fin d.

def indexEquiv {d : ℕ} :
    ComponentIdx (S := (realLorentzTensor d)) ![Color.up] ≃ Fin 1 ⊕ Fin d :=
  ComponentIdx.single (S := realLorentzTensor d) (c := Color.up)

              instance tensorial {d : ℕ} : Tensorial (realLorentzTensor d) ![.up] (Vector d) where
  toTensor := LinearEquiv.symm <|
    Equiv.toLinearEquiv
    ((Tensor.basis (S := (realLorentzTensor d)) ![.up]).repr.toEquiv.trans <|
  Finsupp.equivFunOnFinite.trans <|
  (Equiv.piCongrLeft' _ indexEquiv))
    { map_add := fun x y => byd:ℕx:(realLorentzTensor d).Tensor ![Color.up]y:(realLorentzTensor d).Tensor ![Color.up]⊢ ((Tensor.basis ![Color.up]).repr.toEquiv.trans
      (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
    (x + y) =
  ((Tensor.basis ![Color.up]).repr.toEquiv.trans
        (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
      x +
    ((Tensor.basis ![Color.up]).repr.toEquiv.trans
        (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
      y
        simp [map_add]d:ℕx:(realLorentzTensor d).Tensor ![Color.up]y:(realLorentzTensor d).Tensor ![Color.up]⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)
    (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up]).repr x + (Tensor.basis ![Color.up]).repr y)) =
  (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up]).repr x)) +
    (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up]).repr y))
        rflAll goals completed! 🐙
      map_smul := fun c x => byd:ℕc:ℝx:(realLorentzTensor d).Tensor ![Color.up]⊢ ((Tensor.basis ![Color.up]).repr.toEquiv.trans
      (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
    (c • x) =
  c •
    ((Tensor.basis ![Color.up]).repr.toEquiv.trans
        (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
      x
        simp [_root_.map_smul]d:ℕc:ℝx:(realLorentzTensor d).Tensor ![Color.up]⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite (c • (Tensor.basis ![Color.up]).repr x)) =
  c • (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up]).repr x))
        rflAll goals completed! 🐙}lemma toTensor_symm_apply {d : ℕ} (p : ℝT[d, .up]) :
    (toTensor (self := tensorial)).symm p =
    (Equiv.piCongrLeft' _ indexEquiv <|
    Finsupp.equivFunOnFinite <|
    (Tensor.basis (S := (realLorentzTensor d)) _).repr p) := rfl

lemma toTensor_symm_pure {d : ℕ} (p : Pure (realLorentzTensor d) ![.up]) (i : Fin 1 ⊕ Fin d) :
    (toTensor (self := tensorial)).symm p.toTensor i =
    ((Lorentz.contrBasis d).repr (p 0)) (indexEquiv.symm i 0) := byd:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.up]i:Fin 1 ⊕ Fin d⊢ toTensor.symm p.toTensor i = ((contrBasis d).repr (p 0)) (indexEquiv.symm i 0)
  rw [toTensor_symm_applyd:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.up]i:Fin 1 ⊕ Fin d⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up]).repr p.toTensor)) i =
  ((contrBasis d).repr (p 0)) (indexEquiv.symm i 0)d:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.up]i:Fin 1 ⊕ Fin d⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up]).repr p.toTensor)) i =
  ((contrBasis d).repr (p 0)) (indexEquiv.symm i 0)]d:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.up]i:Fin 1 ⊕ Fin d⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up]).repr p.toTensor)) i =
  ((contrBasis d).repr (p 0)) (indexEquiv.symm i 0)
  simp only [Equiv.piCongrLeft'_apply, Finsupp.equivFunOnFinite_apply, Tensor.basis_repr_pure,
    Pure.component, Finset.univ_unique, Fin.default_eq_zero, Finset.prod_singleton, cons_val_zero]d:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.up]i:Fin 1 ⊕ Fin d⊢ ((contrBasis d).repr (p 0)) (indexEquiv.symm i 0) = ((contrBasis d).repr (p 0)) (indexEquiv.symm i 0)
  rflAll goals completed! 🐙

Basis

              set_option backward.isDefEq.respectTransparency false in
lemma toTensor_symm_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) :
    (toTensor (self := tensorial)).symm (Tensor.basis ![Color.up] (indexEquiv.symm μ)) =
    basis μ := byd:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor.symm ((Tensor.basis ![Color.up]) (indexEquiv.symm μ)) = basis μ
  funext id:ℕμ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ toTensor.symm ((Tensor.basis ![Color.up]) (indexEquiv.symm μ)) i = basis μ i
  simp [Tensor.basis_apply, toTensor_symm_pure, Pure.basisVector, Finsupp.single_apply,
    indexEquiv]All goals completed! 🐙

lemma toTensor_basis_eq_tensor_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) :
    toTensor (basis μ) = Tensor.basis ![Color.up] (indexEquiv.symm μ) := byd:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor (basis μ) = (Tensor.basis ![Color.up]) (indexEquiv.symm μ)
  rw [← toTensor_symm_basisd:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor (toTensor.symm ((Tensor.basis ![Color.up]) (indexEquiv.symm μ))) =
  (Tensor.basis ![Color.up]) (indexEquiv.symm μ)d:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor (toTensor.symm ((Tensor.basis ![Color.up]) (indexEquiv.symm μ))) =
  (Tensor.basis ![Color.up]) (indexEquiv.symm μ)]d:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor (toTensor.symm ((Tensor.basis ![Color.up]) (indexEquiv.symm μ))) =
  (Tensor.basis ![Color.up]) (indexEquiv.symm μ)
  simpAll goals completed! 🐙

lemma basis_eq_map_tensor_basis {d} : basis =
    ((Tensor.basis
    (S := realLorentzTensor d) ![Color.up]).map toTensor.symm).reindex indexEquiv := byd:ℕ⊢ basis = ((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv
  ext μd:ℕμ:Fin 1 ⊕ Fin di✝:Fin 1 ⊕ Fin d⊢ basis μ i✝ = (((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv) μ i✝
  rw [← toTensor_symm_basisd:ℕμ:Fin 1 ⊕ Fin di✝:Fin 1 ⊕ Fin d⊢ toTensor.symm ((Tensor.basis ![Color.up]) (indexEquiv.symm μ)) i✝ =
  (((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv) μ i✝d:ℕμ:Fin 1 ⊕ Fin di✝:Fin 1 ⊕ Fin d⊢ toTensor.symm ((Tensor.basis ![Color.up]) (indexEquiv.symm μ)) i✝ =
  (((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv) μ i✝]d:ℕμ:Fin 1 ⊕ Fin di✝:Fin 1 ⊕ Fin d⊢ toTensor.symm ((Tensor.basis ![Color.up]) (indexEquiv.symm μ)) i✝ =
  (((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv) μ i✝
  simpAll goals completed! 🐙

lemma tensor_basis_map_eq_basis_reindex {d} :
    (Tensor.basis (S := realLorentzTensor d) ![Color.up]).map toTensor.symm =
    basis.reindex indexEquiv.symm := byd:ℕ⊢ (Tensor.basis ![Color.up]).map toTensor.symm = basis.reindex indexEquiv.symm
  rw [basis_eq_map_tensor_basisd:ℕ⊢ (Tensor.basis ![Color.up]).map toTensor.symm =
  (((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv).reindex indexEquiv.symmd:ℕ⊢ (Tensor.basis ![Color.up]).map toTensor.symm =
  (((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv).reindex indexEquiv.symm]d:ℕ⊢ (Tensor.basis ![Color.up]).map toTensor.symm =
  (((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv).reindex indexEquiv.symm
  ext μd:ℕμ:ComponentIdx ![Color.up]i✝:Fin 1 ⊕ Fin d⊢ ((Tensor.basis ![Color.up]).map toTensor.symm) μ i✝ =
  ((((Tensor.basis ![Color.up]).map toTensor.symm).reindex indexEquiv).reindex indexEquiv.symm) μ i✝
  simpAll goals completed! 🐙lemma tensor_basis_repr_toTensor_apply {d : ℕ} (p : Vector d) (μ : ComponentIdx ![Color.up]) :
    (Tensor.basis ![Color.up]).repr (toTensor p) μ =
    p (indexEquiv μ) := byd:ℕp:Vector dμ:ComponentIdx ![Color.up]⊢ ((Tensor.basis ![Color.up]).repr (toTensor p)) μ = p (indexEquiv μ)
  obtain ⟨p, rfl⟩ := toTensor.symm.surjective pd:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]⊢ ((Tensor.basis ![Color.up]).repr (toTensor (toTensor.symm p))) μ = toTensor.symm p (indexEquiv μ)
  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, LinearEquiv.apply_symm_apply]d:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]⊢ ((Tensor.basis ![Color.up]).repr p) μ = toTensor.symm p (indexEquiv μ)
  apply induction_on_pure (t := p)hd:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (p : Tensor.Pure (realLorentzTensor d) ![Color.up]),
  ((Tensor.basis ![Color.up]).repr p.toTensor) μ = toTensor.symm p.toTensor (indexEquiv μ)hsmuld:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (r : ℝ) (t : (realLorentzTensor d).Tensor ![Color.up]),
  ((Tensor.basis ![Color.up]).repr t) μ = toTensor.symm t (indexEquiv μ) →
    ((Tensor.basis ![Color.up]).repr (r • t)) μ = toTensor.symm (r • t) (indexEquiv μ)haddd:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (t1 t2 : (realLorentzTensor d).Tensor ![Color.up]),
  ((Tensor.basis ![Color.up]).repr t1) μ = toTensor.symm t1 (indexEquiv μ) →
    ((Tensor.basis ![Color.up]).repr t2) μ = toTensor.symm t2 (indexEquiv μ) →
      ((Tensor.basis ![Color.up]).repr (t1 + t2)) μ = toTensor.symm (t1 + t2) (indexEquiv μ)
  ·hd:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (p : Tensor.Pure (realLorentzTensor d) ![Color.up]),
  ((Tensor.basis ![Color.up]).repr p.toTensor) μ = toTensor.symm p.toTensor (indexEquiv μ) intro phd:ℕμ:ComponentIdx ![Color.up]p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]⊢ ((Tensor.basis ![Color.up]).repr p.toTensor) μ = toTensor.symm p.toTensor (indexEquiv μ)
    simp [Tensor.basis_repr_pure, toTensor_symm_pure, Pure.component]hd:ℕμ:ComponentIdx ![Color.up]p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]⊢ ((contrBasis d).repr (p 0)) (μ 0) = ((contrBasis d).repr (p 0)) (μ 0)
    rflAll goals completed! 🐙
  ·hsmuld:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (r : ℝ) (t : (realLorentzTensor d).Tensor ![Color.up]),
  ((Tensor.basis ![Color.up]).repr t) μ = toTensor.symm t (indexEquiv μ) →
    ((Tensor.basis ![Color.up]).repr (r • t)) μ = toTensor.symm (r • t) (indexEquiv μ) intro r t hhsmuld:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]r:ℝt:(realLorentzTensor d).Tensor ![Color.up]h:((Tensor.basis ![Color.up]).repr t) μ = toTensor.symm t (indexEquiv μ)⊢ ((Tensor.basis ![Color.up]).repr (r • t)) μ = toTensor.symm (r • t) (indexEquiv μ)
    simp [h]All goals completed! 🐙
  ·haddd:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (t1 t2 : (realLorentzTensor d).Tensor ![Color.up]),
  ((Tensor.basis ![Color.up]).repr t1) μ = toTensor.symm t1 (indexEquiv μ) →
    ((Tensor.basis ![Color.up]).repr t2) μ = toTensor.symm t2 (indexEquiv μ) →
      ((Tensor.basis ![Color.up]).repr (t1 + t2)) μ = toTensor.symm (t1 + t2) (indexEquiv μ) intro t1 t2 h1 h2haddd:ℕμ:ComponentIdx ![Color.up]p:(realLorentzTensor d).Tensor ![Color.up]t1:(realLorentzTensor d).Tensor ![Color.up]t2:(realLorentzTensor d).Tensor ![Color.up]h1:((Tensor.basis ![Color.up]).repr t1) μ = toTensor.symm t1 (indexEquiv μ)h2:((Tensor.basis ![Color.up]).repr t2) μ = toTensor.symm t2 (indexEquiv μ)⊢ ((Tensor.basis ![Color.up]).repr (t1 + t2)) μ = toTensor.symm (t1 + t2) (indexEquiv μ)
    simp [h1, h2]All goals completed! 🐙

The action of the Lorentz group

              

set_option backward.isDefEq.respectTransparency false in
lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : Vector d) :
    (Λ • p) i = ∑ j, Λ.1 i j * p j := byd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:Vector d⊢ (Λ • p) i = ∑ j, ↑Λ i j * p j
  obtain ⟨p, rfl⟩ := toTensor.symm.surjective pd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ (Λ • toTensor.symm p) i = ∑ j, ↑Λ i j * toTensor.symm p j
  rw [smul_toTensor_symmd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ toTensor.symm (Λ • p) i = ∑ j, ↑Λ i j * toTensor.symm p jd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ toTensor.symm (Λ • p) i = ∑ j, ↑Λ i j * toTensor.symm p j]d:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ toTensor.symm (Λ • p) i = ∑ j, ↑Λ i j * toTensor.symm p j
  apply induction_on_pure (t := p)hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (p : Tensor.Pure (realLorentzTensor d) ![Color.up]),
  toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor jhsmuld:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (r : ℝ) (t : (realLorentzTensor d).Tensor ![Color.up]),
  toTensor.symm (Λ • t) i = ∑ j, ↑Λ i j * toTensor.symm t j →
    toTensor.symm (Λ • r • t) i = ∑ j, ↑Λ i j * toTensor.symm (r • t) jhaddd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (t1 t2 : (realLorentzTensor d).Tensor ![Color.up]),
  toTensor.symm (Λ • t1) i = ∑ j, ↑Λ i j * toTensor.symm t1 j →
    toTensor.symm (Λ • t2) i = ∑ j, ↑Λ i j * toTensor.symm t2 j →
      toTensor.symm (Λ • (t1 + t2)) i = ∑ j, ↑Λ i j * toTensor.symm (t1 + t2) j
  ·hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (p : Tensor.Pure (realLorentzTensor d) ![Color.up]),
  toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j intro phd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]⊢ toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j
    have toTensor_symm_pure_val : ∀ (q : Pure (realLorentzTensor d) ![.up]) (j : Fin 1 ⊕ Fin d),
        (toTensor (self := tensorial)).symm q.toTensor j = (q 0).val j := fun q j => byd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]q:Tensor.Pure (realLorentzTensor d) ![Color.up]j:Fin 1 ⊕ Fin d⊢ toTensor.symm q.toTensor j = (q 0).val jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j
      rw [toTensor_symm_pure,d:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]q:Tensor.Pure (realLorentzTensor d) ![Color.up]j:Fin 1 ⊕ Fin d⊢ ((contrBasis d).repr (q 0)) (indexEquiv.symm j 0) = (q 0).val jd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]q:Tensor.Pure (realLorentzTensor d) ![Color.up]j:Fin 1 ⊕ Fin d⊢ (q 0).val (indexEquiv.symm j 0) = (q 0).val jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j contrBasis_repr_applyd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]q:Tensor.Pure (realLorentzTensor d) ![Color.up]j:Fin 1 ⊕ Fin d⊢ (q 0).val (indexEquiv.symm j 0) = (q 0).val jd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]q:Tensor.Pure (realLorentzTensor d) ![Color.up]j:Fin 1 ⊕ Fin d⊢ (q 0).val (indexEquiv.symm j 0) = (q 0).val jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j]d:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]q:Tensor.Pure (realLorentzTensor d) ![Color.up]j:Fin 1 ⊕ Fin d⊢ (q 0).val (indexEquiv.symm j 0) = (q 0).val jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j
      rflhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j
    rw [actionT_purehd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p).toTensor i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p).toTensor i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j]hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ toTensor.symm (Λ • p).toTensor i = ∑ j, ↑Λ i j * toTensor.symm p.toTensor j
    simp only [toTensor_symm_pure_val]hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ ((Λ • p) 0).val i = ∑ x, ↑Λ i x * (p 0).val x
    show (Λ.1 *ᵥ (p 0)).val i = ∑ j, Λ.1 i j * (p 0).val jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ (↑Λ *ᵥ p 0).val i = ∑ j, ↑Λ i j * (p 0).val j
    rw [ContrMod.mulVec_val,hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ (↑Λ *ᵥ (p 0).val) i = ∑ j, ↑Λ i j * (p 0).val jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ (∑ i, MulOpposite.op ((p 0).val i) • (↑Λ)ᵀ i) i = ∑ j, ↑Λ i j * (p 0).val j mulVec_eq_sumhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ (∑ i, MulOpposite.op ((p 0).val i) • (↑Λ)ᵀ i) i = ∑ j, ↑Λ i j * (p 0).val jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ (∑ i, MulOpposite.op ((p 0).val i) • (↑Λ)ᵀ i) i = ∑ j, ↑Λ i j * (p 0).val j]hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.up]p:Tensor.Pure (realLorentzTensor d) ![Color.up]toTensor_symm_pure_val:∀ (q : Tensor.Pure (realLorentzTensor d) ![Color.up]) (j : Fin 1 ⊕ Fin d), toTensor.symm q.toTensor j = (q 0).val j⊢ (∑ i, MulOpposite.op ((p 0).val i) • (↑Λ)ᵀ i) i = ∑ j, ↑Λ i j * (p 0).val j
    simp only [Finset.sum_apply, Pi.smul_apply, transpose_apply,
      MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op]All goals completed! 🐙
  ·hsmuld:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (r : ℝ) (t : (realLorentzTensor d).Tensor ![Color.up]),
  toTensor.symm (Λ • t) i = ∑ j, ↑Λ i j * toTensor.symm t j →
    toTensor.symm (Λ • r • t) i = ∑ j, ↑Λ i j * toTensor.symm (r • t) j intro r t hhsmuld:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]r:ℝt:(realLorentzTensor d).Tensor ![Color.up]h:toTensor.symm (Λ • t) i = ∑ j, ↑Λ i j * toTensor.symm t j⊢ toTensor.symm (Λ • r • t) i = ∑ j, ↑Λ i j * toTensor.symm (r • t) j
    simp only [actionT_smul, _root_.map_smul, apply_smul, h, Finset.mul_sum, mul_left_comm]All goals completed! 🐙
  ·haddd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]⊢ ∀ (t1 t2 : (realLorentzTensor d).Tensor ![Color.up]),
  toTensor.symm (Λ • t1) i = ∑ j, ↑Λ i j * toTensor.symm t1 j →
    toTensor.symm (Λ • t2) i = ∑ j, ↑Λ i j * toTensor.symm t2 j →
      toTensor.symm (Λ • (t1 + t2)) i = ∑ j, ↑Λ i j * toTensor.symm (t1 + t2) j intro t1 t2 h1 h2haddd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.up]t1:(realLorentzTensor d).Tensor ![Color.up]t2:(realLorentzTensor d).Tensor ![Color.up]h1:toTensor.symm (Λ • t1) i = ∑ j, ↑Λ i j * toTensor.symm t1 jh2:toTensor.symm (Λ • t2) i = ∑ j, ↑Λ i j * toTensor.symm t2 j⊢ toTensor.symm (Λ • (t1 + t2)) i = ∑ j, ↑Λ i j * toTensor.symm (t1 + t2) j
    simp only [actionT_add, map_add, apply_add, h1, h2, mul_add, Finset.sum_add_distrib]All goals completed! 🐙

lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : Vector d) :
    Λ • p = Λ.1 *ᵥ p := byd:ℕΛ:↑(LorentzGroup d)p:Vector d⊢ Λ • p = ↑Λ *ᵥ p
  funext id:ℕΛ:↑(LorentzGroup d)p:Vector di:Fin 1 ⊕ Fin d⊢ (Λ • p) i = (↑Λ *ᵥ p) i
  rw [smul_eq_sum,d:ℕΛ:↑(LorentzGroup d)p:Vector di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * p j = (↑Λ *ᵥ p) id:ℕΛ:↑(LorentzGroup d)p:Vector di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * p j = (∑ i, MulOpposite.op (p i) • (↑Λ)ᵀ i) i mulVec_eq_sumd:ℕΛ:↑(LorentzGroup d)p:Vector di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * p j = (∑ i, MulOpposite.op (p i) • (↑Λ)ᵀ i) id:ℕΛ:↑(LorentzGroup d)p:Vector di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * p j = (∑ i, MulOpposite.op (p i) • (↑Λ)ᵀ i) i]d:ℕΛ:↑(LorentzGroup d)p:Vector di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * p j = (∑ i, MulOpposite.op (p i) • (↑Λ)ᵀ i) i
  simp only [op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply, smul_eq_mul,
    mul_comm]All goals completed! 🐙lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) :
    Λ • (p + q) = Λ • p + Λ • q := byd:ℕΛ:↑(LorentzGroup d)p:Vector dq:Vector d⊢ Λ • (p + q) = Λ • p + Λ • q simpAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
@[simp]
lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) :
    Λ • (p - q) = Λ • p - Λ • q := byd:ℕΛ:↑(LorentzGroup d)p:Vector dq:Vector d⊢ Λ • (p - q) = Λ • p - Λ • q
  rw [smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)p:Vector dq:Vector d⊢ ↑Λ *ᵥ (p - q) = Λ • p - Λ • qAll goals completed! 🐙 smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)p:Vector dq:Vector d⊢ ↑Λ *ᵥ (p - q) = ↑Λ *ᵥ p - Λ • qAll goals completed! 🐙 smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)p:Vector dq:Vector d⊢ ↑Λ *ᵥ (p - q) = ↑Λ *ᵥ p - ↑Λ *ᵥ qAll goals completed! 🐙 Matrix.mulVec_subd:ℕΛ:↑(LorentzGroup d)p:Vector dq:Vector d⊢ ↑Λ *ᵥ p - ↑Λ *ᵥ q = ↑Λ *ᵥ p - ↑Λ *ᵥ qAll goals completed! 🐙]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) :
    Λ • (0 : Vector d) = 0 := byd:ℕΛ:↑(LorentzGroup d)⊢ Λ • 0 = 0
  rw [smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)⊢ ↑Λ *ᵥ 0 = 0All goals completed! 🐙 Matrix.mulVec_zerod:ℕΛ:↑(LorentzGroup d)⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : Vector d) :
    Λ • (-p) = - (Λ • p) := byd:ℕΛ:↑(LorentzGroup d)p:Vector d⊢ Λ • -p = -(Λ • p)
  rw [smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)p:Vector d⊢ ↑Λ *ᵥ -p = -(Λ • p)All goals completed! 🐙 smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)p:Vector d⊢ ↑Λ *ᵥ -p = -(↑Λ *ᵥ p)All goals completed! 🐙 Matrix.mulVec_negd:ℕΛ:↑(LorentzGroup d)p:Vector d⊢ -(↑Λ *ᵥ p) = -(↑Λ *ᵥ p)All goals completed! 🐙]All goals completed! 🐙lemma neg_smul {d} (Λ : LorentzGroup d) (p : Vector d) :
    (-Λ) • p = - (Λ • p) := byd:ℕΛ:↑(LorentzGroup d)p:Vector d⊢ -Λ • p = -(Λ • p)
  funext id:ℕΛ:↑(LorentzGroup d)p:Vector di:Fin 1 ⊕ Fin d⊢ (-Λ • p) i = (-(Λ • p)) i
  simp [smul_eq_sum, neg_apply]All goals completed! 🐙lemma _root_.LorentzGroup.eq_of_action_vector_eq {d : ℕ}
    {Λ Λ' : LorentzGroup d} (h : ∀ p : Vector d, Λ • p = Λ' • p) :
    Λ = Λ' := byd:ℕΛ:↑(LorentzGroup d)Λ':↑(LorentzGroup d)h:∀ (p : Vector d), Λ • p = Λ' • p⊢ Λ = Λ'
  apply LorentzGroup.eq_of_mulVec_eqd:ℕΛ:↑(LorentzGroup d)Λ':↑(LorentzGroup d)h:∀ (p : Vector d), Λ • p = Λ' • p⊢ ∀ (x : Fin 1 ⊕ Fin d → ℝ), ↑Λ *ᵥ x = ↑Λ' *ᵥ x
  simp_all [smul_eq_mulVec]All goals completed! 🐙

B. The continuous action of the Lorentz group

The Lorentz action on vectors as a continuous linear map.

def actionCLM {d : ℕ} (Λ : LorentzGroup d) :
    Vector d →L[ℝ] Vector d :=
  LinearMap.toContinuousLinearMap
    { toFun := fun v => Λ • v
      map_add' := smul_add Λ
      map_smul' := fun c v => byd:ℕΛ:↑(LorentzGroup d)c:ℝv:Vector d⊢ Λ • c • v = (RingHom.id ℝ) c • Λ • v
        simp only [RingHom.id_apply]d:ℕΛ:↑(LorentzGroup d)c:ℝv:Vector d⊢ Λ • c • v = c • Λ • v
        funext id:ℕΛ:↑(LorentzGroup d)c:ℝv:Vector di:Fin 1 ⊕ Fin d⊢ (Λ • c • v) i = (c • Λ • v) i
        simp only [smul_eq_sum, apply_smul, Finset.mul_sum, mul_left_comm]All goals completed! 🐙}

              lemma actionCLM_apply {d : ℕ} (Λ : LorentzGroup d) (p : Vector d) :
    actionCLM Λ p = Λ • p := rfllemma actionCLM_injective {d : ℕ} (Λ : LorentzGroup d) :
    Function.Injective (actionCLM Λ) := byd:ℕΛ:↑(LorentzGroup d)⊢ Function.Injective ⇑(actionCLM Λ)
  intro x1 x2d:ℕΛ:↑(LorentzGroup d)x1:Vector dx2:Vector d⊢ (actionCLM Λ) x1 = (actionCLM Λ) x2 → x1 = x2
  simp [actionCLM_apply]All goals completed! 🐙lemma actionCLM_surjective {d : ℕ} (Λ : LorentzGroup d) :
    Function.Surjective (actionCLM Λ) := byd:ℕΛ:↑(LorentzGroup d)⊢ Function.Surjective ⇑(actionCLM Λ)
  intro x1d:ℕΛ:↑(LorentzGroup d)x1:Vector d⊢ ∃ a, (actionCLM Λ) a = x1
  use (actionCLM Λ⁻¹) x1hd:ℕΛ:↑(LorentzGroup d)x1:Vector d⊢ (actionCLM Λ) ((actionCLM Λ⁻¹) x1) = x1
  simp [actionCLM_apply]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
    Λ • basis μ = ∑ ν, Λ.1 ν μ • basis ν := byd:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin d⊢ Λ • basis μ = ∑ ν, ↑Λ ν μ • basis ν
  funext id:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ (Λ • basis μ) i = (∑ ν, ↑Λ ν μ • basis ν) i
  rw [smul_eq_sum,d:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * basis μ j = (∑ ν, ↑Λ ν μ • basis ν) id:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * basis μ j = ∑ c, (↑Λ c μ • basis c) i Fintype.sum_applyd:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * basis μ j = ∑ c, (↑Λ c μ • basis c) id:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * basis μ j = ∑ c, (↑Λ c μ • basis c) i]d:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ i j * basis μ j = ∑ c, (↑Λ c μ • basis c) i
  simp [basis_apply, Finset.sum_ite_eq, Finset.sum_ite_eq']All goals completed! 🐙