HepLean Documentation

HepLean.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) ℂ (CoeSort.coe Lorentz.complexContr)

      The standard basis of complex contravariant Lorentz vectors.

      Equations
      Instances For
        source
        @[simp]
        theorem Lorentz.complexContrBasis_toFin13ℂ (i : Fin 1 ⊕ Fin 3) :
        Lorentz.ContrℂModule.toFin13ℂ (Lorentz.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 Lorentz.complexContrBasis Lorentz.complexContrBasis) (Lorentz.complexContr.ρ M) i j = LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup M) i j
        source
        theorem Lorentz.complexContrBasis_ρ_val (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (v : CoeSort.coe Lorentz.complexContr) :
        ((Lorentz.complexContr.ρ M) v).val = (LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup M)).mulVec v.val
        source
        def Lorentz.complexContrBasisFin4 :
        Basis (Fin 4) ℂ (CoeSort.coe Lorentz.complexContr)

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

        Equations
        Instances For
          source
          def Lorentz.complexCoBasis :
          Basis (Fin 1 ⊕ Fin 3) ℂ (CoeSort.coe Lorentz.complexCo)

          The standard basis of complex covariant Lorentz vectors.

          Equations
          Instances For
            source
            @[simp]
            theorem Lorentz.complexCoBasis_toFin13ℂ (i : Fin 1 ⊕ Fin 3) :
            Lorentz.CoℂModule.toFin13ℂ (Lorentz.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 Lorentz.complexCoBasis Lorentz.complexCoBasis) (Lorentz.complexCo.ρ M) i j = (LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup M))⁻¹.transpose i j
            source
            def Lorentz.complexCoBasisFin4 :
            Basis (Fin 4) ℂ (CoeSort.coe Lorentz.complexCo)

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

            Equations
            Instances For

              Relation to real #

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

              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 : Lorentz.ContrMod 3) :
                (Lorentz.inclCongrRealLorentz v).val = ⇑Complex.ofRealHom ∘ v.toFin1dℝ
                source
                theorem Lorentz.complexContrBasis_of_real (i : Fin 1 ⊕ Fin 3) :
                Lorentz.complexContrBasis i = Lorentz.inclCongrRealLorentz (Lorentz.ContrMod.stdBasis i)
                source
                theorem Lorentz.inclCongrRealLorentz_ρ (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (v : Lorentz.ContrMod 3) :
                (Lorentz.complexContr.ρ M) (Lorentz.inclCongrRealLorentz v) = Lorentz.inclCongrRealLorentz (((Lorentz.Contr 3).ρ (Lorentz.SL2C.toLorentzGroup M)) v)

                TODO: Rename.

                source
                theorem Lorentz.SL2CRep_ρ_basis (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (i : Fin 1 ⊕ Fin 3) :
                (Lorentz.complexContr.ρ M) (Lorentz.complexContrBasis i) = ∑ j : Fin 1 ⊕ Fin 3, ↑(Lorentz.SL2C.toLorentzGroup M) j i • Lorentz.complexContrBasis j

                TODO: Include relation to real Lorentz vectors.