Contraction of Real Lorentz vectors

def Lorentz.contrModCoModBi (d : ℕ) : ContrMod d →ₗ[ℝ] CoMod d →ₗ[ℝ] ℝ

The bi-linear map corresponding to contraction of a contravariant Lorentz vector with a covariant Lorentz vector.

Equations

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

def Lorentz.coModContrModBi (d : ℕ) : CoMod d →ₗ[ℝ] ContrMod d →ₗ[ℝ] ℝ

The bi-linear map corresponding to contraction of a covariant Lorentz vector with a contravariant Lorentz vector.

Equations

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

def Lorentz.contrCoContract {d : ℕ} : CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d) (Co d) ⟶ 𝟙_ (Rep ℝ ↑(LorentzGroup d))

The linear map from Contr d ⊗ Co d to ℝ given by summing over components of contravariant Lorentz vector and covariant Lorentz vector in the standard basis (i.e. the dot product). In terms of index notation this is the contraction is ψⁱ φᵢ.

Equations

• Lorentz.contrCoContract = { hom := ModuleCat.ofHom (TensorProduct.lift (Lorentz.contrModCoModBi d)), comm := ⋯ }

def Lorentz.«term⟪_,_⟫ₘ» : Lean.ParserDescr

Notation for contrCoContract acting on a tmul.

Equations

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

theorem Lorentz.contrCoContract_hom_tmul {d : ℕ} (ψ : ↑(Contr d).V) (φ : ↑(Co d).V) : (CategoryTheory.ConcreteCategory.hom contrCoContract.hom) (ψ ⊗ₜ[ℝ] φ) = ContrMod.toFin1dℝ ψ ⬝ᵥ CoMod.toFin1dℝ φ

def Lorentz.coContrContract {d : ℕ} : CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d) (Contr d) ⟶ 𝟙_ (Rep ℝ ↑(LorentzGroup d))

The linear map from Co d ⊗ Contr d to ℝ given by summing over components of contravariant Lorentz vector and covariant Lorentz vector in the standard basis (i.e. the dot product). In terms of index notation this is the contraction is ψⁱ φᵢ.

Equations

• Lorentz.coContrContract = { hom := ModuleCat.ofHom (TensorProduct.lift (Lorentz.coModContrModBi d)), comm := ⋯ }

def Lorentz.«term⟪_,_⟫ₘ_1» : Lean.ParserDescr

Notation for coContrContract acting on a tmul.

Equations

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

theorem Lorentz.coContrContract_hom_tmul {d : ℕ} (φ : ↑(Co d).V) (ψ : ↑(Contr d).V) : (CategoryTheory.ConcreteCategory.hom coContrContract.hom) (φ ⊗ₜ[ℝ] ψ) = CoMod.toFin1dℝ φ ⬝ᵥ ContrMod.toFin1dℝ ψ

Symmetry relations

theorem Lorentz.contrCoContract_tmul_symm {d : ℕ} (φ : ↑(Contr d).V) (ψ : ↑(Co d).V) : (CategoryTheory.ConcreteCategory.hom contrCoContract.hom) (φ ⊗ₜ[ℝ] ψ) = (CategoryTheory.ConcreteCategory.hom coContrContract.hom) (ψ ⊗ₜ[ℝ] φ)

theorem Lorentz.coContrContract_tmul_symm {d : ℕ} (φ : ↑(Co d).V) (ψ : ↑(Contr d).V) : (CategoryTheory.ConcreteCategory.hom coContrContract.hom) (φ ⊗ₜ[ℝ] ψ) = (CategoryTheory.ConcreteCategory.hom contrCoContract.hom) (ψ ⊗ₜ[ℝ] φ)

Contracting contr vectors with contr vectors etc.

def Lorentz.contrContrContract {d : ℕ} : CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d) (Contr d) ⟶ 𝟙_ (Rep ℝ ↑(LorentzGroup d))

The linear map from Contr d ⊗ Contr d to ℝ induced by the homomorphism Contr.toCo and the contraction contrCoContract.

Equations

• Lorentz.contrContrContract = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Lorentz.Contr d) (Lorentz.Contr.toCo d)) Lorentz.contrCoContract

def Lorentz.contrContrContractField {d : ℕ} : TensorProduct ℝ ↑(Contr d).V ↑(Contr d).V →ₗ[ℝ] ℝ

The linear map from Contr d ⊗ Contr d to ℝ induced by the homomorphism Contr.toCo and the contraction contrCoContract.

Equations

• Lorentz.contrContrContractField = ModuleCat.Hom.hom Lorentz.contrContrContract.hom

def Lorentz.«term⟪_,_⟫ₘ_2» : Lean.ParserDescr

Notation for contrContrContractField acting on a tmul.

Equations

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

theorem Lorentz.contrContrContract_hom_tmul {d : ℕ} (φ ψ : ↑(Contr d).V) : contrContrContractField (φ ⊗ₜ[ℝ] ψ) = ContrMod.toFin1dℝ φ ⬝ᵥ minkowskiMatrix.mulVec (ContrMod.toFin1dℝ ψ)

def Lorentz.coCoContract {d : ℕ} : CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d) (Co d) ⟶ 𝟙_ (Rep ℝ ↑(LorentzGroup d))

The linear map from Co d ⊗ Co d to ℝ induced by the homomorphism Co.toContr and the contraction coContrContract.

Equations

• Lorentz.coCoContract = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Lorentz.Co d) (Lorentz.Co.toContr d)) Lorentz.coContrContract

def Lorentz.«term⟪_,_⟫ₘ_3» : Lean.ParserDescr

Notation for coCoContract acting on a tmul.

Equations

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

theorem Lorentz.coCoContract_hom_tmul {d : ℕ} (φ ψ : ↑(Co d).V) : (CategoryTheory.ConcreteCategory.hom coCoContract.hom) (φ ⊗ₜ[ℝ] ψ) = CoMod.toFin1dℝ φ ⬝ᵥ minkowskiMatrix.mulVec (CoMod.toFin1dℝ ψ)

Lemmas related to contraction.

We derive the lemmas in main for contrContrContractField.

@[simp]

theorem Lorentz.contrContrContractField.action_tmul {d : ℕ} (x y : ↑(Contr d).V) (g : ↑(LorentzGroup d)) : contrContrContractField (((Contr d).ρ g) x ⊗ₜ[ℝ] ((Contr d).ρ g) y) = contrContrContractField (x ⊗ₜ[ℝ] y)

theorem Lorentz.contrContrContractField.as_sum {d : ℕ} (x y : ↑(Contr d).V) : contrContrContractField (x ⊗ₜ[ℝ] y) = x.val (Sum.inl 0) * y.val (Sum.inl 0) - ∑ i : Fin d, x.val (Sum.inr i) * y.val (Sum.inr i)

theorem Lorentz.contrContrContractField.as_sum_toSpace {d : ℕ} (x y : ↑(Contr d).V) : contrContrContractField (x ⊗ₜ[ℝ] y) = x.val (Sum.inl 0) * y.val (Sum.inl 0) - inner (ContrMod.toSpace x) (ContrMod.toSpace y)

theorem Lorentz.contrContrContractField.stdBasis_inl {d : ℕ} : contrContrContractField (ContrMod.stdBasis (Sum.inl 0) ⊗ₜ[ℝ] ContrMod.stdBasis (Sum.inl 0)) = 1

theorem Lorentz.contrContrContractField.symm {d : ℕ} (x y : ↑(Contr d).V) : contrContrContractField (x ⊗ₜ[ℝ] y) = contrContrContractField (y ⊗ₜ[ℝ] x)

theorem Lorentz.contrContrContractField.dual_mulVec_right {d : ℕ} (x y : ↑(Contr d).V) {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : contrContrContractField (x ⊗ₜ[ℝ] ContrMod.mulVec (minkowskiMatrix.dual Λ) y) = contrContrContractField (ContrMod.mulVec Λ x ⊗ₜ[ℝ] y)

theorem Lorentz.contrContrContractField.dual_mulVec_left {d : ℕ} (x y : ↑(Contr d).V) {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : contrContrContractField (ContrMod.mulVec (minkowskiMatrix.dual Λ) x ⊗ₜ[ℝ] y) = contrContrContractField (x ⊗ₜ[ℝ] ContrMod.mulVec Λ y)

theorem Lorentz.contrContrContractField.right_parity {d : ℕ} (x y : ↑(Contr d).V) : contrContrContractField (x ⊗ₜ[ℝ] ((Contr d).ρ LorentzGroup.parity) y) = ∑ i : Fin 1 ⊕ Fin d, x.val i * y.val i

theorem Lorentz.contrContrContractField.self_parity_eq_zero_iff {d : ℕ} (y : ↑(Contr d).V) : contrContrContractField (y ⊗ₜ[ℝ] ((Contr d).ρ LorentzGroup.parity) y) = 0 ↔ y = 0

theorem Lorentz.contrContrContractField.nondegenerate {d : ℕ} (y : ↑(Contr d).V) : (∀ (x : ↑(Contr d).V), contrContrContractField (x ⊗ₜ[ℝ] y) = 0) ↔ y = 0

The metric tensor is non-degenerate.

theorem Lorentz.contrContrContractField.matrix_apply_eq_iff_sub {d : ℕ} (x y : ↑(Contr d).V) {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : contrContrContractField (x ⊗ₜ[ℝ] ContrMod.mulVec Λ y) = contrContrContractField (x ⊗ₜ[ℝ] ContrMod.mulVec Λ' y) ↔ contrContrContractField (x ⊗ₜ[ℝ] ContrMod.mulVec (Λ - Λ') y) = 0

theorem Lorentz.contrContrContractField.matrix_eq_iff_eq_forall' {d : ℕ} {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : (∀ (v : ↑(Contr d).V), ContrMod.mulVec Λ v = ContrMod.mulVec Λ' v) ↔ ∀ (w v : ↑(Contr d).V), contrContrContractField (v ⊗ₜ[ℝ] ContrMod.mulVec Λ w) = contrContrContractField (v ⊗ₜ[ℝ] ContrMod.mulVec Λ' w)

theorem Lorentz.contrContrContractField.matrix_eq_iff_eq_forall {d : ℕ} {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : Λ = Λ' ↔ ∀ (w v : ↑(Contr d).V), contrContrContractField (v ⊗ₜ[ℝ] ContrMod.mulVec Λ w) = contrContrContractField (v ⊗ₜ[ℝ] ContrMod.mulVec Λ' w)

theorem Lorentz.contrContrContractField.matrix_eq_id_iff {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : Λ = 1 ↔ ∀ (w v : ↑(Contr d).V), contrContrContractField (v ⊗ₜ[ℝ] ContrMod.mulVec Λ w) = contrContrContractField (v ⊗ₜ[ℝ] w)

theorem LorentzGroup.mem_iff_invariant {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : Λ ∈ LorentzGroup d ↔ ∀ (w v : ↑(Lorentz.Contr d).V), Lorentz.contrContrContractField (Lorentz.ContrMod.mulVec Λ v ⊗ₜ[ℝ] Lorentz.ContrMod.mulVec Λ w) = Lorentz.contrContrContractField (v ⊗ₜ[ℝ] w)

theorem LorentzGroup.mem_iff_norm {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} : Λ ∈ LorentzGroup d ↔ ∀ (w : ↑(Lorentz.Contr d).V), Lorentz.contrContrContractField (Lorentz.ContrMod.mulVec Λ w ⊗ₜ[ℝ] Lorentz.ContrMod.mulVec Λ w) = Lorentz.contrContrContractField (w ⊗ₜ[ℝ] w)

Some equalities and inequalities

theorem Lorentz.contrContrContractField.inl_sq_eq {d : ℕ} (v : ↑(Contr d).V) : v.val (Sum.inl 0) ^ 2 = contrContrContractField (v ⊗ₜ[ℝ] v) + ∑ i : Fin d, v.val (Sum.inr i) ^ 2

theorem Lorentz.contrContrContractField.le_inl_sq {d : ℕ} (v : ↑(Contr d).V) : contrContrContractField (v ⊗ₜ[ℝ] v) ≤ v.val (Sum.inl 0) ^ 2

theorem Lorentz.contrContrContractField.ge_abs_inner_product {d : ℕ} (v w : ↑(Contr d).V) : v.val (Sum.inl 0) * w.val (Sum.inl 0) - ‖inner (ContrMod.toSpace v) (ContrMod.toSpace w)‖ ≤ contrContrContractField (v ⊗ₜ[ℝ] w)

theorem Lorentz.contrContrContractField.ge_sub_norm {d : ℕ} (v w : ↑(Contr d).V) : v.val (Sum.inl 0) * w.val (Sum.inl 0) - ‖ContrMod.toSpace v‖ * ‖ContrMod.toSpace w‖ ≤ contrContrContractField (v ⊗ₜ[ℝ] w)

The Minkowski metric and the standard basis

@[simp]

theorem Lorentz.contrContrContractField.basis_left {d : ℕ} {v : ↑(Contr d).V} (μ : Fin 1 ⊕ Fin d) : contrContrContractField (ContrMod.stdBasis μ ⊗ₜ[ℝ] v) = minkowskiMatrix μ μ * ContrMod.toFin1dℝ v μ

theorem Lorentz.contrContrContractField.on_basis_mulVec {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} (μ ν : Fin 1 ⊕ Fin d) : contrContrContractField (ContrMod.stdBasis μ ⊗ₜ[ℝ] ContrMod.mulVec Λ (ContrMod.stdBasis ν)) = minkowskiMatrix μ μ * Λ μ ν

theorem Lorentz.contrContrContractField.on_basis {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : contrContrContractField (ContrMod.stdBasis μ ⊗ₜ[ℝ] ContrMod.stdBasis ν) = minkowskiMatrix μ ν

theorem Lorentz.contrContrContractField.matrix_apply_stdBasis {d : ℕ} {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ} (ν μ : Fin 1 ⊕ Fin d) : Λ ν μ = minkowskiMatrix ν ν * contrContrContractField (ContrMod.stdBasis ν ⊗ₜ[ℝ] ContrMod.mulVec Λ (ContrMod.stdBasis μ))

Self-adjoint

theorem Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint (x : ContrMod 3) : ↑(contrContrContractField (x ⊗ₜ[ℝ] x)) = (↑(ContrMod.toSelfAdjoint x)).det