1. Physlib
  2. Relativity
  3. Tensors
  4. RealTensor
  5. CoVector
  6. Basic
Imports
/- Copyright (c) 2025 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 Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.Geometry.Manifold.IsManifold.Basic

Lorentz co vectors

In this module we define Lorentz vectors as real Lorentz tensors with a single up index. We create an API around Lorentz vectors to make working with them as easy as possible.

@[expose] public section

Real contravariant Lorentz vector.

def CoVector (d : ℕ := 3) := Fin 1 ⊕ Fin d → ℝ
instance {d} : AddCommMonoid (CoVector d) := inferInstanceAs (AddCommMonoid (Fin 1 ⊕ Fin d → ℝ))instance {d} : Module ℝ (CoVector d) := inferInstanceAs (Module ℝ (Fin 1 ⊕ Fin d → ℝ))instance {d} : AddCommGroup (CoVector d) := inferInstanceAs (AddCommGroup (Fin 1 ⊕ Fin d → ℝ))instance {d} : FiniteDimensional ℝ (CoVector d) := inferInstanceAs (FiniteDimensional ℝ (Fin 1 ⊕ Fin d → ℝ))

The equivalence between CoVector d and EuclideanSpace ℝ (Fin 1 ⊕ Fin d).

def equivEuclid (d : ℕ) : CoVector d ≃ₗ[ℝ] EuclideanSpace ℝ (Fin 1 ⊕ Fin d) := (WithLp.linearEquiv _ _ _).symm
@[ext] lemma eq_of_apply_eq {d : ℕ} {v w : CoVector d} (h : ∀ i, v i = w i) : v = w := d:ℕv:CoVector dw:CoVector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w i⊢ v = w d:ℕv:CoVector dw:CoVector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w i⊢ (equivEuclid d) v = (equivEuclid d) w d:ℕv:CoVector dw:CoVector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w ii:Fin 1 ⊕ Fin d⊢ ((equivEuclid d) v).ofLp i = ((equivEuclid d) w).ofLp i All goals completed! 🐙instance (d : ℕ) : Norm (CoVector d) where norm := fun v => ‖equivEuclid d v‖lemma norm_eq_equivEuclid (d : ℕ) (v : CoVector d) : ‖v‖ = ‖equivEuclid d v‖ := rflAll goals completed! 🐙instance isNormedSpace (d : ℕ) : NormedSpace ℝ (CoVector d) where norm_smul_le c v := d:ℕc:ℝv:CoVector d⊢ ‖c • v‖ ≤ ‖c‖ * ‖v‖ d:ℕc:ℝv:CoVector d⊢ ‖c • (equivEuclid d) v‖ ≤ ‖c‖ * ‖(equivEuclid d) v‖ All goals completed! 🐙instance (d : ℕ) : Inner ℝ (CoVector d) where inner := fun v w => ⟪equivEuclid d v, equivEuclid d w⟫_ℝlemma inner_eq_equivEuclid (d : ℕ) (v w : CoVector d) : ⟪v, w⟫_ℝ = ⟪equivEuclid d v, equivEuclid d w⟫_ℝ := rfl

The Euclidean inner product structure on CoVector.

instance innerProductSpace (d : ℕ) : InnerProductSpace ℝ (CoVector d) where norm_sq_eq_re_inner v := d:ℕv:CoVector d⊢ ‖v‖ ^ 2 = RCLike.re ⟪v, v⟫_ℝ d:ℕv:CoVector d⊢ ‖(equivEuclid d) v‖ ^ 2 = RCLike.re ⟪(equivEuclid d) v, (equivEuclid d) v⟫_ℝ All goals completed! 🐙 conj_inner_symm x y := d:ℕx:CoVector dy:CoVector d⊢ (starRingEnd ℝ) ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ d:ℕx:CoVector dy:CoVector d⊢ (starRingEnd ℝ) ⟪(equivEuclid d) y, (equivEuclid d) x⟫_ℝ = ⟪(equivEuclid d) x, (equivEuclid d) y⟫_ℝ All goals completed! 🐙 add_left x y z := d:ℕx:CoVector dy:CoVector dz:CoVector d⊢ ⟪x + y, z⟫_ℝ = ⟪x, z⟫_ℝ + ⟪y, z⟫_ℝ d:ℕx:CoVector dy:CoVector dz:CoVector d⊢ ⟪(equivEuclid d) x + (equivEuclid d) y, (equivEuclid d) z⟫_ℝ = ⟪(equivEuclid d) x, (equivEuclid d) z⟫_ℝ + ⟪(equivEuclid d) y, (equivEuclid d) z⟫_ℝ All goals completed! 🐙 smul_left x y r := d:ℕx:CoVector dy:CoVector dr:ℝ⊢ ⟪r • x, y⟫_ℝ = (starRingEnd ℝ) r * ⟪x, y⟫_ℝ d:ℕx:CoVector dy:CoVector dr:ℝ⊢ ⟪r • (equivEuclid d) x, (equivEuclid d) y⟫_ℝ = (starRingEnd ℝ) r * ⟪(equivEuclid d) x, (equivEuclid d) y⟫_ℝ All goals completed! 🐙

The instance of a ChartedSpace on Vector d.

instance : ChartedSpace (CoVector d) (CoVector d) := chartedSpaceSelf (CoVector d)
instance {d} : CoeFun (CoVector d) (fun _ => Fin 1 ⊕ Fin d → ℝ) where coe := fun v => v@[simp] lemma apply_smul {d : ℕ} (c : ℝ) (v : CoVector d) (i : Fin 1 ⊕ Fin d) : (c • v) i = c * v i := rfl@[simp] lemma apply_add {d : ℕ} (v w : CoVector d) (i : Fin 1 ⊕ Fin d) : (v + w) i = v i + w i := rfl@[simp] lemma apply_sub {d : ℕ} (v w : CoVector d) (i : Fin 1 ⊕ Fin d) : (v - w) i = v i - w i := d:ℕv:CoVector dw:CoVector di:Fin 1 ⊕ Fin d⊢ (v - w) i = v i - w i All goals completed! 🐙@[simp] lemma apply_sum {d : ℕ} {ι : Type} [Fintype ι] (f : ι → CoVector d) (i : Fin 1 ⊕ Fin d) : (∑ j, f j) i = ∑ j, f j i := Finset.sum_apply i Finset.univ f@[simp] lemma neg_apply {d : ℕ} (v : CoVector d) (i : Fin 1 ⊕ Fin d) : (-v) i = - v i := rfl@[simp] lemma zero_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) : (0 : CoVector d) i = 0 := rfl

Basis

The basis on Vector d indexed by Fin 1 ⊕ Fin d.

def basis {d : ℕ} : Basis (Fin 1 ⊕ Fin d) ℝ (CoVector d) := Pi.basisFun ℝ _
@[simp] lemma basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : basis μ ν = if μ = ν then 1 else 0 := d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ basis μ ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (Pi.basisFun ℝ (Fin 1 ⊕ Fin d)) μ ν = if μ = ν then 1 else 0 erw [d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Pi.single μ 1 ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (if ν = μ then 1 else 0) = if μ = ν then 1 else 0d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (if ν = μ then 1 else 0) = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (ν = μ) = (μ = ν) All goals completed! 🐙lemma basis_repr_apply {d : ℕ} (p : CoVector d) (μ : Fin 1 ⊕ Fin d) : basis.repr p μ = p μ := d:ℕp:CoVector dμ:Fin 1 ⊕ Fin d⊢ (basis.repr p) μ = p μ d:ℕp:CoVector dμ:Fin 1 ⊕ Fin d⊢ ((Pi.basisFun ℝ (Fin 1 ⊕ Fin d)).repr p) μ = p μ erw [d:ℕp:CoVector dμ:Fin 1 ⊕ Fin d⊢ p μ = p μAll goals completed! 🐙lemma map_apply_eq_basis_mulVec {d : ℕ} (f : CoVector d →ₗ[ℝ] CoVector d) (p : CoVector d) : (f p) = (LinearMap.toMatrix basis basis) f *ᵥ p := d:ℕf:CoVector d →ₗ[ℝ] CoVector dp:CoVector d⊢ f p = (LinearMap.toMatrix basis basis) f *ᵥ p All goals completed! 🐙