Physlib.Relativity.Tensors.RealTensor.CoVector.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.CoVector.Basic
public import Physlib.Relativity.Tensors.RealTensor.Basic
public import Mathlib.Geometry.Manifold.ChartedSpace

Tensorial nature of Lorentz covectors

We define the tensorial instance on Lorentz.coVector, 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.down] ≃ Fin 1 ⊕ Fin d :=
  ComponentIdx.single (S := realLorentzTensor d) (c := Color.down)

              instance tensorial {d : ℕ} : Tensorial (realLorentzTensor d) ![.down] (CoVector d) where
  toTensor := LinearEquiv.symm <|
    Equiv.toLinearEquiv
    ((Tensor.basis (S := (realLorentzTensor d)) ![.down]).repr.toEquiv.trans <|
  Finsupp.equivFunOnFinite.trans <|
  (Equiv.piCongrLeft' _ indexEquiv))
    { map_add := fun x y => byd:ℕx:(realLorentzTensor d).Tensor ![Color.down]y:(realLorentzTensor d).Tensor ![Color.down]⊢ ((Tensor.basis ![Color.down]).repr.toEquiv.trans
      (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
    (x + y) =
  ((Tensor.basis ![Color.down]).repr.toEquiv.trans
        (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
      x +
    ((Tensor.basis ![Color.down]).repr.toEquiv.trans
        (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
      y
        simp [map_add]d:ℕx:(realLorentzTensor d).Tensor ![Color.down]y:(realLorentzTensor d).Tensor ![Color.down]⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)
    (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.down]).repr x + (Tensor.basis ![Color.down]).repr y)) =
  (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.down]).repr x)) +
    (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.down]).repr y))
        rflAll goals completed! 🐙
      map_smul := fun c x => byd:ℕc:ℝx:(realLorentzTensor d).Tensor ![Color.down]⊢ ((Tensor.basis ![Color.down]).repr.toEquiv.trans
      (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
    (c • x) =
  c •
    ((Tensor.basis ![Color.down]).repr.toEquiv.trans
        (Finsupp.equivFunOnFinite.trans (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv)))
      x
        simp [_root_.map_smul]d:ℕc:ℝx:(realLorentzTensor d).Tensor ![Color.down]⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite (c • (Tensor.basis ![Color.down]).repr x)) =
  c • (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.down]).repr x))
        rflAll goals completed! 🐙}lemma toTensor_symm_apply {d : ℕ} (p : ℝT[d, .down]) :
    (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) ![.down]) (i : Fin 1 ⊕ Fin d) :
    (toTensor (self := tensorial)).symm p.toTensor i =
    ((Lorentz.coBasis d).repr (p 0)) (indexEquiv.symm i 0) := byd:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.down]i:Fin 1 ⊕ Fin d⊢ toTensor.symm p.toTensor i = ((coBasis d).repr (p 0)) (indexEquiv.symm i 0)
  rw [toTensor_symm_applyd:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.down]i:Fin 1 ⊕ Fin d⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.down]).repr p.toTensor))
    i =
  ((coBasis d).repr (p 0)) (indexEquiv.symm i 0)d:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.down]i:Fin 1 ⊕ Fin d⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.down]).repr p.toTensor))
    i =
  ((coBasis d).repr (p 0)) (indexEquiv.symm i 0)]d:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.down]i:Fin 1 ⊕ Fin d⊢ (Equiv.piCongrLeft' (fun a => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.down]).repr p.toTensor))
    i =
  ((coBasis 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, Fin.isValue, Finset.prod_singleton,
    cons_val_zero]d:ℕp:Tensor.Pure (realLorentzTensor d) ![Color.down]i:Fin 1 ⊕ Fin d⊢ ((coBasis d).repr (p 0)) (indexEquiv.symm i 0) = ((coBasis 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.down] (indexEquiv.symm μ)) =
    basis μ := byd:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor.symm ((Tensor.basis ![Color.down]) (indexEquiv.symm μ)) = basis μ
  funext id:ℕμ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ toTensor.symm ((Tensor.basis ![Color.down]) (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.down] (indexEquiv.symm μ) := byd:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor (basis μ) = (Tensor.basis ![Color.down]) (indexEquiv.symm μ)
  rw [← toTensor_symm_basisd:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor (toTensor.symm ((Tensor.basis ![Color.down]) (indexEquiv.symm μ))) =
  (Tensor.basis ![Color.down]) (indexEquiv.symm μ)d:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor (toTensor.symm ((Tensor.basis ![Color.down]) (indexEquiv.symm μ))) =
  (Tensor.basis ![Color.down]) (indexEquiv.symm μ)]d:ℕμ:Fin 1 ⊕ Fin d⊢ toTensor (toTensor.symm ((Tensor.basis ![Color.down]) (indexEquiv.symm μ))) =
  (Tensor.basis ![Color.down]) (indexEquiv.symm μ)
  simpAll goals completed! 🐙

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

lemma tensor_basis_map_eq_basis_reindex {d} :
    (Tensor.basis (S := realLorentzTensor d) ![Color.down]).map toTensor.symm =
    basis.reindex indexEquiv.symm := byd:ℕ⊢ (Tensor.basis ![Color.down]).map toTensor.symm = basis.reindex indexEquiv.symm
  rw [basis_eq_map_tensor_basisd:ℕ⊢ (Tensor.basis ![Color.down]).map toTensor.symm =
  (((Tensor.basis ![Color.down]).map toTensor.symm).reindex indexEquiv).reindex indexEquiv.symmd:ℕ⊢ (Tensor.basis ![Color.down]).map toTensor.symm =
  (((Tensor.basis ![Color.down]).map toTensor.symm).reindex indexEquiv).reindex indexEquiv.symm]d:ℕ⊢ (Tensor.basis ![Color.down]).map toTensor.symm =
  (((Tensor.basis ![Color.down]).map toTensor.symm).reindex indexEquiv).reindex indexEquiv.symm
  ext μd:ℕμ:ComponentIdx ![Color.down]i✝:Fin 1 ⊕ Fin d⊢ ((Tensor.basis ![Color.down]).map toTensor.symm) μ i✝ =
  ((((Tensor.basis ![Color.down]).map toTensor.symm).reindex indexEquiv).reindex indexEquiv.symm) μ i✝
  simpAll goals completed! 🐙lemma tensor_basis_repr_toTensor_apply {d : ℕ} (p : CoVector d) (μ : ComponentIdx ![Color.down]) :
    (Tensor.basis ![Color.down]).repr (toTensor p) μ =
    p (indexEquiv μ) := byd:ℕp:CoVector dμ:ComponentIdx ![Color.down]⊢ ((Tensor.basis ![Color.down]).repr (toTensor p)) μ = p (indexEquiv μ)
  obtain ⟨p, rfl⟩ := toTensor.symm.surjective pd:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]⊢ ((Tensor.basis ![Color.down]).repr (toTensor (toTensor.symm p))) μ = toTensor.symm p (indexEquiv μ)
  simp only [LinearEquiv.apply_symm_apply]d:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]⊢ ((Tensor.basis ![Color.down]).repr p) μ = toTensor.symm p (indexEquiv μ)
  apply induction_on_pure (t := p)hd:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (p : Tensor.Pure (realLorentzTensor d) ![Color.down]),
  ((Tensor.basis ![Color.down]).repr p.toTensor) μ = toTensor.symm p.toTensor (indexEquiv μ)hsmuld:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (r : ℝ) (t : (realLorentzTensor d).Tensor ![Color.down]),
  ((Tensor.basis ![Color.down]).repr t) μ = toTensor.symm t (indexEquiv μ) →
    ((Tensor.basis ![Color.down]).repr (r • t)) μ = toTensor.symm (r • t) (indexEquiv μ)haddd:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (t1 t2 : (realLorentzTensor d).Tensor ![Color.down]),
  ((Tensor.basis ![Color.down]).repr t1) μ = toTensor.symm t1 (indexEquiv μ) →
    ((Tensor.basis ![Color.down]).repr t2) μ = toTensor.symm t2 (indexEquiv μ) →
      ((Tensor.basis ![Color.down]).repr (t1 + t2)) μ = toTensor.symm (t1 + t2) (indexEquiv μ)
  ·hd:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (p : Tensor.Pure (realLorentzTensor d) ![Color.down]),
  ((Tensor.basis ![Color.down]).repr p.toTensor) μ = toTensor.symm p.toTensor (indexEquiv μ) intro phd:ℕμ:ComponentIdx ![Color.down]p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ ((Tensor.basis ![Color.down]).repr p.toTensor) μ = toTensor.symm p.toTensor (indexEquiv μ)
    simp only [Tensor.basis_repr_pure, Pure.component, Finset.univ_unique, Fin.default_eq_zero,
      Fin.isValue, Finset.prod_singleton, cons_val_zero, toTensor_symm_pure,
      Equiv.symm_apply_apply]hd:ℕμ:ComponentIdx ![Color.down]p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ ((coBasis d).repr (p 0)) (μ 0) = ((coBasis d).repr (p 0)) (μ 0)
    rflAll goals completed! 🐙
  ·hsmuld:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (r : ℝ) (t : (realLorentzTensor d).Tensor ![Color.down]),
  ((Tensor.basis ![Color.down]).repr t) μ = toTensor.symm t (indexEquiv μ) →
    ((Tensor.basis ![Color.down]).repr (r • t)) μ = toTensor.symm (r • t) (indexEquiv μ) intro r t hhsmuld:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]r:ℝt:(realLorentzTensor d).Tensor ![Color.down]h:((Tensor.basis ![Color.down]).repr t) μ = toTensor.symm t (indexEquiv μ)⊢ ((Tensor.basis ![Color.down]).repr (r • t)) μ = toTensor.symm (r • t) (indexEquiv μ)
    simp [h]All goals completed! 🐙
  ·haddd:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (t1 t2 : (realLorentzTensor d).Tensor ![Color.down]),
  ((Tensor.basis ![Color.down]).repr t1) μ = toTensor.symm t1 (indexEquiv μ) →
    ((Tensor.basis ![Color.down]).repr t2) μ = toTensor.symm t2 (indexEquiv μ) →
      ((Tensor.basis ![Color.down]).repr (t1 + t2)) μ = toTensor.symm (t1 + t2) (indexEquiv μ) intro t1 t2 h1 h2haddd:ℕμ:ComponentIdx ![Color.down]p:(realLorentzTensor d).Tensor ![Color.down]t1:(realLorentzTensor d).Tensor ![Color.down]t2:(realLorentzTensor d).Tensor ![Color.down]h1:((Tensor.basis ![Color.down]).repr t1) μ = toTensor.symm t1 (indexEquiv μ)h2:((Tensor.basis ![Color.down]).repr t2) μ = toTensor.symm t2 (indexEquiv μ)⊢ ((Tensor.basis ![Color.down]).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 : CoVector d) :
    (Λ • p) i = ∑ j, Λ⁻¹.1 j i * p j := byd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:CoVector d⊢ (Λ • p) i = ∑ j, ↑Λ⁻¹ j i * p j
  obtain ⟨p, rfl⟩ := toTensor.symm.surjective pd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ (Λ • toTensor.symm p) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p j
  rw [smul_toTensor_symmd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ toTensor.symm (Λ • p) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p jd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ toTensor.symm (Λ • p) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p j]d:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ toTensor.symm (Λ • p) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p j
  apply induction_on_pure (t := p)hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (p : Tensor.Pure (realLorentzTensor d) ![Color.down]),
  toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor jhsmuld:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (r : ℝ) (t : (realLorentzTensor d).Tensor ![Color.down]),
  toTensor.symm (Λ • t) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t j →
    toTensor.symm (Λ • r • t) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm (r • t) jhaddd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (t1 t2 : (realLorentzTensor d).Tensor ![Color.down]),
  toTensor.symm (Λ • t1) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t1 j →
    toTensor.symm (Λ • t2) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t2 j →
      toTensor.symm (Λ • (t1 + t2)) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm (t1 + t2) j
  ·hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (p : Tensor.Pure (realLorentzTensor d) ![Color.down]),
  toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j intro phd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ toTensor.symm (Λ • p.toTensor) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j
    rw [actionT_pure,hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ toTensor.symm (Λ • p).toTensor i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ ((coBasis d).repr ((Λ • p) 0)) (indexEquiv.symm i 0) = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j toTensor_symm_purehd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ ((coBasis d).repr ((Λ • p) 0)) (indexEquiv.symm i 0) = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ ((coBasis d).repr ((Λ • p) 0)) (indexEquiv.symm i 0) = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j]hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ ((coBasis d).repr ((Λ • p) 0)) (indexEquiv.symm i 0) = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j
    conv_lhs =>
      enter [1, 2]d:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]| (Λ • p) 0
      change (LorentzGroup.transpose Λ⁻¹) *ᵥ (p 0)d:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]| ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ p 0
    rw [coBasis_repr_applyhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ (↑(LorentzGroup.transpose Λ⁻¹) *ᵥ p 0).val (indexEquiv.symm i 0) = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ (↑(LorentzGroup.transpose Λ⁻¹) *ᵥ p 0).val (indexEquiv.symm i 0) = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j]hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ (↑(LorentzGroup.transpose Λ⁻¹) *ᵥ p 0).val (indexEquiv.symm i 0) = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j
    conv_lhs => simp [indexEquiv]d:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]| (↑(LorentzGroup.transpose Λ⁻¹) *ᵥ (p 0).val) i
    rw [mulVec_eq_sumhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ (∑ i, MulOpposite.op ((p 0).val i) • (↑(LorentzGroup.transpose Λ⁻¹))ᵀ i) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor jhd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ (∑ i, MulOpposite.op ((p 0).val i) • (↑(LorentzGroup.transpose Λ⁻¹))ᵀ i) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j]hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ (∑ i, MulOpposite.op ((p 0).val i) • (↑(LorentzGroup.transpose Λ⁻¹))ᵀ i) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm p.toTensor j
    simp only [Finset.sum_apply, Pi.smul_apply, transpose_apply, MulOpposite.smul_eq_mul_unop,
      MulOpposite.unop_op, toTensor_symm_pure, coBasis_repr_apply]hd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p✝:(realLorentzTensor d).Tensor ![Color.down]p:Tensor.Pure (realLorentzTensor d) ![Color.down]⊢ ∑ x, ↑(LorentzGroup.transpose Λ⁻¹) i x * (p 0).val x = ∑ x, ↑Λ⁻¹ x i * (p 0).val (indexEquiv.symm x 0)
    rflAll goals completed! 🐙
  ·hsmuld:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]⊢ ∀ (r : ℝ) (t : (realLorentzTensor d).Tensor ![Color.down]),
  toTensor.symm (Λ • t) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t j →
    toTensor.symm (Λ • r • t) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm (r • t) j intro r t hhsmuld:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]r:ℝt:(realLorentzTensor d).Tensor ![Color.down]h:toTensor.symm (Λ • t) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t j⊢ toTensor.symm (Λ • r • t) i = ∑ j, ↑Λ⁻¹ j i * 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.down]⊢ ∀ (t1 t2 : (realLorentzTensor d).Tensor ![Color.down]),
  toTensor.symm (Λ • t1) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t1 j →
    toTensor.symm (Λ • t2) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t2 j →
      toTensor.symm (Λ • (t1 + t2)) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm (t1 + t2) j intro t1 t2 h1 h2haddd:ℕi:Fin 1 ⊕ Fin dΛ:↑(LorentzGroup d)p:(realLorentzTensor d).Tensor ![Color.down]t1:(realLorentzTensor d).Tensor ![Color.down]t2:(realLorentzTensor d).Tensor ![Color.down]h1:toTensor.symm (Λ • t1) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t1 jh2:toTensor.symm (Λ • t2) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm t2 j⊢ toTensor.symm (Λ • (t1 + t2)) i = ∑ j, ↑Λ⁻¹ j i * toTensor.symm (t1 + t2) j
    simp only [actionT_add, map_add, h1, h2, apply_add, mul_add, Finset.sum_add_distrib]All goals completed! 🐙

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

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

set_option backward.isDefEq.respectTransparency false in
lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) :
    Λ • (0 : CoVector d) = 0 := byd:ℕΛ:↑(LorentzGroup d)⊢ Λ • 0 = 0
  rw [smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)⊢ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ 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 : CoVector d) :
    Λ • (-p) = - (Λ • p) := byd:ℕΛ:↑(LorentzGroup d)p:CoVector d⊢ Λ • -p = -(Λ • p)
  rw [smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)p:CoVector d⊢ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ -p = -(Λ • p)All goals completed! 🐙 smul_eq_mulVec,d:ℕΛ:↑(LorentzGroup d)p:CoVector d⊢ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ -p = -(↑(LorentzGroup.transpose Λ⁻¹) *ᵥ p)All goals completed! 🐙 Matrix.mulVec_negd:ℕΛ:↑(LorentzGroup d)p:CoVector d⊢ -(↑(LorentzGroup.transpose Λ⁻¹) *ᵥ p) = -(↑(LorentzGroup.transpose Λ⁻¹) *ᵥ p)All goals completed! 🐙]All goals completed! 🐙

The Lorentz action on vectors as a continuous linear map.

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

lemma actionCLM_apply {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) :
    actionCLM Λ p = Λ • p := rfl



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, ↑Λ⁻¹ j i * basis μ j = (∑ ν, ↑Λ⁻¹ μ ν • basis ν) id:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ⁻¹ j i * basis μ j = ∑ c, (↑Λ⁻¹ μ c • basis c) i Fintype.sum_applyd:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ⁻¹ j i * basis μ j = ∑ c, (↑Λ⁻¹ μ c • basis c) id:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ⁻¹ j i * basis μ j = ∑ c, (↑Λ⁻¹ μ c • basis c) i]d:ℕΛ:↑(LorentzGroup d)μ:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ ∑ j, ↑Λ⁻¹ j i * basis μ j = ∑ c, (↑Λ⁻¹ μ c • basis c) i
  simp only [apply_smul, basis_apply, mul_ite, mul_one, mul_zero,
    Finset.sum_ite_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte]All goals completed! 🐙