PhysLean Documentation

PhysLean.Relativity.Lorentz.ComplexVector.Two

Tensor products of two complex Lorentz vectors #

source
def Lorentz.contrContrToMatrix :
↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr complexContr).V ≃ₗ[ℂ] Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ

Equivalence of complexContr ⊗ complexContr to 4 x 4 complex matrices.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Lorentz.contrContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
    contrContrToMatrix.symm M = ∑ i : Fin 1 ⊕ Fin 3, ∑ j : Fin 1 ⊕ Fin 3, M i j • complexContrBasis i ⊗ₜ[ℂ] complexContrBasis j

    Expanding contrContrToMatrix in terms of the standard basis.

    source
    def Lorentz.coCoToMatrix :
    ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexCo complexCo).V ≃ₗ[ℂ] Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ

    Equivalence of complexCo ⊗ complexCo to 4 x 4 complex matrices.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Lorentz.coCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
      coCoToMatrix.symm M = ∑ i : Fin 1 ⊕ Fin 3, ∑ j : Fin 1 ⊕ Fin 3, M i j • complexCoBasis i ⊗ₜ[ℂ] complexCoBasis j

      Expanding coCoToMatrix in terms of the standard basis.

      source
      def Lorentz.contrCoToMatrix :
      ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr complexCo).V ≃ₗ[ℂ] Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ

      Equivalence of complexContr ⊗ complexCo to 4 x 4 complex matrices.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Lorentz.contrCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
        contrCoToMatrix.symm M = ∑ i : Fin 1 ⊕ Fin 3, ∑ j : Fin 1 ⊕ Fin 3, M i j • complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j

        Expansion of contrCoToMatrix in terms of the standard basis.

        source
        def Lorentz.coContrToMatrix :
        ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexCo complexContr).V ≃ₗ[ℂ] Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ

        Equivalence of complexCo ⊗ complexContr to 4 x 4 complex matrices.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Lorentz.coContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
          coContrToMatrix.symm M = ∑ i : Fin 1 ⊕ Fin 3, ∑ j : Fin 1 ⊕ Fin 3, M i j • complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j

          Expansion of coContrToMatrix in terms of the standard basis.

          Group actions #

          source
          theorem Lorentz.contrContrToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr complexContr).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          contrContrToMatrix ((TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) v) = LorentzGroup.toComplex (SL2C.toLorentzGroup M) * contrContrToMatrix v * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)).transpose
          source
          theorem Lorentz.coCoToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexCo complexCo).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          coCoToMatrix ((TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) v) = (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹.transpose * coCoToMatrix v * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹
          source
          theorem Lorentz.contrCoToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexContr complexCo).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          contrCoToMatrix ((TensorProduct.map (complexContr.ρ M) (complexCo.ρ M)) v) = LorentzGroup.toComplex (SL2C.toLorentzGroup M) * contrCoToMatrix v * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹
          source
          theorem Lorentz.coContrToMatrix_ρ (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj complexCo complexContr).V) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          coContrToMatrix ((TensorProduct.map (complexCo.ρ M) (complexContr.ρ M)) v) = (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹.transpose * coContrToMatrix v * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)).transpose

          The symm version of the group actions. #

          source
          theorem Lorentz.contrContrToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) (contrContrToMatrix.symm v) = contrContrToMatrix.symm (LorentzGroup.toComplex (SL2C.toLorentzGroup M) * v * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)).transpose)
          source
          theorem Lorentz.coCoToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) (coCoToMatrix.symm v) = coCoToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹.transpose * v * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹)
          source
          theorem Lorentz.contrCoToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          (TensorProduct.map (complexContr.ρ M) (complexCo.ρ M)) (contrCoToMatrix.symm v) = contrCoToMatrix.symm (LorentzGroup.toComplex (SL2C.toLorentzGroup M) * v * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹)
          source
          theorem Lorentz.coContrToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) :
          (TensorProduct.map (complexCo.ρ M) (complexContr.ρ M)) (coContrToMatrix.symm v) = coContrToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹.transpose * v * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)).transpose)