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.

def TensorSpecies.Tensor.ComponentIdx.complexify {n : ℕ} {c : Fin n → realLorentzTensor.Color} : ComponentIdx c ≃ ComponentIdx (realLorentzTensor.colorToComplex ∘ c)

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

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.

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

@[simp]

theorem realLorentzTensor.permCond_colorToComplex {n m : ℕ} {c : Fin n → Color} {c1 : Fin m → Color} {σ : Fin m → Fin n} (h : TensorSpecies.Tensor.PermCond c c1 σ) : TensorSpecies.Tensor.PermCond (colorToComplex ∘ c) (colorToComplex ∘ c1) σ

The PermCond condition is preserved under colorToComplex.

theorem realLorentzTensor.permT_toComplex {n m : ℕ} {c : Fin n → Color} {c1 : Fin m → Color} {σ : Fin m → Fin n} (h : TensorSpecies.Tensor.PermCond c c1 σ) (t : realLorentzTensor.Tensor c) : toComplex ((TensorSpecies.Tensor.permT σ h) t) = (TensorSpecies.Tensor.permT σ ⋯) (toComplex t)

The map toComplex commutes with permT.

@[simp]

theorem realLorentzTensor.colorToComplex_append {n m : ℕ} (c : Fin n → Color) (c1 : Fin m → Color) : colorToComplex ∘ Fin.append c c1 = Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1)

colorToComplex commutes with Fin.append (as functions).

noncomputable def realLorentzTensor.prodTColorToComplex {n m : ℕ} {c : Fin n → Color} {c1 : Fin m → Color} : complexLorentzTensor.Tensor (colorToComplex ∘ c) → complexLorentzTensor.Tensor (colorToComplex ∘ c1) → complexLorentzTensor.Tensor (colorToComplex ∘ Fin.append c c1)

prodT on the complex side, with colors written as colorToComplex ∘ Fin.append .... This is prodT followed by a cast using colorToComplex_append.

theorem realLorentzTensor.prodT_toComplex {n m : ℕ} {c : Fin n → Color} {c1 : Fin m → Color} (t : realLorentzTensor.Tensor c) (t1 : realLorentzTensor.Tensor c1) : toComplex ((TensorSpecies.Tensor.prodT t) t1) = prodTColorToComplex (toComplex t) (toComplex t1)

The map toComplex commutes with prodT.

@[simp]

theorem realLorentzTensor.tau_colorToComplex (x : Color) : complexLorentzTensor.τ (colorToComplex x) = colorToComplex (realLorentzTensor.τ x)

τ commutes with colorToComplex on the Lorentz up/down colors.

theorem realLorentzTensor.contrT_toComplex {n : ℕ} {c : Fin (n + 1 + 1) → Color} {i j : Fin (n + 1 + 1)} (h : i ≠ j ∧ realLorentzTensor.τ (c i) = c j) (t : realLorentzTensor.Tensor c) : toComplex ((TensorSpecies.Tensor.contrT n i j h) t) = (TensorSpecies.Tensor.contrT n i j ⋯) (toComplex t)

The map toComplex commutes with contrT.

@[simp]

theorem realLorentzTensor.complex_repDim_up : complexLorentzTensor.repDim complexLorentzTensor.Color.up = 4

@[simp]

theorem realLorentzTensor.complex_repDim_down : complexLorentzTensor.repDim complexLorentzTensor.Color.down = 4

def realLorentzTensor.evalIdxToComplex {n : ℕ} {c : Fin (n + 1) → Color} (i : Fin (n + 1)) (b : Fin (realLorentzTensor.repDim (c i))) : Fin (complexLorentzTensor.repDim ((colorToComplex ∘ c) i))

Convert an evaluation index from the real repDim to the complex repDim.

noncomputable def realLorentzTensor.evalTColorToComplex {n : ℕ} {c : Fin (n + 1) → Color} (i : Fin (n + 1)) (b : Fin (realLorentzTensor.repDim (c i))) : complexLorentzTensor.Tensor (colorToComplex ∘ c) → complexLorentzTensor.Tensor (colorToComplex ∘ c ∘ i.succAbove)

evalT on the complex side, but with output colors as colorToComplex ∘ (c ∘ i.succAbove). Implemented via permT (σ := id) (by simp) as a transport.

theorem realLorentzTensor.evalT_toComplex {n : ℕ} {c : Fin (n + 1) → Color} (i : Fin (n + 1)) (b : Fin (realLorentzTensor.repDim (c i))) (t : realLorentzTensor.Tensor c) : toComplex ((TensorSpecies.Tensor.evalT i b) t) = evalTColorToComplex i b (toComplex t)

The map toComplex commutes with evalT.