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) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (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 := ⋯ }

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) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (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 := ⋯ }

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) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (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

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) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (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

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

The contraction on the basis

theorem Lorentz.contrCoContract_basis {d : ℕ} (i j : Fin 1 ⊕ Fin d) : (CategoryTheory.ConcreteCategory.hom contrCoContract.hom) ((contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j) = if i = j then 1 else 0

theorem Lorentz.coContrContract_basis {d : ℕ} (i j : Fin 1 ⊕ Fin d) : (CategoryTheory.ConcreteCategory.hom coContrContract.hom) ((coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j) = if i = j then 1 else 0