Metric for real Lorentz vectors

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

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

noncomputable def Lorentz.preContrMetric (d : ℕ := 3) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (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 = Rep.ofHom { toFun := fun (a : ℝ) => a • Lorentz.preContrMetricVal d, map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }

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

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

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

noncomputable def Lorentz.preCoMetric (d : ℕ := 3) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (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 = Rep.ofHom { toFun := fun (a : ℝ) => a • Lorentz.preCoMetricVal d, map_add' := ⋯, map_smul' := ⋯, isIntertwining' := ⋯ }

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

Contraction of metrics

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

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