Metric for complex Lorentz vectors

def Lorentz.contrMetricVal : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr complexContr).V

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

Equations

• Lorentz.contrMetricVal = Lorentz.contrContrToMatrix.symm (minkowskiMatrix.map ⇑Complex.ofRealHom)

theorem Lorentz.contrMetricVal_expand_tmul : contrMetricVal = complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)

The expansion of contrMetricVal into basis vectors.

def Lorentz.contrMetric : 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr complexContr

The metric ηᵃᵃ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr, making its invariance under the action of SL(2,ℂ).

Equations

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

theorem Lorentz.contrMetric_apply_one : (CategoryTheory.ConcreteCategory.hom contrMetric.hom) 1 = contrMetricVal

def Lorentz.coMetricVal : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexCo complexCo).V

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

Equations

• Lorentz.coMetricVal = Lorentz.coCoToMatrix.symm (minkowskiMatrix.map ⇑Complex.ofRealHom)

theorem Lorentz.coMetricVal_expand_tmul : coMetricVal = complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)

The expansion of coMetricVal into basis vectors.

def Lorentz.coMetric : 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj complexCo complexCo

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

Equations

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

theorem Lorentz.coMetric_apply_one : (CategoryTheory.ConcreteCategory.hom coMetric.hom) 1 = coMetricVal

Contraction of metrics

theorem Lorentz.contrCoContraction_apply_metric : (CategoryTheory.ConcreteCategory.hom (β_ complexContr complexCo).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft complexContr.V (CategoryTheory.MonoidalCategoryStruct.leftUnitor complexCo.V).hom)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft complexContr.V (CategoryTheory.MonoidalCategoryStruct.whiskerRight contrCoContraction.hom complexCo.V))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft complexContr.V (CategoryTheory.MonoidalCategoryStruct.associator complexContr.V complexCo.V complexCo.V).inv)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator complexContr.V complexContr.V (CategoryTheory.MonoidalCategoryStruct.tensorObj complexCo.V complexCo.V)).hom) ((CategoryTheory.ConcreteCategory.hom contrMetric.hom) 1 ⊗ₜ[ℂ] (CategoryTheory.ConcreteCategory.hom coMetric.hom) 1))))) = (CategoryTheory.ConcreteCategory.hom coContrUnit.hom) 1

theorem Lorentz.coContrContraction_apply_metric : (CategoryTheory.ConcreteCategory.hom (β_ complexCo complexContr).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft complexCo.V (CategoryTheory.MonoidalCategoryStruct.leftUnitor complexContr.V).hom)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft complexCo.V (CategoryTheory.MonoidalCategoryStruct.whiskerRight coContrContraction.hom complexContr.V))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft complexCo.V (CategoryTheory.MonoidalCategoryStruct.associator complexCo.V complexContr.V complexContr.V).inv)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator complexCo.V complexCo.V (CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr.V complexContr.V)).hom) ((CategoryTheory.ConcreteCategory.hom coMetric.hom) 1 ⊗ₜ[ℂ] (CategoryTheory.ConcreteCategory.hom contrMetric.hom) 1))))) = (CategoryTheory.ConcreteCategory.hom contrCoUnit.hom) 1