Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Basic

Imports

/-
Copyright (c) 2024 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 Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Modules
public import Mathlib.RepresentationTheory.Rep.Basic

Real Lorentz vectors

We define real Lorentz vectors in as representations of the Lorentz group.

@[expose] public section

The standard basis of contravariant Lorentz vectors.

def contrBasis (d : ℕ := 3) : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d) :=
  Basis.ofEquivFun ContrMod.toFin1dℝEquiv

              

@[simp]
lemma contrBasis_ρ_apply {d : ℕ} (M : LorentzGroup d) (i j : Fin 1 ⊕ Fin d) :
    (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i j =
    M.1 i j := byd:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i j = ↑M i j
  rw [LinearMap.toMatrix_applyd:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ((contrBasis d).repr ((ContrMod.rep M) ((contrBasis d) j))) i = ↑M i jd:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ((contrBasis d).repr ((ContrMod.rep M) ((contrBasis d) j))) i = ↑M i j]d:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ((contrBasis d).repr ((ContrMod.rep M) ((contrBasis d) j))) i = ↑M i j
  simp only [contrBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]d:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ContrMod.toFin1dℝEquiv ((ContrMod.rep M) (ContrMod.toFin1dℝEquiv.symm (Pi.single j 1))) i = ↑M i j
  change (M.1 *ᵥ (Pi.single j 1)) i = _d:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (↑M *ᵥ Pi.single j 1) i = ↑M i j
  simpAll goals completed! 🐙@[simp]
lemma contrBasis_toFin1dℝ {d : ℕ} (i : Fin 1 ⊕ Fin d) :
    (contrBasis d i).toFin1dℝ = Pi.single i 1 := byd:ℕi:Fin 1 ⊕ Fin d⊢ ((contrBasis d) i).toFin1dℝ = Pi.single i 1
  simp only [ContrMod.toFin1dℝ, contrBasis, Basis.coe_ofEquivFun]d:ℕi:Fin 1 ⊕ Fin d⊢ ContrMod.toFin1dℝEquiv (ContrMod.toFin1dℝEquiv.symm (Pi.single i 1)) = Pi.single i 1
  rflAll goals completed! 🐙lemma contrBasis_repr_apply {d : ℕ} (p : ContrMod d) (i : Fin 1 ⊕ Fin d) :
    (contrBasis d).repr p i = p.val i := byd:ℕp:ContrMod di:Fin 1 ⊕ Fin d⊢ ((contrBasis d).repr p) i = p.val i
  simp only [contrBasis, Basis.ofEquivFun_repr_apply]d:ℕp:ContrMod di:Fin 1 ⊕ Fin d⊢ ContrMod.toFin1dℝEquiv p i = p.val i
  rflAll goals completed! 🐙

The standard basis of contravariant Lorentz vectors indexed by Fin (1 + d).

def contrBasisFin (d : ℕ := 3) : Basis (Fin (1 + d)) ℝ (ContrMod d) :=
  Basis.reindex (contrBasis d) finSumFinEquiv

              @[simp]
lemma contrBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) :
    (contrBasisFin d i).toFin1dℝ = Pi.single (finSumFinEquiv.symm i) 1 := byd:ℕi:Fin (1 + d)⊢ ((contrBasisFin d) i).toFin1dℝ = Pi.single (finSumFinEquiv.symm i) 1
  simp only [contrBasisFin, Basis.reindex_apply, contrBasis_toFin1dℝ]All goals completed! 🐙lemma contrBasisFin_repr_apply {d : ℕ} (p : ContrMod d) (i : Fin (1 + d)) :
    (contrBasisFin d).repr p i = p.val (finSumFinEquiv.symm i) := byd:ℕp:ContrMod di:Fin (1 + d)⊢ ((contrBasisFin d).repr p) i = p.val (finSumFinEquiv.symm i) rflAll goals completed! 🐙lemma continuous_contr {T : Type} [TopologicalSpace T] (f : T → ContrMod d)
    (h : Continuous (fun i => (f i).toFin1dℝ)) : Continuous f := byd:ℕT:Typeinst✝:TopologicalSpace Tf:T → ContrMod dh:Continuous fun i => (f i).toFin1dℝ⊢ Continuous f
  exact continuous_induced_rng.mpr hAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma contr_continuous {T : Type} [TopologicalSpace T] (f : ContrMod d → T)
    (h : Continuous (f ∘ (@ContrMod.toFin1dℝEquiv d).symm)) : Continuous f := byd:ℕT:Typeinst✝:TopologicalSpace Tf:ContrMod d → Th:Continuous (f ∘ ⇑ContrMod.toFin1dℝEquiv.symm)⊢ Continuous f
  let x := Equiv.toHomeomorphOfIsInducing (@ContrMod.toFin1dℝEquiv d).toEquiv
    ContrMod.toFin1dℝEquiv_isInducingd:ℕT:Typeinst✝:TopologicalSpace Tf:ContrMod d → Th:Continuous (f ∘ ⇑ContrMod.toFin1dℝEquiv.symm)x:ContrMod d ≃ₜ (Fin 1 ⊕ Fin d → ℝ) := ContrMod.toFin1dℝEquiv.toEquiv.toHomeomorphOfIsInducing ⋯⊢ Continuous f
  rw [← Homeomorph.comp_continuous_iff' x.symmd:ℕT:Typeinst✝:TopologicalSpace Tf:ContrMod d → Th:Continuous (f ∘ ⇑ContrMod.toFin1dℝEquiv.symm)x:ContrMod d ≃ₜ (Fin 1 ⊕ Fin d → ℝ) := ContrMod.toFin1dℝEquiv.toEquiv.toHomeomorphOfIsInducing ⋯⊢ Continuous (f ∘ ⇑x.symm)d:ℕT:Typeinst✝:TopologicalSpace Tf:ContrMod d → Th:Continuous (f ∘ ⇑ContrMod.toFin1dℝEquiv.symm)x:ContrMod d ≃ₜ (Fin 1 ⊕ Fin d → ℝ) := ContrMod.toFin1dℝEquiv.toEquiv.toHomeomorphOfIsInducing ⋯⊢ Continuous (f ∘ ⇑x.symm)]d:ℕT:Typeinst✝:TopologicalSpace Tf:ContrMod d → Th:Continuous (f ∘ ⇑ContrMod.toFin1dℝEquiv.symm)x:ContrMod d ≃ₜ (Fin 1 ⊕ Fin d → ℝ) := ContrMod.toFin1dℝEquiv.toEquiv.toHomeomorphOfIsInducing ⋯⊢ Continuous (f ∘ ⇑x.symm)
  exact hAll goals completed! 🐙

The standard basis of contravariant Lorentz vectors.

def coBasis (d : ℕ := 3) : Basis (Fin 1 ⊕ Fin d) ℝ (CoMod d) :=
  Basis.ofEquivFun CoMod.toFin1dℝEquiv

              

@[simp]
lemma coBasis_ρ_apply {d : ℕ} (M : LorentzGroup d) (i j : Fin 1 ⊕ Fin d) :
    (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i j =
    M⁻¹ᵀ i j := byd:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i j = (↑M)⁻¹ᵀ i j
  rw [LinearMap.toMatrix_applyd:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ((coBasis d).repr ((CoMod.rep M) ((coBasis d) j))) i = (↑M)⁻¹ᵀ i jd:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ((coBasis d).repr ((CoMod.rep M) ((coBasis d) j))) i = (↑M)⁻¹ᵀ i j]d:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ ((coBasis d).repr ((CoMod.rep M) ((coBasis d) j))) i = (↑M)⁻¹ᵀ i j
  simp only [coBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]d:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ CoMod.toFin1dℝEquiv ((CoMod.rep M) (CoMod.toFin1dℝEquiv.symm (Pi.single j 1))) i = (↑M)⁻¹ j i
  change (_ *ᵥ (Pi.single j 1)) i = _d:ℕM:↑(LorentzGroup d)i:Fin 1 ⊕ Fin dj:Fin 1 ⊕ Fin d⊢ (↑(LorentzGroup.transpose M⁻¹) *ᵥ Pi.single j 1) i = (↑M)⁻¹ j i
  simp [LorentzGroup.transpose, ← LorentzGroup.coe_inv]All goals completed! 🐙lemma coBasis_repr_apply {d : ℕ} (p : CoMod d) (i : Fin 1 ⊕ Fin d) :
    (coBasis d).repr p i = p.val i := byd:ℕp:CoMod di:Fin 1 ⊕ Fin d⊢ ((coBasis d).repr p) i = p.val i
  simp only [coBasis, Basis.ofEquivFun_repr_apply]d:ℕp:CoMod di:Fin 1 ⊕ Fin d⊢ CoMod.toFin1dℝEquiv p i = p.val i
  rflAll goals completed! 🐙@[simp]
lemma coBasis_toFin1dℝ {d : ℕ} (i : Fin 1 ⊕ Fin d) :
    (coBasis d i).toFin1dℝ = Pi.single i 1 := byd:ℕi:Fin 1 ⊕ Fin d⊢ ((coBasis d) i).toFin1dℝ = Pi.single i 1
  simp only [coBasis, Basis.coe_ofEquivFun]d:ℕi:Fin 1 ⊕ Fin d⊢ (CoMod.toFin1dℝEquiv.symm (Pi.single i 1)).toFin1dℝ = Pi.single i 1
  rflAll goals completed! 🐙

The standard basis of covariant Lorentz vectors indexed by Fin (1 + d).

def coBasisFin (d : ℕ := 3) : Basis (Fin (1 + d)) ℝ (CoMod d) :=
  Basis.reindex (coBasis d) finSumFinEquiv

@[simp]
lemma coBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) :
    (coBasisFin d i).toFin1dℝ = Pi.single (finSumFinEquiv.symm i) 1 := byd:ℕi:Fin (1 + d)⊢ ((coBasisFin d) i).toFin1dℝ = Pi.single (finSumFinEquiv.symm i) 1
  simp only [coBasisFin, Basis.reindex_apply, coBasis_toFin1dℝ]All goals completed! 🐙

lemma coBasisFin_repr_apply {d : ℕ} (p : CoMod d) (i : Fin (1 + d)) :
    (coBasisFin d).repr p i = p.val (finSumFinEquiv.symm i) := byd:ℕp:CoMod di:Fin (1 + d)⊢ ((coBasisFin d).repr p) i = p.val (finSumFinEquiv.symm i) rflAll goals completed! 🐙

Isomorphism between contravariant and covariant Lorentz vectors

The morphism of representations from ContrMod.rep to CoMod.rep defined by multiplication with the metric.

def Contr.toCo (d : ℕ) : IntertwiningMap (ContrMod.rep (d := d)) (CoMod.rep (d := d)) where
  toFun := fun ψ => CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ)
  map_add' := byd:ℕ⊢ ∀ (x y : ContrMod d),
  CoMod.toFin1dℝEquiv.symm (η *ᵥ (x + y).toFin1dℝ) =
    CoMod.toFin1dℝEquiv.symm (η *ᵥ x.toFin1dℝ) + CoMod.toFin1dℝEquiv.symm (η *ᵥ y.toFin1dℝ)
    intro ψ ψ'd:ℕψ:ContrMod dψ':ContrMod d⊢ CoMod.toFin1dℝEquiv.symm (η *ᵥ (ψ + ψ').toFin1dℝ) =
  CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ) + CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ'.toFin1dℝ)
    simp only [map_add, mulVec_add]All goals completed! 🐙
  map_smul' := byd:ℕ⊢ ∀ (m : ℝ) (x : ContrMod d),
  CoMod.toFin1dℝEquiv.symm (η *ᵥ (m • x).toFin1dℝ) = (RingHom.id ℝ) m • CoMod.toFin1dℝEquiv.symm (η *ᵥ x.toFin1dℝ)
    intro r ψd:ℕr:ℝψ:ContrMod d⊢ CoMod.toFin1dℝEquiv.symm (η *ᵥ (r • ψ).toFin1dℝ) = (RingHom.id ℝ) r • CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ)
    simp only [_root_.map_smul, mulVec_smul, RingHom.id_apply]All goals completed! 🐙
  isIntertwining' g := byd:ℕg:↑(LorentzGroup d)⊢ { toFun := fun ψ => CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ ContrMod.rep g =
  CoMod.rep g ∘ₗ { toFun := fun ψ => CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ), map_add' := ⋯, map_smul' := ⋯ }
    ext1 ψd:ℕg:↑(LorentzGroup d)ψ:ContrMod d⊢ ({ toFun := fun ψ => CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ ContrMod.rep g) ψ =
  (CoMod.rep g ∘ₗ { toFun := fun ψ => CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ), map_add' := ⋯, map_smul' := ⋯ }) ψ
    conv_lhs =>
      change CoMod.toFin1dℝEquiv.symm (η *ᵥ (g.1 *ᵥ ψ.toFin1dℝ))d:ℕg:↑(LorentzGroup d)ψ:ContrMod d| CoMod.toFin1dℝEquiv.symm (η *ᵥ ↑g *ᵥ ψ.toFin1dℝ)
      rw [mulVec_mulVec, LorentzGroup.minkowskiMatrix_comm, ← mulVec_mulVec]d:ℕg:↑(LorentzGroup d)ψ:ContrMod d| CoMod.toFin1dℝEquiv.symm (↑(LorentzGroup.transpose g⁻¹) *ᵥ η *ᵥ ψ.toFin1dℝ)
    rflAll goals completed! 🐙

The morphism of representations from CoMod.rep to ContrMod.rep defined by multiplication with the metric.

def Co.toContr (d : ℕ) : IntertwiningMap (CoMod.rep (d := d)) (ContrMod.rep (d := d)) where
    toFun := fun ψ => ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ)
    map_add' := byd:ℕ⊢ ∀ (x y : CoMod d),
  ContrMod.toFin1dℝEquiv.symm (η *ᵥ (x + y).toFin1dℝ) =
    ContrMod.toFin1dℝEquiv.symm (η *ᵥ x.toFin1dℝ) + ContrMod.toFin1dℝEquiv.symm (η *ᵥ y.toFin1dℝ)
      intro ψ ψ'd:ℕψ:CoMod dψ':CoMod d⊢ ContrMod.toFin1dℝEquiv.symm (η *ᵥ (ψ + ψ').toFin1dℝ) =
  ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ) + ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ'.toFin1dℝ)
      simp only [map_add, mulVec_add]All goals completed! 🐙
    map_smul' := byd:ℕ⊢ ∀ (m : ℝ) (x : CoMod d),
  ContrMod.toFin1dℝEquiv.symm (η *ᵥ (m • x).toFin1dℝ) = (RingHom.id ℝ) m • ContrMod.toFin1dℝEquiv.symm (η *ᵥ x.toFin1dℝ)
      intro r ψd:ℕr:ℝψ:CoMod d⊢ ContrMod.toFin1dℝEquiv.symm (η *ᵥ (r • ψ).toFin1dℝ) = (RingHom.id ℝ) r • ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ)
      simp only [_root_.map_smul, mulVec_smul, RingHom.id_apply]All goals completed! 🐙
    isIntertwining' g := byd:ℕg:↑(LorentzGroup d)⊢ { toFun := fun ψ => ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ CoMod.rep g =
  ContrMod.rep g ∘ₗ { toFun := fun ψ => ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ), map_add' := ⋯, map_smul' := ⋯ }
      ext1 ψd:ℕg:↑(LorentzGroup d)ψ:CoMod d⊢ ({ toFun := fun ψ => ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ CoMod.rep g) ψ =
  (ContrMod.rep g ∘ₗ { toFun := fun ψ => ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ), map_add' := ⋯, map_smul' := ⋯ })
    ψ
      conv_lhs =>
        change ContrMod.toFin1dℝEquiv.symm (η *ᵥ ((LorentzGroup.transpose g⁻¹).1 *ᵥ ψ.toFin1dℝ))d:ℕg:↑(LorentzGroup d)ψ:CoMod d| ContrMod.toFin1dℝEquiv.symm (η *ᵥ ↑(LorentzGroup.transpose g⁻¹) *ᵥ ψ.toFin1dℝ)
        rw [mulVec_mulVec, ← LorentzGroup.comm_minkowskiMatrix, ← mulVec_mulVec]d:ℕg:↑(LorentzGroup d)ψ:CoMod d| ContrMod.toFin1dℝEquiv.symm (↑g *ᵥ η *ᵥ ψ.toFin1dℝ)
      rflAll goals completed! 🐙

The isomorphism between ContrMod.rep and CoMod.rep induced by multiplication with the Minkowski metric.

def contrIsoCo (d : ℕ) : Representation.Equiv (ContrMod.rep (d := d)) (CoMod.rep (d := d)) := byd:ℕ⊢ ContrMod.rep.Equiv CoMod.rep
  refine Representation.Equiv.mk' (Contr.toCo d) (Co.toContr d) ?_ ?_refine_1d:ℕ⊢ Function.LeftInverse (⇑(Co.toContr d)) (Contr.toCo d).toFunrefine_2d:ℕ⊢ Function.RightInverse (⇑(Co.toContr d)) (Contr.toCo d).toFun
  ·refine_1d:ℕ⊢ Function.LeftInverse (⇑(Co.toContr d)) (Contr.toCo d).toFun intro xrefine_1d:ℕx:ContrMod d⊢ (Co.toContr d) ((Contr.toCo d).toFun x) = x
    simp [Contr.toCo, Co.toContr]All goals completed! 🐙
  ·refine_2d:ℕ⊢ Function.RightInverse (⇑(Co.toContr d)) (Contr.toCo d).toFun intro xrefine_2d:ℕx:CoMod d⊢ (Contr.toCo d).toFun ((Co.toContr d) x) = x
    simp [Contr.toCo, Co.toContr]All goals completed! 🐙

Other properties

lemma ρ_stdBasis (μ : Fin 1 ⊕ Fin 3) (Λ : LorentzGroup 3) :
    ContrMod.rep Λ (ContrMod.stdBasis μ) = ∑ j, Λ.1 j μ • ContrMod.stdBasis j := byμ:Fin 1 ⊕ Fin 3Λ:↑(LorentzGroup 3)⊢ (ContrMod.rep Λ) (ContrMod.stdBasis μ) = ∑ j, ↑Λ j μ • ContrMod.stdBasis j
  change Λ *ᵥ ContrMod.stdBasis μ = ∑ j, Λ.1 j μ • ContrMod.stdBasis jμ:Fin 1 ⊕ Fin 3Λ:↑(LorentzGroup 3)⊢ ↑Λ *ᵥ ContrMod.stdBasis μ = ∑ j, ↑Λ j μ • ContrMod.stdBasis j
  apply ContrMod.extμ:Fin 1 ⊕ Fin 3Λ:↑(LorentzGroup 3)⊢ (↑Λ *ᵥ ContrMod.stdBasis μ).val = (∑ j, ↑Λ j μ • ContrMod.stdBasis j).val
  simp only [toLinAlgEquiv_self, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
    Fin.isValue, Finset.sum_singleton, ContrMod.val_add, ContrMod.val_smul]All goals completed! 🐙