Unit for complex Lorentz vectors

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

The contra-co unit for complex lorentz vectors. Usually denoted δⁱᵢ.

Equations

• Lorentz.preContrCoUnitVal d = Lorentz.contrCoToMatrixRe.symm 1

theorem Lorentz.preContrCoUnitVal_expand_tmul {d : ℕ} : preContrCoUnitVal d = ∑ i : Fin 1 ⊕ Fin d, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i

Expansion of preContrCoUnitVal into basis.

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

The contra-co unit for complex lorentz vectors as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo, manifesting the invariance under the SL(2, ℂ) action.

Equations

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

theorem Lorentz.preContrCoUnit_apply_one {d : ℕ} : (CategoryTheory.ConcreteCategory.hom (preContrCoUnit d).hom) 1 = preContrCoUnitVal d

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

The co-contra unit for complex lorentz vectors. Usually denoted δᵢⁱ.

Equations

• Lorentz.preCoContrUnitVal d = Lorentz.coContrToMatrixRe.symm 1

theorem Lorentz.preCoContrUnitVal_expand_tmul {d : ℕ} : preCoContrUnitVal d = ∑ i : Fin 1 ⊕ Fin d, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i

Expansion of preCoContrUnitVal into basis.

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

The co-contra unit for complex lorentz vectors as a morphism 𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ Co d ⊗ Contr d, manifesting the invariance under the LorentzGroup d action.

Equations

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

theorem Lorentz.preCoContrUnit_apply_one {d : ℕ} : (CategoryTheory.ConcreteCategory.hom (preCoContrUnit d).hom) 1 = preCoContrUnitVal d

Contraction of the units

theorem Lorentz.contr_preContrCoUnit {d : ℕ} (x : ↑(Co d).V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Co d)).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight coContrContract (Co d)).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator (Co d) (Contr d) (Co d)).inv.hom) (x ⊗ₜ[ℝ] (CategoryTheory.ConcreteCategory.hom (preContrCoUnit d).hom) 1))) = x

Contraction on the right with contrCoUnit does nothing.

theorem Lorentz.contr_preCoContrUnit {d : ℕ} (x : ↑(Contr d).V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Contr d)).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight contrCoContract (Contr d)).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator (Contr d) (Co d) (Contr d)).inv.hom) (x ⊗ₜ[ℝ] (CategoryTheory.ConcreteCategory.hom (preCoContrUnit d).hom) 1))) = x

Contraction on the right with coContrUnit.

Symmetry properties of the units

theorem Lorentz.preContrCoUnit_symm {d : ℕ} : (CategoryTheory.ConcreteCategory.hom (preContrCoUnit d).hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Contr d) (CategoryTheory.CategoryStruct.id (Co d))).hom) ((CategoryTheory.ConcreteCategory.hom (β_ (Co d) (Contr d)).hom.hom) ((CategoryTheory.ConcreteCategory.hom (preCoContrUnit d).hom) 1))

theorem Lorentz.preCoContrUnit_symm {d : ℕ} : (CategoryTheory.ConcreteCategory.hom (preCoContrUnit d).hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Co d) (CategoryTheory.CategoryStruct.id (Contr d))).hom) ((CategoryTheory.ConcreteCategory.hom (β_ (Contr d) (Co d)).hom.hom) ((CategoryTheory.ConcreteCategory.hom (preContrCoUnit d).hom) 1))