PhysLean Notes

3.1. Complex Lorentz Tensors🔗

This section of the notes is a work-in-progress.

3.1.1. Complex Contravariant Vectors

🔗structure
Lorentz.ContrℂModule : Type
Lorentz.ContrℂModule : Type

The module for contravariant (up-index) complex Lorentz vectors.

Constructor

Lorentz.ContrℂModule.mk

Fields

val : Fin 1 ⊕ Fin 3 → ℂ

The underlying value as a vector Fin 1 ⊕ Fin 3 → ℂ.

🔗def
Lorentz.ContrℂModule.SL2CRep :
  Representation ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)
    Lorentz.ContrℂModule
Lorentz.ContrℂModule.SL2CRep :
  Representation ℂ
    (Matrix.SpecialLinearGroup (Fin 2) ℂ)
    Lorentz.ContrℂModule

The representation of the SL(2, ℂ) on ContrℂModule induced by the representation of the Lorentz group.

🔗def
Lorentz.complexContr : Rep ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ)
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 ψⁱ.