PhysLean Documentation

PhysLean.Relativity.Lorentz.ComplexVector.Unit

Unit for complex Lorentz vectors #

source
def Lorentz.contrCoUnitVal :
↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr complexCo).V

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

Equations
Instances For
    source
    theorem Lorentz.contrCoUnitVal_expand_tmul :
    contrCoUnitVal = complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)

    Expansion of contrCoUnitVal into basis.

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

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Lorentz.contrCoUnit_apply_one :
      (CategoryTheory.ConcreteCategory.hom contrCoUnit.hom) 1 = contrCoUnitVal
      source
      def Lorentz.coContrUnitVal :
      ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexCo complexContr).V

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

      Equations
      Instances For
        source
        theorem Lorentz.coContrUnitVal_expand_tmul :
        coContrUnitVal = complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)

        Expansion of coContrUnitVal into basis.

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

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Lorentz.coContrUnit_apply_one :
          (CategoryTheory.ConcreteCategory.hom coContrUnit.hom) 1 = coContrUnitVal

          Contraction of the units #

          source
          theorem Lorentz.contr_contrCoUnit (x : ↑complexCo.V) :
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor complexCo).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight coContrContraction complexCo).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator complexCo complexContr complexCo).inv.hom) (x ⊗ₜ[ℂ] (CategoryTheory.ConcreteCategory.hom contrCoUnit.hom) 1))) = x

          Contraction on the right with contrCoUnit does nothing.

          source
          theorem Lorentz.contr_coContrUnit (x : ↑complexContr.V) :
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor complexContr).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight contrCoContraction complexContr).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator complexContr complexCo complexContr).inv.hom) (x ⊗ₜ[ℂ] (CategoryTheory.ConcreteCategory.hom coContrUnit.hom) 1))) = x

          Contraction on the right with coContrUnit.

          Symmetry properties of the units #

          source
          theorem Lorentz.contrCoUnit_symm :
          (CategoryTheory.ConcreteCategory.hom contrCoUnit.hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft complexContr (CategoryTheory.CategoryStruct.id complexCo)).hom) ((CategoryTheory.ConcreteCategory.hom (β_ complexCo complexContr).hom.hom) ((CategoryTheory.ConcreteCategory.hom coContrUnit.hom) 1))
          source
          theorem Lorentz.coContrUnit_symm :
          (CategoryTheory.ConcreteCategory.hom coContrUnit.hom) 1 = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft complexCo (CategoryTheory.CategoryStruct.id complexContr)).hom) ((CategoryTheory.ConcreteCategory.hom (β_ complexContr complexCo).hom.hom) ((CategoryTheory.ConcreteCategory.hom contrCoUnit.hom) 1))