PhysLean Documentation

PhysLean.Relativity.Lorentz.ComplexVector.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 :
      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 :
        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 :
          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 :
            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
              • One or more equations did not get rendered due to their size.
              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