1. Physlib
  2. Relativity
  3. Tensors
  4. RealTensor
  5. Vector
  6. MinkowskiProduct
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 Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic

Minkowski product on Lorentz vectors

In this module we define and create an API around the Minkowski product on Lorentz vectors.

@[expose] public section

The minkowskiProduct

The Minkowski product of Lorentz vectors in the +--- convention..

def minkowskiProductMap {d : ℕ} (p q : Vector d) : ℝ := {η' d | μ ν ⊗ p | μ ⊗ q | ν}ᵀ.toField
All goals completed! 🐙) (d:ℕp:Vector dq:Vector dx:Fin 1 ⊕ Fin d⊢ x ∉ Finset.univ → minkowskiMatrix x x * p x = 0 All goals completed! 🐙)] d:ℕp:Vector dq:Vector d⊢ p (Sum.inl 0) * q (Sum.inl 0) + -∑ x, p (Sum.inr x) * q (Sum.inr x) = p (Sum.inl 0) * q (Sum.inl 0) - ∑ i, p (Sum.inr i) * q (Sum.inr i) All goals completed! 🐙lemma minkowskiProductMap_symm {d : ℕ} (p q : Vector d) : minkowskiProductMap p q = minkowskiProductMap q p := d:ℕp:Vector dq:Vector d⊢ p.minkowskiProductMap q = q.minkowskiProductMap p All goals completed! 🐙@[simp] lemma minkowskiProductMap_add_fst {d : ℕ} (p q r : Vector d) : minkowskiProductMap (p + q) r = minkowskiProductMap p r + minkowskiProductMap q r := d:ℕp:Vector dq:Vector dr:Vector d⊢ (p + q).minkowskiProductMap r = p.minkowskiProductMap r + q.minkowskiProductMap r d:ℕp:Vector dq:Vector dr:Vector d⊢ p (Sum.inl 0) * r (Sum.inl 0) + q (Sum.inl 0) * r (Sum.inl 0) - (∑ x, p (Sum.inr x) * r (Sum.inr x) + ∑ x, q (Sum.inr x) * r (Sum.inr x)) = p (Sum.inl 0) * r (Sum.inl 0) - ∑ x, p (Sum.inr x) * r (Sum.inr x) + (q (Sum.inl 0) * r (Sum.inl 0) - ∑ x, q (Sum.inr x) * r (Sum.inr x)) All goals completed! 🐙All goals completed! 🐙@[simp] lemma minkowskiProductMap_smul_fst {d : ℕ} (c : ℝ) (p q : Vector d) : minkowskiProductMap (c • p) q = c * minkowskiProductMap p q := d:ℕc:ℝp:Vector dq:Vector d⊢ (c • p).minkowskiProductMap q = c * p.minkowskiProductMap q All goals completed! 🐙All goals completed! 🐙

The Minkowski product of two Lorentz vectors as a linear map.

d:ℕ⊢ ∀ (y : Vector d), Continuous fun x => { toFun := fun q => x.minkowskiProductMap q, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } y d:ℕq:Vector d⊢ Continuous fun x => { toFun := fun q => x.minkowskiProductMap q, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } q d:ℕq:Vector d⊢ Continuous fun x => x.minkowskiProductMap q d:ℕq:Vector d| Continuous fun x => x.minkowskiProductMap q d:ℕq:Vector dp:Vector d| p.minkowskiProductMap q d:ℕq:Vector dp:Vector d| p (Sum.inl 0) * q (Sum.inl 0) - ∑ i, p (Sum.inr i) * q (Sum.inr i) All goals completed! 🐙
@[inherit_doc minkowskiProduct] scoped notation "⟪" p ", " q "⟫ₘ" => minkowskiProduct p qlemma minkowskiProduct_apply {d : ℕ} (p q : Vector d) : ⟪p, q⟫ₘ = minkowskiProductMap p q := rfld:ℕp:Vector dq:Vector d⊢ q.minkowskiProductMap p = (minkowskiProduct q) p All goals completed! 🐙All goals completed! 🐙d:ℕp:Vector dq:Vector d⊢ p (Sum.inl 0) * q (Sum.inl 0) - ∑ i, p (Sum.inr i) * q (Sum.inr i) = ∑ μ, minkowskiMatrix μ μ * p μ * q μ d:ℕp:Vector dq:Vector d⊢ p (Sum.inl 0) * q (Sum.inl 0) - ∑ i, p (Sum.inr i) * q (Sum.inr i) = p (Sum.inl 0) * q (Sum.inl 0) + -∑ x, p (Sum.inr x) * q (Sum.inr x) All goals completed! 🐙d:ℕp:Vector dq:Vector dΛ:↑(LorentzGroup d)⊢ toField ((contrT 0 0 1 ⋯) ((prodT ((contrT 1 0 2 ⋯) ((prodT (coMetric d)) (Tensorial.toTensor p)))) (Tensorial.toTensor q))) = (minkowskiProduct p) q All goals completed! 🐙d:ℕp:Vector d⊢ p.timeComponent * p.timeComponent = RCLike.re p.timeComponent * RCLike.re p.timeComponent + RCLike.im p.timeComponent * RCLike.im p.timeComponent All goals completed! 🐙 d:ℕp:Vector d⊢ inner ℝ p.spatialPart p.spatialPart = ‖p.spatialPart‖ ^ 2 All goals completed! 🐙d:ℕp:Vector d⊢ ‖p.timeComponent‖ ^ 2 - ‖p.spatialPart‖ ^ 2 ≤ p.timeComponent ^ 2 All goals completed! 🐙d:ℕμ:Fin 1 ⊕ Fin dp:Vector d⊢ ∑ μ_1, minkowskiMatrix μ_1 μ_1 * basis μ μ_1 * p μ_1 = minkowskiMatrix μ μ * p μ All goals completed! 🐙All goals completed! 🐙d:ℕp:Vector dh:∀ (q : Vector d), (minkowskiProduct p) q = 0μ:Fin 1 ⊕ Fin d⊢ 0 = minkowskiMatrix μ μ * 0 μ All goals completed! 🐙 d:ℕp:Vector d⊢ p = 0 → ∀ (q : Vector d), (minkowskiProduct p) q = 0 d:ℕp:Vector dh:p = 0⊢ ∀ (q : Vector d), (minkowskiProduct p) q = 0 d:ℕ⊢ ∀ (q : Vector d), (minkowskiProduct 0) q = 0 All goals completed! 🐙

The adjoint of a linear map

d:ℕf:Vector d →ₗ[ℝ] Vector dh:∀ (p q : Vector d), (minkowskiProduct (f p)) q = (minkowskiProduct p) qp:Vector dh1:∀ (q : Vector d), (minkowskiProduct (f p)) q = (minkowskiProduct p) qh2:f p = p⊢ f p = p All goals completed! 🐙 d:ℕf:Vector d →ₗ[ℝ] Vector d⊢ f = LinearMap.id → ∀ (p q : Vector d), (minkowskiProduct (f p)) q = (minkowskiProduct p) q d:ℕf:Vector d →ₗ[ℝ] Vector dh:f = LinearMap.id⊢ ∀ (p q : Vector d), (minkowskiProduct (f p)) q = (minkowskiProduct p) q d:ℕ⊢ ∀ (p q : Vector d), (minkowskiProduct (LinearMap.id p)) q = (minkowskiProduct p) q All goals completed! 🐙

The adjoint of a linear map from Vector d to itself with respect to the minkowskiProduct.

def adjoint {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : Vector d →ₗ[ℝ] Vector d := (LinearMap.toMatrix Vector.basis Vector.basis).symm <| minkowskiMatrix.dual <| LinearMap.toMatrix Vector.basis Vector.basis f
d:ℕf:Vector d →ₗ[ℝ] Vector dp:Vector dq:Vector dμ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ minkowskiMatrix ν ν * p μ * (LinearMap.toMatrix basis basis) f ν μ * q ν = minkowskiMatrix ν ν * p μ * (LinearMap.toMatrix basis basis) f ν μ * q ν * 1 All goals completed! 🐙All goals completed! 🐙

The property IsLorentz of linear maps

A linear map Vector d →ₗ[ℝ] Vector d satisfies IsLorentz if it preserves the minkowski product.

def IsLorentz {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : Prop := ∀ p q : Vector d, ⟪f p, f q⟫ₘ = ⟪p, q⟫ₘ
lemma isLorentz_iff {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : IsLorentz f ↔ ∀ p q : Vector d, ⟪f p, f q⟫ₘ = ⟪p, q⟫ₘ := d:ℕf:Vector d →ₗ[ℝ] Vector d⊢ IsLorentz f ↔ ∀ (p q : Vector d), (minkowskiProduct (f p)) (f q) = (minkowskiProduct p) q All goals completed! 🐙d:ℕf:Vector d →ₗ[ℝ] Vector dh:∀ (μ ν : Fin 1 ⊕ Fin d), (minkowskiProduct (f (basis μ))) (f (basis ν)) = (minkowskiProduct (basis μ)) (basis ν)p:Vector dq:Vector dhp:p = ∑ μ, p μ • basis μhq:q = ∑ ν, q ν • basis ν⊢ (minkowskiProduct (f (∑ μ, p μ • basis μ))) (f (∑ ν, q ν • basis ν)) = (minkowskiProduct (∑ μ, p μ • basis μ)) (∑ ν, q ν • basis ν) All goals completed! 🐙All goals completed! 🐙d:ℕf:Vector d →ₗ[ℝ] Vector d⊢ (LinearMap.toMatrix basis basis) (adjoint f) * (LinearMap.toMatrix basis basis) f = 1 ↔ minkowskiMatrix.dual ((LinearMap.toMatrix basis basis) f) * (LinearMap.toMatrix basis basis) f = 1 All goals completed! 🐙