Complex Lorentz tensors from real Lorentz tensors

i. Overview

In this module we describe how to pass from real Lorentz tensors to complex Lorentz tensors in a functorial way. Specifically, we construct a canonical equivariant semilinear map

• toComplex : ℝT(3, c) →ₛₗ[Complex.ofRealHom] ℂT(colorToComplex ∘ c)

which is compatible with the natural operations on tensors (permutations of indices, tensor products, contractions and evaluations).

ii. Key results

The main definitions and statements are:

• colorToComplex upgrades the colour of a real Lorentz tensor to the corresponding complex Lorentz colour.
• TensorSpecies.Tensor.ComponentIdx.complexify transports component indices along colorToComplex.
• toComplex is the basic semilinear map from real to complex Lorentz tensors.
• toComplex_basis and toComplex_pure_basisVector show that toComplex sends basis tensors to basis tensors.
• toComplex_eq_zero_iff and toComplex_injective show that toComplex is injective.
• toComplex_equivariant states that toComplex is equivariant for the action of the complexified Lorentz group.
• permT_toComplex, prodT_toComplex, contrT_toComplex and evalT_toComplex express that toComplex commutes with the basic tensor operations.

iii. Table of contents

• A. Colours and component indices
• B. The semilinear map toComplex
  • B.1. Expression in the tensor basis
  • B.2. Behaviour on basis vectors and injectivity
  • B.3. Equivariance under the Lorentz action
• C. Compatibility with permutations: permT
• D. Compatibility with tensor products: prodT
• E. Compatibility with contraction: contrT
• F. Compatibility with evaluation: evalT

iv. References

The general formalism of Lorentz tensors and their operations is developed in other parts of the library; here we only specialise to the passage from real to complex Lorentz tensors.

A. Colours and component indices

We first explain how the Lorentz colour data and component indices for real tensors are transported to the complex setting.

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

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

theorem realLorentzTensor.colorToComplex_match_up {n : ℕ} {c : Fin n → Color} {j : Fin n} (hc : c j = Color.up) : (match c j with | Color.up => complexLorentzTensor.Color.up | Color.down => complexLorentzTensor.Color.down) = complexLorentzTensor.Color.up

simp helper: reduce match c j after a case split on c j (avoids dependent rw / Pi.smul_apply).

theorem realLorentzTensor.colorToComplex_match_down {n : ℕ} {c : Fin n → Color} {j : Fin n} (hc : c j = Color.down) : (match c j with | Color.up => complexLorentzTensor.Color.up | Color.down => complexLorentzTensor.Color.down) = complexLorentzTensor.Color.down

theorem realLorentzTensor.colorToComplex_comp_eq_match {n : ℕ} (c : Fin n → Color) (j : Fin n) : (colorToComplex ∘ c) j = match c j with | Color.up => complexLorentzTensor.Color.up | Color.down => complexLorentzTensor.Color.down

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.

@[simp]

theorem realLorentzTensor.ComponentIdx.complexify_apply {n : ℕ} {c : Fin n → Color} (f : TensorSpecies.Tensor.ComponentIdx c) (j : Fin n) : TensorSpecies.Tensor.ComponentIdx.complexify f j = Fin.cast ⋯ (f j)

@[simp]

theorem realLorentzTensor.ComponentIdx.complexify_toFun_apply {n : ℕ} {c : Fin n → Color} (f : TensorSpecies.Tensor.ComponentIdx c) (j : Fin n) : TensorSpecies.Tensor.ComponentIdx.complexify.toFun f j = TensorSpecies.Tensor.ComponentIdx.complexify f j

B. The semilinear map toComplex

We now define the basic semilinear map from real Lorentz tensors to complex Lorentz tensors. It is characterised by sending the standard tensor basis on the real side to the corresponding basis on the complex side, and is therefore determined by the behaviour on components.

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

theorem realLorentzTensor.toComplex_repr {n : ℕ} {c : Fin n → Color} (v : realLorentzTensor.Tensor c) (i : TensorSpecies.Tensor.ComponentIdx c) : ((TensorSpecies.Tensor.basis (colorToComplex ∘ c)).repr (toComplex v)) (TensorSpecies.Tensor.ComponentIdx.complexify i) = ↑(((TensorSpecies.Tensor.basis c).repr v) i)

The representation of toComplex v in the complexified basis equals the real representation coerced to complex.

@[simp]

theorem realLorentzTensor.toComplex_basis {n : ℕ} {c : Fin n → Color} (i : TensorSpecies.Tensor.ComponentIdx c) : toComplex ((TensorSpecies.Tensor.basis c) i) = (TensorSpecies.Tensor.basis (colorToComplex ∘ c)) (TensorSpecies.Tensor.ComponentIdx.complexify i)

toComplex sends basis elements to basis elements.

@[simp]

theorem realLorentzTensor.toComplex_pure_basisVector {n : ℕ} {c : Fin n → Color} (b : TensorSpecies.Tensor.ComponentIdx c) : toComplex (TensorSpecies.Tensor.Pure.basisVector c b).toTensor = (TensorSpecies.Tensor.Pure.basisVector (colorToComplex ∘ c) (TensorSpecies.Tensor.ComponentIdx.complexify b)).toTensor

toComplex on a pure basis vector.

theorem realLorentzTensor.toComplex_map_smul {n : ℕ} (c : Fin n → Color) (r : ℝ) (t : realLorentzTensor.Tensor c) : toComplex (r • t) = ↑r • toComplex t

@[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_slot_repr_up {n : ℕ} {c : Fin n → Color} (k : Fin n) (h : c k = Color.up) (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) (b : TensorSpecies.Tensor.ComponentIdx c) (i : TensorSpecies.Tensor.ComponentIdx (colorToComplex ∘ c)) : ↑(((realLorentzTensor.basis (c k)).repr (((realLorentzTensor.FD.obj { as := c k }).ρ (Lorentz.SL2C.toLorentzGroup Λ)) ((realLorentzTensor.basis (c k)) (b k)))) (TensorSpecies.Tensor.ComponentIdx.complexify.symm i k)) = LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ) (finSumFinEquiv.symm (Fin.cast ⋯ (i k))) (finSumFinEquiv.symm (Fin.cast ⋯ (b k)))

Local lemma for toComplex_equivariant: isolates the heavy matrix step for a contravariant slot.

theorem realLorentzTensor.toComplex_equivariant_slot_repr_down {n : ℕ} {c : Fin n → Color} (k : Fin n) (h : c k = Color.down) (Λ : Matrix.SpecialLinearGroup (Fin 2) ℂ) (b : TensorSpecies.Tensor.ComponentIdx c) (i : TensorSpecies.Tensor.ComponentIdx (colorToComplex ∘ c)) : ↑(((realLorentzTensor.basis (c k)).repr (((realLorentzTensor.FD.obj { as := c k }).ρ (Lorentz.SL2C.toLorentzGroup Λ)) ((realLorentzTensor.basis (c k)) (b k)))) (TensorSpecies.Tensor.ComponentIdx.complexify.symm i k)) = (LorentzGroup.toComplex (Lorentz.SL2C.toLorentzGroup Λ))⁻¹ (finSumFinEquiv.symm (Fin.cast ⋯ (b k))) (finSumFinEquiv.symm (Fin.cast ⋯ (i k)))

Local lemma for toComplex_equivariant: isolates the heavy matrix step for a covariant slot.

B.3. Equivariance under the Lorentz action

Finally we record that toComplex is equivariant for the natural action of SL(2, ℂ) (and hence the induced Lorentz action) on tensors.

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.

C. Compatibility with permutations: permT

We first show that complexification is compatible with permutation of tensor slots. On colours this is encoded in the PermCond predicate, and on tensors by the operator permT.

@[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.

@[simp]

theorem realLorentzTensor.permT_basis_real {n m : ℕ} {c : Fin n → Color} {c1 : Fin m → Color} {σ : Fin m → Fin n} (h : TensorSpecies.Tensor.PermCond c c1 σ) (b : TensorSpecies.Tensor.ComponentIdx c) : (TensorSpecies.Tensor.permT σ h) ((TensorSpecies.Tensor.basis c) b) = (TensorSpecies.Tensor.basis c1) fun (j : Fin m) => Fin.cast ⋯ (b (σ j))

permT sends basis vectors to basis vectors.

@[simp]

theorem realLorentzTensor.permT_basis_complex {n m : ℕ} {c : Fin n → complexLorentzTensor.Color} {c1 : Fin m → complexLorentzTensor.Color} {σ : Fin m → Fin n} (h : TensorSpecies.Tensor.PermCond c c1 σ) (b : TensorSpecies.Tensor.ComponentIdx c) : (TensorSpecies.Tensor.permT σ h) ((TensorSpecies.Tensor.basis c) b) = (TensorSpecies.Tensor.basis c1) fun (j : Fin m) => Fin.cast ⋯ (b (σ j))

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.

D. Compatibility with tensor products: prodT

@[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).

theorem realLorentzTensor.permCond_prodTColorToComplex {n m : ℕ} {c : Fin n → Color} {c1 : Fin m → Color} : TensorSpecies.Tensor.PermCond (Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1)) (colorToComplex ∘ Fin.append c c1) id

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.

@[simp]

theorem realLorentzTensor.complexify_prod {n m : ℕ} {c : Fin n → Color} {c1 : Fin m → Color} (b : TensorSpecies.Tensor.ComponentIdx c) (b1 : TensorSpecies.Tensor.ComponentIdx c1) : TensorSpecies.Tensor.ComponentIdx.complexify (b.prod b1) = cast ⋯ ((TensorSpecies.Tensor.ComponentIdx.complexify b).prod (TensorSpecies.Tensor.ComponentIdx.complexify b1))

complexify commutes with prod of component indices.

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.

E. Compatibility with contraction: contrT

@[simp]

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

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

@[simp]

theorem realLorentzTensor.ComponentIdx.complexify_comp_dropPairEmb {n : ℕ} {c : Fin (n + 1 + 1) → Color} {i j : Fin (n + 1 + 1)} (b : TensorSpecies.Tensor.ComponentIdx c) (m : Fin n) : TensorSpecies.Tensor.ComponentIdx.complexify (fun (k : Fin n) => b (TensorSpecies.Tensor.Pure.dropPairEmb i j k)) m = TensorSpecies.Tensor.ComponentIdx.complexify b (TensorSpecies.Tensor.Pure.dropPairEmb i j m)

complexify commutes with precomposition by dropPairEmb. We use fun k => b (Pure.dropPairEmb i j k) and direct application (ComponentIdx.complexify b) (Pure.dropPairEmb i j m) rather than composition so that dependent ComponentIdx types unify correctly (avoiding Function.comp type mismatch).

theorem realLorentzTensor.toComplex_contrP_basisVector {n : ℕ} {c : Fin (n + 1 + 1) → Color} {i j : Fin (n + 1 + 1)} (h : i ≠ j ∧ realLorentzTensor.τ (c i) = c j) (b : TensorSpecies.Tensor.ComponentIdx c) : toComplex (TensorSpecies.Tensor.Pure.contrP i j h (TensorSpecies.Tensor.Pure.basisVector c b)) = TensorSpecies.Tensor.Pure.contrP i j ⋯ (TensorSpecies.Tensor.Pure.basisVector (colorToComplex ∘ c) (TensorSpecies.Tensor.ComponentIdx.complexify b))

For a real basis vector, toComplex(contrP(basisVector c b)) equals contrP(basisVector (colorToComplex ∘ c) (complexify b)) (complex species).

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.

F. Compatibility with evaluation: evalT

@[simp]

theorem realLorentzTensor.ComponentIdx.complexify_comp_succAbove {n : ℕ} {c : Fin (n + 1) → Color} (i : Fin (n + 1)) (b : TensorSpecies.Tensor.ComponentIdx c) (m : Fin n) : TensorSpecies.Tensor.ComponentIdx.complexify (fun (k : Fin n) => b (i.succAbove k)) m = TensorSpecies.Tensor.ComponentIdx.complexify b (i.succAbove m)

complexify commutes with precomposition by succAbove.

@[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.toComplex_evalP_basisVector {n : ℕ} {c : Fin (n + 1) → Color} (i : Fin (n + 1)) (b : Fin (realLorentzTensor.repDim (c i))) (b' : TensorSpecies.Tensor.ComponentIdx c) : toComplex (TensorSpecies.Tensor.Pure.evalP i b (TensorSpecies.Tensor.Pure.basisVector c b')) = (TensorSpecies.Tensor.permT id ⋯) (TensorSpecies.Tensor.Pure.evalP i (evalIdxToComplex i b) (TensorSpecies.Tensor.Pure.basisVector (colorToComplex ∘ c) (TensorSpecies.Tensor.ComponentIdx.complexify b')))

For a real basis vector, toComplex(evalP(basisVector c b)) equals evalP(basisVector (colorToComplex ∘ c) (complexify b)) (complex species).

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.