Bispinors

Definitions

def complexLorentzTensor.contrBispinorUp (p : complexLorentzTensor.Tensor ![Color.up]) : complexLorentzTensor.Tensor ![Color.upL, Color.upR]

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

def complexLorentzTensor.contrBispinorDown (p : complexLorentzTensor.Tensor ![Color.up]) : complexLorentzTensor.Tensor ![Color.downL, Color.downR]

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

def complexLorentzTensor.coBispinorUp (p : complexLorentzTensor.Tensor ![Color.down]) : complexLorentzTensor.Tensor ![Color.upL, Color.upR]

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

def complexLorentzTensor.coBispinorDown (p : complexLorentzTensor.Tensor ![Color.down]) : complexLorentzTensor.Tensor ![Color.downL, Color.downR]

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

Basic equalities.

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.

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.