PhysLean Documentation

PhysLean.Relativity.Tensors.RealTensor.Vector.Pre.Basic

Real Lorentz vectors #

We define real Lorentz vectors in as representations of the Lorentz group.

source
def Lorentz.Contr (d : ℕ) :
Rep ℝ ↑(LorentzGroup d)

The representation of LorentzGroup d on real vectors corresponding to contravariant Lorentz vectors. In index notation these have an up index ψⁱ.

Equations
Instances For
    source
    def Lorentz.contrBasis (d : ℕ := 3) :
    Basis (Fin 1 ⊕ Fin d) ℝ ↑(Contr d).V

    The standard basis of contravariant Lorentz vectors.

    Equations
    Instances For
      source
      @[simp]
      theorem Lorentz.contrBasis_ρ_apply {d : ℕ} (M : ↑(LorentzGroup d)) (i j : Fin 1 ⊕ Fin d) :
      (LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M) i j = ↑M i j
      source
      @[simp]
      theorem Lorentz.contrBasis_toFin1dℝ {d : ℕ} (i : Fin 1 ⊕ Fin d) :
      ContrMod.toFin1dℝ ((contrBasis d) i) = Pi.single i 1
      source
      def Lorentz.contrBasisFin (d : ℕ := 3) :
      Basis (Fin (1 + d)) ℝ ↑(Contr d).V

      The standard basis of contravariant Lorentz vectors indexed by Fin (1 + d).

      Equations
      Instances For
        source
        @[simp]
        theorem Lorentz.contrBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) :
        ContrMod.toFin1dℝ ((contrBasisFin d) i) = Pi.single (finSumFinEquiv.symm i) 1
        source
        theorem Lorentz.contrBasisFin_repr_apply {d : ℕ} (p : ↑(Contr d).V) (i : Fin (1 + d)) :
        ((contrBasisFin d).repr p) i = p.val (finSumFinEquiv.symm i)
        source
        instance Lorentz.instTopologicalSpaceCarrierRealVModuleCatElemMatrixSumFinOfNatNatLorentzGroupContr {d : ℕ} :
        TopologicalSpace ↑(Contr d).V

        The representation of contravariant Lorentz vectors forms a topological space, induced by its equivalence to Fin 1 ⊕ Fin d → ℝ.

        Equations
        source
        theorem Lorentz.continuous_contr {d : ℕ} {T : Type} [TopologicalSpace T] (f : T → ↑(Contr d).V) (h : Continuous fun (i : T) => ContrMod.toFin1dℝ (f i)) :
        Continuous f
        source
        theorem Lorentz.contr_continuous {d : ℕ} {T : Type} [TopologicalSpace T] (f : ↑(Contr d).V → T) (h : Continuous (f ∘ ⇑ContrMod.toFin1dℝEquiv.symm)) :
        Continuous f
        source
        def Lorentz.Co (d : ℕ) :
        Rep ℝ ↑(LorentzGroup d)

        The representation of LorentzGroup d on real vectors corresponding to covariant Lorentz vectors. In index notation these have an up index ψⁱ.

        Equations
        Instances For
          source
          def Lorentz.coBasis (d : ℕ := 3) :
          Basis (Fin 1 ⊕ Fin d) ℝ ↑(Co d).V

          The standard basis of contravariant Lorentz vectors.

          Equations
          Instances For
            source
            @[simp]
            theorem Lorentz.coBasis_ρ_apply {d : ℕ} (M : ↑(LorentzGroup d)) (i j : Fin 1 ⊕ Fin d) :
            (LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M) i j = (↑M)⁻¹.transpose i j
            source
            @[simp]
            theorem Lorentz.coBasis_toFin1dℝ {d : ℕ} (i : Fin 1 ⊕ Fin d) :
            CoMod.toFin1dℝ ((coBasis d) i) = Pi.single i 1
            source
            def Lorentz.coBasisFin (d : ℕ := 3) :
            Basis (Fin (1 + d)) ℝ ↑(Co d).V

            The standard basis of covaraitn Lorentz vectors indexed by Fin (1 + d).

            Equations
            Instances For
              source
              @[simp]
              theorem Lorentz.coBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) :
              CoMod.toFin1dℝ ((coBasisFin d) i) = Pi.single (finSumFinEquiv.symm i) 1

              Isomorphism between contravariant and covariant Lorentz vectors #

              source
              def Lorentz.Contr.toCo (d : ℕ) :
              Contr d ⟶ Co d

              The morphism of representations from Contr d to Co d defined by multiplication with the metric.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lorentz.Co.toContr (d : ℕ) :
                Co d ⟶ Contr d

                The morphism of representations from Co d to Contr d defined by multiplication with the metric.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Lorentz.contrIsoCo (d : ℕ) :
                  Contr d ≅ Co d

                  The isomorphism between Contr d and Co d induced by multiplication with the Minkowski metric.

                  Equations
                  Instances For

                    Other properties #

                    source
                    theorem Lorentz.Contr.ρ_stdBasis (μ : Fin 1 ⊕ Fin 3) (Λ : ↑(LorentzGroup 3)) :
                    ((Contr 3).ρ Λ) (ContrMod.stdBasis μ) = ∑ j : Fin 1 ⊕ Fin 3, ↑Λ j μ • ContrMod.stdBasis j