Complex Lorentz tensors from Real Lorentz tensors

In this module we define the equivariant semi-linear map from real Lorentz tensors to complex Lorentz tensors.

def realLorentzTensor.colorToComplex (c : realLorentzTensor.C) : complexLorentzTensor.Color

The map from colors of real Lorentz tensors to complex Lorentz tensors.

Equations

• realLorentzTensor.colorToComplex realLorentzTensor.Color.up = complexLorentzTensor.Color.up
• realLorentzTensor.colorToComplex realLorentzTensor.Color.down = complexLorentzTensor.Color.down

def realLorentzTensor.toComplex {n : ℕ} (c : Fin n → realLorentzTensor.C) : realLorentzTensor.Tensor c →ₛₗ[Complex.ofRealHom] complexLorentzTensor.Tensor (colorToComplex ∘ c)

The semilinear map from real Lorentz tensors to complex Lorentz tensors.

Semiformal implmentation note: Probably the easist way to define this is through basis.

Equations

• realLorentzTensor.toComplex c = sorry

def realLorentzTensor.toComplex_injective : InformalLemma

The map toComplex is injective.

Equations

• realLorentzTensor.toComplex_injective = { deps := [], tag := "7RKCJ" }

def realLorentzTensor.toComplex_equivariant : InformalLemma

The map toComplex is equivariant.

Equations

• realLorentzTensor.toComplex_equivariant = { deps := [], tag := "7RKDY" }

Relation to tensor operations

def realLorentzTensor.permT_toComplex : InformalLemma

The map toComplex commutes with permT.

Equations

• realLorentzTensor.permT_toComplex = { deps := [`TensorSpecies.Tensor.permT], tag := "7RKA6" }

def realLorentzTensor.prodT_toComplex : InformalLemma

The map toComplex commutes with prodT.

Equations

• realLorentzTensor.prodT_toComplex = { deps := [`TensorSpecies.Tensor.prodT], tag := "7RKFF" }

def realLorentzTensor.contrT_toComplex : InformalLemma

The map toComplex commutes with contrT.

Equations

• realLorentzTensor.contrT_toComplex = { deps := [`TensorSpecies.Tensor.contrT], tag := "7RKFR" }

def realLorentzTensor.evalT_toComplex : InformalLemma

The map toComplex commutes with evalT.

Equations

• realLorentzTensor.evalT_toComplex = { deps := [`TensorSpecies.Tensor.evalT], tag := "7RKGK" }