Contraction of Lorentz vectors

def Lorentz.contrCoContrBi : ↑complexContr.V →ₗ[ℂ] ↑complexCo.V →ₗ[ℂ] ℂ

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.contrContrCoBi : ↑complexCo.V →ₗ[ℂ] ↑complexContr.V →ₗ[ℂ] ℂ

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.contrCoContraction : CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr complexCo ⟶ 𝟙_ (Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ))

The linear map from complexContr ⊗ complexCo 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.contrCoContraction = { hom := ModuleCat.ofHom (TensorProduct.lift Lorentz.contrCoContrBi), comm := Lorentz.contrCoContraction.proof_1 }

theorem Lorentz.contrCoContraction_hom_tmul (ψ : ↑complexContr.V) (φ : ↑complexCo.V) : (CategoryTheory.ConcreteCategory.hom contrCoContraction.hom) (ψ ⊗ₜ[ℂ] φ) = ContrℂModule.toFin13ℂ ψ ⬝ᵥ CoℂModule.toFin13ℂ φ

theorem Lorentz.contrCoContraction_basis (i j : Fin 4) : (CategoryTheory.ConcreteCategory.hom contrCoContraction.hom) (complexContrBasisFin4 i ⊗ₜ[ℂ] complexCoBasisFin4 j) = if ↑i = ↑j then 1 else 0

theorem Lorentz.contrCoContraction_basis' (i j : Fin 1 ⊕ Fin 3) : (CategoryTheory.ConcreteCategory.hom contrCoContraction.hom) (complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j) = if i = j then 1 else 0

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

The linear map from complexCo ⊗ complexContr to ℂ given by summing over components of covariant Lorentz vector and contravariant Lorentz vector in the standard basis (i.e. the dot product). In terms of index notation this is the contraction is φᵢ ψⁱ.

Equations

• Lorentz.coContrContraction = { hom := ModuleCat.ofHom (TensorProduct.lift Lorentz.contrContrCoBi), comm := Lorentz.coContrContraction.proof_1 }

theorem Lorentz.coContrContraction_hom_tmul (φ : ↑complexCo.V) (ψ : ↑complexContr.V) : (CategoryTheory.ConcreteCategory.hom coContrContraction.hom) (φ ⊗ₜ[ℂ] ψ) = CoℂModule.toFin13ℂ φ ⬝ᵥ ContrℂModule.toFin13ℂ ψ

theorem Lorentz.coContrContraction_basis (i j : Fin 4) : (CategoryTheory.ConcreteCategory.hom coContrContraction.hom) (complexCoBasisFin4 i ⊗ₜ[ℂ] complexContrBasisFin4 j) = if ↑i = ↑j then 1 else 0

theorem Lorentz.coContrContraction_basis' (i j : Fin 1 ⊕ Fin 3) : (CategoryTheory.ConcreteCategory.hom coContrContraction.hom) (complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j) = if i = j then 1 else 0

Symmetry

theorem Lorentz.contrCoContraction_tmul_symm (φ : ↑complexContr.V) (ψ : ↑complexCo.V) : (CategoryTheory.ConcreteCategory.hom contrCoContraction.hom) (φ ⊗ₜ[ℂ] ψ) = (CategoryTheory.ConcreteCategory.hom coContrContraction.hom) (ψ ⊗ₜ[ℂ] φ)

theorem Lorentz.coContrContraction_tmul_symm (φ : ↑complexCo.V) (ψ : ↑complexContr.V) : (CategoryTheory.ConcreteCategory.hom coContrContraction.hom) (φ ⊗ₜ[ℂ] ψ) = (CategoryTheory.ConcreteCategory.hom contrCoContraction.hom) (ψ ⊗ₜ[ℂ] φ)