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.

source

def Lorentz.CoVector (d : ℕ := 3) :

Type

Real contravariant Lorentz vector.

Equations

Lorentz.CoVector d = (Fin 1 ⊕ Fin d → ℝ)

Instances For

source

instance Lorentz.CoVector.instAddCommMonoid {d : ℕ} :

AddCommMonoid (CoVector d)

Equations

Lorentz.CoVector.instAddCommMonoid = inferInstanceAs (AddCommMonoid (Fin 1 ⊕ Fin d → ℝ))

source

instance Lorentz.CoVector.instModuleReal {d : ℕ} :

Module ℝ (CoVector d)

Equations

Lorentz.CoVector.instModuleReal = inferInstanceAs (Module ℝ (Fin 1 ⊕ Fin d → ℝ))

source

instance Lorentz.CoVector.instAddCommGroup {d : ℕ} :

AddCommGroup (CoVector d)

Equations

Lorentz.CoVector.instAddCommGroup = inferInstanceAs (AddCommGroup (Fin 1 ⊕ Fin d → ℝ))

source

instance Lorentz.CoVector.instFiniteDimensionalReal {d : ℕ} :

FiniteDimensional ℝ (CoVector d)

source

instance Lorentz.CoVector.isNormedAddCommGroup (d : ℕ) :

NormedAddCommGroup (CoVector d)

Equations

Lorentz.CoVector.isNormedAddCommGroup d = inferInstanceAs (NormedAddCommGroup (Fin 1 ⊕ Fin d → ℝ))

source

instance Lorentz.CoVector.isNormedSpace (d : ℕ) :

NormedSpace ℝ (CoVector d)

Equations

Lorentz.CoVector.isNormedSpace d = inferInstanceAs (NormedSpace ℝ (Fin 1 ⊕ Fin d → ℝ))

source

instance Lorentz.CoVector.instChartedSpace {d : ℕ} :

ChartedSpace (CoVector d) (CoVector d)

The instance of a ChartedSpace on Vector d.

Equations

Lorentz.CoVector.instChartedSpace = chartedSpaceSelf (Lorentz.CoVector d)

source

instance Lorentz.CoVector.instCoeFunForallSumFinOfNatNatReal {d : ℕ} :

CoeFun (CoVector d) fun (x : CoVector d) => Fin 1 ⊕ Fin d → ℝ

Equations

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

source

@[simp]

theorem Lorentz.CoVector.apply_smul {d : ℕ} (c : ℝ) (v : CoVector d) (i : Fin 1 ⊕ Fin d) :

(c • v) i = c * v i

source

@[simp]

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

(v + w) i = v i + w i

source

@[simp]

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

(v - w) i = v i - w i

source

@[simp]

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

(-v) i = -v i

source

@[simp]

theorem Lorentz.CoVector.zero_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) :

0 i = 0

Tensorial #

source

def Lorentz.CoVector.indexEquiv {d : ℕ} :

TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.down ] ≃ 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.

Instances For

source

instance Lorentz.CoVector.tensorial {d : ℕ} :

(realLorentzTensor d).Tensorial ![realLorentzTensor.Color.down ] (CoVector d)

Equations

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

source

theorem Lorentz.CoVector.toTensor_symm_pure {d : ℕ} (p : TensorSpecies.Tensor.Pure (realLorentzTensor d) ![realLorentzTensor.Color.down ]) (i : Fin 1 ⊕ Fin d) :

TensorSpecies.Tensorial.toTensor.symm p.toTensor i = ((coBasisFin d).repr (p 0)) (indexEquiv.symm i 0)

Basis #

source

def Lorentz.CoVector.basis {d : ℕ} :

Module.Basis (Fin 1 ⊕ Fin d) ℝ (CoVector d)

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

Equations

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

Instances For

source

@[simp]

theorem Lorentz.CoVector.basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) :

basis μ ν = if μ = ν then 1 else 0

source

theorem Lorentz.CoVector.toTensor_symm_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) :

TensorSpecies.Tensorial.toTensor.symm ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.down ]) (indexEquiv.symm μ)) = basis μ

source

theorem Lorentz.CoVector.toTensor_basis_eq_tensor_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) :

TensorSpecies.Tensorial.toTensor (basis μ) = (TensorSpecies.Tensor.basis ![realLorentzTensor.Color.down ]) (indexEquiv.symm μ)

source

theorem Lorentz.CoVector.basis_eq_map_tensor_basis :

basis = ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.down ]).map TensorSpecies.Tensorial.toTensor.symm).reindex indexEquiv

source

theorem Lorentz.CoVector.tensor_basis_map_eq_basis_reindex :

(TensorSpecies.Tensor.basis ![realLorentzTensor.Color.down ]).map TensorSpecies.Tensorial.toTensor.symm = basis.reindex indexEquiv.symm

source

theorem Lorentz.CoVector.tensor_basis_repr_toTensor_apply {d : ℕ} (p : CoVector d) (μ : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.down ]) :

((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.down ]).repr (TensorSpecies.Tensorial.toTensor p)) μ = p (indexEquiv μ)

source

theorem Lorentz.CoVector.basis_repr_apply {d : ℕ} (p : CoVector d) (μ : Fin 1 ⊕ Fin d) :

(basis.repr p) μ = p μ

source

theorem Lorentz.CoVector.map_apply_eq_basis_mulVec {d : ℕ} (f : CoVector d →ₗ[ℝ ] CoVector d) (p : CoVector d) :

f p = ((LinearMap.toMatrix basis basis) f).mulVec p

The action of the Lorentz group #

source

theorem Lorentz.CoVector.smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : ↑(LorentzGroup d)) (p : CoVector d) :

(Λ • p) i = ∑ j : Fin 1 ⊕ Fin d, ↑Λ⁻¹ j i * p j

source

theorem Lorentz.CoVector.smul_eq_mulVec {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : CoVector d) :

Λ • p = (↑(LorentzGroup.transpose Λ⁻¹)).mulVec p

source

theorem Lorentz.CoVector.smul_add {d : ℕ} (Λ : ↑(LorentzGroup d)) (p q : CoVector d) :

Λ • (p + q) = Λ • p + Λ • q

source

@[simp]

theorem Lorentz.CoVector.smul_sub {d : ℕ} (Λ : ↑(LorentzGroup d)) (p q : CoVector d) :

Λ • (p - q) = Λ • p - Λ • q

source

theorem Lorentz.CoVector.smul_zero {d : ℕ} (Λ : ↑(LorentzGroup d)) :

Λ • 0 = 0

source

theorem Lorentz.CoVector.smul_neg {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : CoVector d) :

Λ • -p = -(Λ • p)

source

def Lorentz.CoVector.actionCLM {d : ℕ} (Λ : ↑(LorentzGroup d)) :

CoVector d →L[ℝ ] CoVector d

The Lorentz action on vectors as a continuous linear map.

Equations

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

Instances For

source

theorem Lorentz.CoVector.actionCLM_apply {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : CoVector d) :

(actionCLM Λ) p = Λ • p

source

theorem Lorentz.CoVector.smul_basis {d : ℕ} (Λ : ↑(LorentzGroup d)) (μ : Fin 1 ⊕ Fin d) :

Λ • basis μ = ∑ ν : Fin 1 ⊕ Fin d, ↑Λ⁻¹ μ ν • basis ν

PhysLean Documentation

PhysLean.Relativity.Tensors.RealTensor.CoVector.Basic

Lorentz co vectors #

Tensorial #

Basis #

The action of the Lorentz group #