Documentation

PhysLean.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic

Complex Lorentz vectors #

We define complex Lorentz vectors in 4d space-time as representations of SL(2, C).

source
def Lorentz.complexContr :
Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)

The representation of SL(2, ℂ) on complex vectors corresponding to contravariant Lorentz vectors. In index notation these have an up index ψⁱ.

Equations
    Instances For
      source
      def Lorentz.complexCo :
      Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)

      The representation of SL(2, ℂ) on complex vectors corresponding to contravariant Lorentz vectors. In index notation these have a down index ψⁱ.

      Equations
        Instances For
          source
          def Lorentz.complexContrBasis :
          Module.Basis (Fin 1 ⊕ Fin 3) ℂ ↑complexContr.V

          The standard basis of complex contravariant Lorentz vectors.

          Equations
            Instances For
              source
              @[simp]
              theorem Lorentz.complexContrBasis_toFin13ℂ (i : Fin 1 ⊕ Fin 3) :
              ContrℂModule.toFin13ℂ (complexContrBasis i) = Pi.single i 1
              source
              @[simp]
              theorem Lorentz.complexContrBasis_ρ_apply (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (i j : Fin 1 ⊕ Fin 3) :
              (LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M) i j = LorentzGroup.toComplex (SL2C.toLorentzGroup M) i j
              source
              theorem Lorentz.complexContrBasis_ρ_val (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (v : ↑complexContr.V) :
              ((complexContr.ρ M) v).val = (LorentzGroup.toComplex (SL2C.toLorentzGroup M)).mulVec v.val
              source
              def Lorentz.complexContrBasisFin4 :
              Module.Basis (Fin 4) ℂ ↑complexContr.V

              The standard basis of complex contravariant Lorentz vectors indexed by Fin 4.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem Lorentz.complexContrBasisFin4_apply_zero :
                  complexContrBasisFin4 0 = complexContrBasis (Sum.inl 0)
                  source
                  @[simp]
                  theorem Lorentz.complexContrBasisFin4_apply_one :
                  complexContrBasisFin4 1 = complexContrBasis (Sum.inr 0)
                  source
                  @[simp]
                  theorem Lorentz.complexContrBasisFin4_apply_two :
                  complexContrBasisFin4 2 = complexContrBasis (Sum.inr 1)
                  source
                  @[simp]
                  theorem Lorentz.complexContrBasisFin4_apply_three :
                  complexContrBasisFin4 3 = complexContrBasis (Sum.inr 2)
                  source
                  @[simp]
                  theorem Lorentz.complexContrBasisFin4_apply_succ (i : Fin 3) :
                  complexContrBasisFin4 i.succ = complexContrBasis (Sum.inr i)
                  source
                  def Lorentz.complexCoBasis :
                  Module.Basis (Fin 1 ⊕ Fin 3) ℂ ↑complexCo.V

                  The standard basis of complex covariant Lorentz vectors.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem Lorentz.complexCoBasis_toFin13ℂ (i : Fin 1 ⊕ Fin 3) :
                      CoℂModule.toFin13ℂ (complexCoBasis i) = Pi.single i 1
                      source
                      @[simp]
                      theorem Lorentz.complexCoBasis_ρ_apply (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (i j : Fin 1 ⊕ Fin 3) :
                      (LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M) i j = (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹.transpose i j
                      source
                      def Lorentz.complexCoBasisFin4 :
                      Module.Basis (Fin 4) ℂ ↑complexCo.V

                      The standard basis of complex covariant Lorentz vectors indexed by Fin 4.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem Lorentz.complexCoBasisFin4_apply_zero :
                          complexCoBasisFin4 0 = complexCoBasis (Sum.inl 0)
                          source
                          @[simp]
                          theorem Lorentz.complexCoBasisFin4_apply_one :
                          complexCoBasisFin4 1 = complexCoBasis (Sum.inr 0)
                          source
                          @[simp]
                          theorem Lorentz.complexCoBasisFin4_apply_two :
                          complexCoBasisFin4 2 = complexCoBasis (Sum.inr 1)
                          source
                          @[simp]
                          theorem Lorentz.complexCoBasisFin4_apply_three :
                          complexCoBasisFin4 3 = complexCoBasis (Sum.inr 2)

                          Relation to real #

                          source
                          def Lorentz.inclCongrRealLorentz :
                          ContrMod 3 →ₛₗ[Complex.ofRealHom] ↑complexContr.V

                          The semilinear map including real Lorentz vectors into complex contravariant lorentz vectors.

                          Equations
                            Instances For
                              source
                              theorem Lorentz.inclCongrRealLorentz_val (v : ContrMod 3) :
                              (inclCongrRealLorentz v).val = ⇑Complex.ofRealHom ∘ v.toFin1dℝ
                              source
                              theorem Lorentz.complexContrBasis_of_real (i : Fin 1 ⊕ Fin 3) :
                              complexContrBasis i = inclCongrRealLorentz (ContrMod.stdBasis i)
                              source
                              theorem Lorentz.inclCongrRealLorentz_ρ (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (v : ContrMod 3) :
                              (complexContr.ρ M) (inclCongrRealLorentz v) = inclCongrRealLorentz (((Contr 3).ρ (SL2C.toLorentzGroup M)) v)
                              source
                              theorem Lorentz.SL2CRep_ρ_basis (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (i : Fin 1 ⊕ Fin 3) :
                              (complexContr.ρ M) (complexContrBasis i) = ∑ j : Fin 1 ⊕ Fin 3, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j