PhysLean Documentation

PhysLean.Relativity.Lorentz.Bispinors.Basic

Bispinors #

Definitions #

source
def complexLorentzTensor.contrBispinorUp (p : ↑Lorentz.complexContr.V) :
↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ((Sum.elim ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1) ![Color.up] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 2))).V

A bispinor pᵃᵃ created from a lorentz vector p^μ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def complexLorentzTensor.contrBispinorDown (p : ↑Lorentz.complexContr.V) :
    ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk (((Sum.elim (Sum.elim ![Color.downL, Color.downL] ![Color.downR, Color.downR] ∘ ⇑finSumFinEquiv.symm) ((Sum.elim ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1) ![Color.up] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 2) ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 3) ∘ Fin.succAbove 1 ∘ Fin.succAbove 2))).V

    A bispinor pₐₐ created from a lorentz vector p^μ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def complexLorentzTensor.coBispinorUp (p : ↑Lorentz.complexCo.V) :
      ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk ((Sum.elim ![Color.up, Color.upL, Color.upR] ![Color.down] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 2))).V

      A bispinor pᵃᵃ created from a lorentz vector p_μ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def complexLorentzTensor.coBispinorDown (p : ↑Lorentz.complexCo.V) :
        ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk (((Sum.elim (Sum.elim ![Color.downL, Color.downL] ![Color.downR, Color.downR] ∘ ⇑finSumFinEquiv.symm) ((Sum.elim ![Color.up, Color.upL, Color.upR] ![Color.down] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 2) ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 0 ∘ Fin.succAbove 3) ∘ Fin.succAbove 1 ∘ Fin.succAbove 2))).V

        A bispinor pₐₐ created from a lorentz vector p_μ.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Tensor nodes #

          source
          theorem complexLorentzTensor.tensorNode_contrBispinorUp (p : ↑Lorentz.complexContr.V) :
          (TensorTree.tensorNode (contrBispinorUp p)).tensor = (TensorTree.contr 0 2 ⋯ ((TensorTree.tensorNode PauliMatrix.pauliCo).prod (TensorTree.tensorNode (TensorTree.vecNodeE complexLorentzTensor Color.up p).tensor))).tensor

          The definitional tensor node relation for contrBispinorUp.

          source
          theorem complexLorentzTensor.tensorNode_contrBispinorDown (p : ↑Lorentz.complexContr.V) :
          (TensorTree.tensorNode (contrBispinorDown p)).tensor = (TensorTree.contr 1 2 ⋯ (TensorTree.contr 0 3 ⋯ (((TensorTree.tensorNode altLeftMetric).prod (TensorTree.tensorNode altRightMetric)).prod (TensorTree.tensorNode (contrBispinorUp p))))).tensor

          The definitional tensor node relation for contrBispinorDown.

          source
          theorem complexLorentzTensor.tensorNode_coBispinorUp (p : ↑Lorentz.complexCo.V) :
          (TensorTree.tensorNode (coBispinorUp p)).tensor = (TensorTree.contr 0 2 ⋯ ((TensorTree.tensorNode PauliMatrix.pauliContr).prod (TensorTree.tensorNode (TensorTree.vecNodeE complexLorentzTensor Color.down p).tensor))).tensor

          The definitional tensor node relation for coBispinorUp.

          source
          theorem complexLorentzTensor.tensorNode_coBispinorDown (p : ↑Lorentz.complexCo.V) :
          (TensorTree.tensorNode (coBispinorDown p)).tensor = (TensorTree.contr 1 2 ⋯ (TensorTree.contr 0 3 ⋯ (((TensorTree.tensorNode altLeftMetric).prod (TensorTree.tensorNode altRightMetric)).prod (TensorTree.tensorNode (coBispinorUp p))))).tensor

          The definitional tensor node relation for coBispinorDown.

          Basic equalities. #

          source
          def complexLorentzTensor.contrBispinorUp_eq_metric_contr_contrBispinorDown :
          InformalLemma

          {contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ.

          Proof: expand contrBispinorDown and use fact that metrics contract to the identity.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def complexLorentzTensor.coBispinorUp_eq_metric_contr_coBispinorDown :
            InformalLemma

            {coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ.

            proof: expand coBispinorDown and use fact that metrics contract to the identity.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem complexLorentzTensor.contrBispinorDown_expand (p : ↑Lorentz.complexContr.V) :
              (TensorTree.tensorNode (contrBispinorDown p)).tensor = (TensorTree.contr 1 2 ⋯ (TensorTree.contr 0 3 ⋯ (((TensorTree.tensorNode altLeftMetric).prod (TensorTree.tensorNode altRightMetric)).prod (TensorTree.contr 0 2 ⋯ ((TensorTree.tensorNode PauliMatrix.pauliCo).prod (TensorTree.tensorNode (TensorTree.vecNodeE complexLorentzTensor Color.up p).tensor)))))).tensor
              source
              theorem complexLorentzTensor.coBispinorDown_expand (p : ↑Lorentz.complexCo.V) :
              (TensorTree.tensorNode (coBispinorDown p)).tensor = (TensorTree.contr 1 2 ⋯ (TensorTree.contr 0 3 ⋯ (((TensorTree.tensorNode altLeftMetric).prod (TensorTree.tensorNode altRightMetric)).prod (TensorTree.contr 0 2 ⋯ ((TensorTree.tensorNode PauliMatrix.pauliContr).prod (TensorTree.tensorNode (TensorTree.vecNodeE complexLorentzTensor Color.down p).tensor)))))).tensor