Lorentz 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.

def Lorentz.Vector (d : ℕ := 3) : Type

Real contravariant Lorentz vector.

Equations

• Lorentz.Vector d = (Fin 1 ⊕ Fin d → ℝ)

instance Lorentz.Vector.instAddCommMonoid {d : ℕ} : AddCommMonoid (Vector d)

Equations

• Lorentz.Vector.instAddCommMonoid = inferInstanceAs (AddCommMonoid (EuclideanSpace ℝ (Fin 1 ⊕ Fin d)))

instance Lorentz.Vector.instModuleReal {d : ℕ} : Module ℝ (Vector d)

Equations

• Lorentz.Vector.instModuleReal = inferInstanceAs (Module ℝ (EuclideanSpace ℝ (Fin 1 ⊕ Fin d)))

instance Lorentz.Vector.instAddCommGroup {d : ℕ} : AddCommGroup (Vector d)

Equations

• Lorentz.Vector.instAddCommGroup = inferInstanceAs (AddCommGroup (EuclideanSpace ℝ (Fin 1 ⊕ Fin d)))

instance Lorentz.Vector.instFiniteDimensionalReal {d : ℕ} : FiniteDimensional ℝ (Vector d)

instance Lorentz.Vector.isNormedAddCommGroup (d : ℕ) : NormedAddCommGroup (Vector d)

Equations

• Lorentz.Vector.isNormedAddCommGroup d = inferInstanceAs (NormedAddCommGroup (EuclideanSpace ℝ (Fin 1 ⊕ Fin d)))

instance Lorentz.Vector.isNormedSpace (d : ℕ) : NormedSpace ℝ (Vector d)

Equations

• Lorentz.Vector.isNormedSpace d = inferInstanceAs (NormedSpace ℝ (EuclideanSpace ℝ (Fin 1 ⊕ Fin d)))

instance Lorentz.Vector.innerProductSpace (d : ℕ) : InnerProductSpace ℝ (Vector d)

The Euclidean inner product structure on Vector.

Equations

• Lorentz.Vector.innerProductSpace d = inferInstanceAs (InnerProductSpace ℝ (EuclideanSpace ℝ (Fin 1 ⊕ Fin d)))

instance Lorentz.Vector.instChartedSpace {d : ℕ} : ChartedSpace (Vector d) (Vector d)

The instance of a ChartedSpace on Vector d.

Equations

• Lorentz.Vector.instChartedSpace = chartedSpaceSelf (Lorentz.Vector d)

instance Lorentz.Vector.instCoeFunForallSumFinOfNatNatReal {d : ℕ} : CoeFun (Vector d) fun (x : Vector d) => Fin 1 ⊕ Fin d → ℝ

Equations

• Lorentz.Vector.instCoeFunForallSumFinOfNatNatReal = { coe := fun (v : Lorentz.Vector d) => v }

@[simp]

theorem Lorentz.Vector.apply_smul {d : ℕ} (c : ℝ) (v : Vector d) (i : Fin 1 ⊕ Fin d) : (c • v) i = c * v i

@[simp]

theorem Lorentz.Vector.apply_add {d : ℕ} (v w : Vector d) (i : Fin 1 ⊕ Fin d) : (v + w) i = v i + w i

@[simp]

theorem Lorentz.Vector.apply_sub {d : ℕ} (v w : Vector d) (i : Fin 1 ⊕ Fin d) : (v - w) i = v i - w i

theorem Lorentz.Vector.apply_sum {d : ℕ} {ι : Type} [Fintype ι] (f : ι → Vector d) (i : Fin 1 ⊕ Fin d) : (∑ j : ι, f j) i = ∑ j : ι, f j i

@[simp]

theorem Lorentz.Vector.neg_apply {d : ℕ} (v : Vector d) (i : Fin 1 ⊕ Fin d) : (-v) i = -v i

@[simp]

theorem Lorentz.Vector.zero_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) : 0 i = 0

def Lorentz.Vector.coordCLM {d : ℕ} (i : Fin 1 ⊕ Fin d) : Vector d →L[ℝ] ℝ

The continuous linear map from a Lorentz vector to one of its coordinates.

Equations

• Lorentz.Vector.coordCLM i = { toFun := fun (v : Lorentz.Vector d) => v i, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem Lorentz.Vector.coordCLM_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) (v : Vector d) : (coordCLM i) v = v i

@[simp]

theorem Lorentz.Vector.fderiv_apply {d : ℕ} (μ : Fin 1 ⊕ Fin d) (x : Vector d) : fderiv ℝ (fun (v : Vector d) => v μ) x = coordCLM μ

Tensorial

def Lorentz.Vector.indexEquiv {d : ℕ} : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up] ≃ Fin 1 ⊕ Fin d

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

Equations

• One or more equations did not get rendered due to their size.

instance Lorentz.Vector.tensorial {d : ℕ} : (realLorentzTensor d).Tensorial ![realLorentzTensor.Color.up] (Vector d)

Equations

• One or more equations did not get rendered due to their size.

theorem Lorentz.Vector.toTensor_symm_apply {d : ℕ} (p : (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up]) : TensorSpecies.Tensorial.toTensor.symm p = (Equiv.piCongrLeft' (fun (a : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up]) => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr p))

theorem Lorentz.Vector.toTensor_symm_pure {d : ℕ} (p : TensorSpecies.Tensor.Pure (realLorentzTensor d) ![realLorentzTensor.Color.up]) (i : Fin 1 ⊕ Fin d) : TensorSpecies.Tensorial.toTensor.symm p.toTensor i = ((contrBasisFin d).repr (p 0)) (indexEquiv.symm i 0)

Basis

def Lorentz.Vector.basis {d : ℕ} : Module.Basis (Fin 1 ⊕ Fin d) ℝ (Vector d)

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

Equations

• Lorentz.Vector.basis = Pi.basisFun ℝ (Fin 1 ⊕ Fin d)

@[simp]

theorem Lorentz.Vector.basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : basis μ ν = if μ = ν then 1 else 0

theorem Lorentz.Vector.toTensor_symm_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : TensorSpecies.Tensorial.toTensor.symm ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) (indexEquiv.symm μ)) = basis μ

theorem Lorentz.Vector.toTensor_basis_eq_tensor_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : TensorSpecies.Tensorial.toTensor (basis μ) = (TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) (indexEquiv.symm μ)

theorem Lorentz.Vector.basis_eq_map_tensor_basis {d : ℕ} : basis = ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).map TensorSpecies.Tensorial.toTensor.symm).reindex indexEquiv

theorem Lorentz.Vector.tensor_basis_map_eq_basis_reindex {d : ℕ} : (TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).map TensorSpecies.Tensorial.toTensor.symm = basis.reindex indexEquiv.symm

theorem Lorentz.Vector.tensor_basis_repr_toTensor_apply {d : ℕ} (p : Vector d) (μ : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up]) : ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr (TensorSpecies.Tensorial.toTensor p)) μ = p (indexEquiv μ)

theorem Lorentz.Vector.basis_repr_apply {d : ℕ} (p : Vector d) (μ : Fin 1 ⊕ Fin d) : (basis.repr p) μ = p μ

theorem Lorentz.Vector.map_apply_eq_basis_mulVec {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) (p : Vector d) : f p = ((LinearMap.toMatrix basis basis) f).mulVec p

theorem Lorentz.Vector.sum_basis_eq_zero_iff {d : ℕ} (f : Fin 1 ⊕ Fin d → ℝ) : ∑ μ : Fin 1 ⊕ Fin d, f μ • basis μ = 0 ↔ ∀ (μ : Fin 1 ⊕ Fin d), f μ = 0

theorem Lorentz.Vector.sum_inl_inr_basis_eq_zero_iff {d : ℕ} (f₀ : ℝ) (f : Fin d → ℝ) : f₀ • basis (Sum.inl 0) + ∑ i : Fin d, f i • basis (Sum.inr i) = 0 ↔ f₀ = 0 ∧ ∀ (i : Fin d), f i = 0

The action of the Lorentz group

theorem Lorentz.Vector.smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : ↑(LorentzGroup d)) (p : Vector d) : (Λ • p) i = ∑ j : Fin 1 ⊕ Fin d, ↑Λ i j * p j

theorem Lorentz.Vector.smul_eq_mulVec {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : Vector d) : Λ • p = (↑Λ).mulVec p

theorem Lorentz.Vector.smul_add {d : ℕ} (Λ : ↑(LorentzGroup d)) (p q : Vector d) : Λ • (p + q) = Λ • p + Λ • q

@[simp]

theorem Lorentz.Vector.smul_sub {d : ℕ} (Λ : ↑(LorentzGroup d)) (p q : Vector d) : Λ • (p - q) = Λ • p - Λ • q

theorem Lorentz.Vector.smul_zero {d : ℕ} (Λ : ↑(LorentzGroup d)) : Λ • 0 = 0

theorem Lorentz.Vector.smul_neg {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : Vector d) : Λ • -p = -(Λ • p)

theorem Lorentz.Vector.neg_smul {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : Vector d) : -Λ • p = -(Λ • p)

theorem LorentzGroup.eq_of_action_vector_eq {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : ∀ (p : Lorentz.Vector d), Λ • p = Λ' • p) : Λ = Λ'

def Lorentz.Vector.actionCLM {d : ℕ} (Λ : ↑(LorentzGroup d)) : Vector d →L[ℝ] Vector d

The Lorentz action on vectors as a continuous linear map.

Equations

• Lorentz.Vector.actionCLM Λ = LinearMap.toContinuousLinearMap { toFun := fun (v : Lorentz.Vector d) => Λ • v, map_add' := ⋯, map_smul' := ⋯ }

theorem Lorentz.Vector.actionCLM_apply {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : Vector d) : (actionCLM Λ) p = Λ • p

theorem Lorentz.Vector.smul_basis {d : ℕ} (Λ : ↑(LorentzGroup d)) (μ : Fin 1 ⊕ Fin d) : Λ • basis μ = ∑ ν : Fin 1 ⊕ Fin d, ↑Λ ν μ • basis ν

Spatial part

@[reducible, inline]

abbrev Lorentz.Vector.spatialPart {d : ℕ} (v : Vector d) : EuclideanSpace ℝ (Fin d)

Extract spatial components from a Lorentz vector, returning them as a vector in Euclidean space.

Equations

• v.spatialPart i = v (Sum.inr i)

theorem Lorentz.Vector.spatialPart_apply_eq_toCoord {d : ℕ} (v : Vector d) (i : Fin d) : v.spatialPart i = v (Sum.inr i)

theorem Lorentz.Vector.spatialPart_basis_sum_inr {d : ℕ} (i j : Fin d) : (basis (Sum.inr i)).spatialPart j = (Finsupp.single (Sum.inr i) 1) (Sum.inr j)

theorem Lorentz.Vector.spatialPart_basis_sum_inl {d : ℕ} (i : Fin d) : (basis (Sum.inl 0)).spatialPart i = 0

The time component

@[reducible, inline]

abbrev Lorentz.Vector.timeComponent {d : ℕ} (v : Vector d) : ℝ

Extract time component from a Lorentz vector

Equations

• v.timeComponent = v (Sum.inl 0)

theorem Lorentz.Vector.timeComponent_basis_sum_inr {d : ℕ} (i : Fin d) : (basis (Sum.inr i)).timeComponent = 0

theorem Lorentz.Vector.timeComponent_basis_sum_inl {d : ℕ} : (basis (Sum.inl 0)).timeComponent = 1

## Smoothness

def Lorentz.Vector.asSmoothManifold (d : ℕ) : ModelWithCorners ℝ (Vector d) (Vector d)

The structure of a smooth manifold on Vector .

Equations

• Lorentz.Vector.asSmoothManifold d = modelWithCornersSelf ℝ (Lorentz.Vector d)