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 : Color) : 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 TensorSpecies.Tensor.ComponentIdx.complexify {n : ℕ} {c : Fin n → realLorentzTensor.Color} : ComponentIdx c ≃ ComponentIdx (realLorentzTensor.colorToComplex ∘ c)

The complification of the component index of a real Lorentz tensor to a complex Lorentz tensor.

Equations

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

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

The semilinear map from real Lorentz tensors to complex Lorentz tensors, defined through basis.

Equations

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

theorem realLorentzTensor.toComplex_eq_sum_basis {n : ℕ} (c : Fin n → Color) (v : realLorentzTensor.Tensor c) : toComplex v = ∑ i : TensorSpecies.Tensor.ComponentIdx (colorToComplex ∘ c), ((TensorSpecies.Tensor.basis c).repr v) (TensorSpecies.Tensor.ComponentIdx.complexify.symm i) • (TensorSpecies.Tensor.basis (colorToComplex ∘ c)) i

@[simp]

theorem realLorentzTensor.toComplex_eq_zero_iff {n : ℕ} (c : Fin n → Color) (v : realLorentzTensor.Tensor c) : toComplex v = 0 ↔ v = 0

theorem realLorentzTensor.toComplex_injective {n : ℕ} (c : Fin n → Color) : Function.Injective ⇑toComplex

The map toComplex is injective.

theorem realLorentzTensor.toComplex_equivariant {n : ℕ} {c : Fin n → Color} (v : realLorentzTensor.Tensor c) (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) : Λ • toComplex v = toComplex (Lorentz.SL2C.toLorentzGroup Λ • v)

The map toComplex is equivariant.

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" }