Metric for real Lorentz vectors

def Lorentz.preContrMetricVal (d : ℕ := 3) : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d) (Contr d)).V

The metric ηᵃᵃ as an element of (Contr d ⊗ Contr d).V.

Equations

• Lorentz.preContrMetricVal d = Lorentz.contrContrToMatrixRe.symm minkowskiMatrix

theorem Lorentz.preContrMetricVal_expand_tmul {d : ℕ} : preContrMetricVal d = (contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) - ∑ i : Fin d, (contrBasis d) (Sum.inr i) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr i)

Expansion of preContrMetricVal into basis.

theorem Lorentz.preContrMetricVal_expand_tmul_minkowskiMatrix {d : ℕ} : preContrMetricVal d = ∑ i : Fin 1 ⊕ Fin d, minkowskiMatrix i i • (contrBasis d) i ⊗ₜ[ℝ] (contrBasis d) i

def Lorentz.preContrMetric (d : ℕ := 3) : 𝟙_ (Rep ℝ ↑(LorentzGroup d)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d) (Contr d)

The metric ηᵃᵃ as a morphism 𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ Contr d ⊗ Contr d, making its invariance under the action of LorentzGroup d.

Equations

• Lorentz.preContrMetric d = { hom := ModuleCat.ofHom { toFun := fun (a : ℝ) => a • Lorentz.preContrMetricVal d, map_add' := ⋯, map_smul' := ⋯ }, comm := ⋯ }

theorem Lorentz.preContrMetric_apply_one {d : ℕ} : (CategoryTheory.ConcreteCategory.hom (preContrMetric d).hom) 1 = preContrMetricVal d

def Lorentz.preCoMetricVal (d : ℕ := 3) : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d) (Co d)).V

The metric ηᵢᵢ as an element of (Co d ⊗ Co d).V.

Equations

• Lorentz.preCoMetricVal d = Lorentz.coCoToMatrixRe.symm minkowskiMatrix

theorem Lorentz.preCoMetricVal_expand_tmul {d : ℕ} : preCoMetricVal d = (coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) - ∑ i : Fin d, (coBasis d) (Sum.inr i) ⊗ₜ[ℝ] (coBasis d) (Sum.inr i)

Expansion of preContrMetricVal into basis.

theorem Lorentz.preCoMetricVal_expand_tmul_minkowskiMatrix {d : ℕ} : preCoMetricVal d = ∑ i : Fin 1 ⊕ Fin d, minkowskiMatrix i i • (coBasis d) i ⊗ₜ[ℝ] (coBasis d) i

def Lorentz.preCoMetric (d : ℕ := 3) : 𝟙_ (Rep ℝ ↑(LorentzGroup d)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d) (Co d)

The metric ηᵢᵢ as a morphism 𝟙_ (Rep ℂ (LorentzGroup d))) ⟶ Co d ⊗ Co d, making its invariance under the action of LorentzGroup d.

Equations

• Lorentz.preCoMetric d = { hom := ModuleCat.ofHom { toFun := fun (a : ℝ) => a • Lorentz.preCoMetricVal d, map_add' := ⋯, map_smul' := ⋯ }, comm := ⋯ }

theorem Lorentz.preCoMetric_apply_one {d : ℕ} : (CategoryTheory.ConcreteCategory.hom (preCoMetric d).hom) 1 = preCoMetricVal d

Contraction of metrics

theorem Lorentz.contrCoContract_apply_metric {d : ℕ} : (CategoryTheory.ConcreteCategory.hom (β_ (Contr d) (Co d)).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Contr d).V (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Co d).V).hom)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Contr d).V (CategoryTheory.MonoidalCategoryStruct.whiskerRight contrCoContract.hom (Co d).V))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Contr d).V (CategoryTheory.MonoidalCategoryStruct.associator (Contr d).V (Co d).V (Co d).V).inv)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator (Contr d).V (Contr d).V (CategoryTheory.MonoidalCategoryStruct.tensorObj (Co d).V (Co d).V)).hom) ((CategoryTheory.ConcreteCategory.hom (preContrMetric d).hom) 1 ⊗ₜ[ℝ] (CategoryTheory.ConcreteCategory.hom (preCoMetric d).hom) 1))))) = (CategoryTheory.ConcreteCategory.hom (preCoContrUnit d).hom) 1

theorem Lorentz.coContrContract_apply_metric {d : ℕ} : (CategoryTheory.ConcreteCategory.hom (β_ (Co d) (Contr d)).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Co d).V (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Contr d).V).hom)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Co d).V (CategoryTheory.MonoidalCategoryStruct.whiskerRight coContrContract.hom (Contr d).V))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Co d).V (CategoryTheory.MonoidalCategoryStruct.associator (Co d).V (Contr d).V (Contr d).V).inv)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator (Co d).V (Co d).V (CategoryTheory.MonoidalCategoryStruct.tensorObj (Contr d).V (Contr d).V)).hom) ((CategoryTheory.ConcreteCategory.hom (preCoMetric d).hom) 1 ⊗ₜ[ℝ] (CategoryTheory.ConcreteCategory.hom (preContrMetric d).hom) 1))))) = (CategoryTheory.ConcreteCategory.hom (preContrCoUnit d).hom) 1