Real Lorentz tensors

Within this directory Pre is used to denote that the definitions are preliminary and which are used to define realLorentzTensor.

inductive realLorentzTensor.Color : Type

The colors associated with complex representations of SL(2, ℂ) of interest to physics.

• up : Color

  The color associated with contravariant Lorentz vectors.

• down : Color

  The color associated with covariant Lorentz vectors.

@[implicit_reducible]

instance realLorentzTensor.instDecidableEqColor : DecidableEq Color

Color for complex Lorentz tensors is decidable.

Equations

• realLorentzTensor.instDecidableEqColor realLorentzTensor.Color.up realLorentzTensor.Color.up = isTrue ⋯
• realLorentzTensor.instDecidableEqColor realLorentzTensor.Color.down realLorentzTensor.Color.down = isTrue ⋯
• realLorentzTensor.instDecidableEqColor realLorentzTensor.Color.up realLorentzTensor.Color.down = isFalse ⋯
• realLorentzTensor.instDecidableEqColor realLorentzTensor.Color.down realLorentzTensor.Color.up = isFalse ⋯

noncomputable def realLorentzTensor (d : ℕ := 3) : TensorSpecies ℝ realLorentzTensor.Color ↑(LorentzGroup d) fun (x : realLorentzTensor.Color) => Fin 1 ⊕ Fin d

The tensor structure for complex Lorentz tensors.

Equations

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

def realLorentzTensor.realLorentzTensorSyntax : Lean.ParserDescr

Notation for a real Lorentz tensor.

Equations

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

def realLorentzTensor.«termℝT(_,_)» : Lean.ParserDescr

Notation for a real Lorentz tensor.

Equations

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

Basis and discrete functor objects

These re-express fields of realLorentzTensor d in terms of Lorentz data.

@[simp]

theorem realLorentzTensor.basisIdxCongr_eq_refl {d : ℕ} {c1 c2 : Color} (h : c1 = c2) : TensorSpecies.basisIdxCongr h = Equiv.refl (Fin 1 ⊕ Fin d)

theorem realLorentzTensor.basisIdxCongr_apply {d : ℕ} {c1 c2 : Color} (h : c1 = c2) (i : Fin 1 ⊕ Fin d) : (TensorSpecies.basisIdxCongr h) i = i

theorem realLorentzTensor.basis_eq_contrBasis {d : ℕ} : (realLorentzTensor d).basis Color.up = Lorentz.contrBasis d

theorem realLorentzTensor.basis_eq_coBasis {d : ℕ} : (realLorentzTensor d).basis Color.down = Lorentz.coBasis d

theorem realLorentzTensor.FD_obj_up {d : ℕ} : (realLorentzTensor d).FD.obj { as := Color.up } = Lorentz.Contr d

theorem realLorentzTensor.FD_obj_down {d : ℕ} : (realLorentzTensor d).FD.obj { as := Color.down } = Lorentz.Co d

Simplifying τ

@[simp]

theorem realLorentzTensor.τ_up_eq_down {d : ℕ} : (realLorentzTensor d).τ Color.up = Color.down

@[simp]

theorem realLorentzTensor.τ_down_eq_up {d : ℕ} : (realLorentzTensor d).τ Color.down = Color.up

Simplification of contractions with respect to basis

theorem realLorentzTensor.contr_basis {d : ℕ} {c : Color} (i j : Fin 1 ⊕ Fin d) : TensorSpecies.castToField ((Rep.Hom.hom ((realLorentzTensor d).contr.app { as := c })) (((realLorentzTensor d).basis c) i ⊗ₜ[ℝ] ((realLorentzTensor d).basis ((realLorentzTensor d).τ c)) j)) = if i = j then 1 else 0

theorem realLorentzTensor.contrT_basis_repr_apply_eq_dropPairSection {n d : ℕ} {c : Fin (n + 1 + 1) → Color} {i j : Fin (n + 1 + 1)} (h : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j) (t : (realLorentzTensor d).Tensor c) (b : TensorSpecies.Tensor.ComponentIdx (c ∘ TensorSpecies.Tensor.Pure.dropPairEmb i j)) : ((TensorSpecies.Tensor.basis (c ∘ TensorSpecies.Tensor.Pure.dropPairEmb i j)).repr ((TensorSpecies.Tensor.contrT n i j h) t)) b = ∑ x : ↥b.DropPairSection, ((TensorSpecies.Tensor.basis c).repr t) ↑x * if ↑x i = ↑x j then 1 else 0

theorem realLorentzTensor.contrT_basis_repr_apply_eq_fin {n d : ℕ} {c : Fin (n + 1 + 1) → Color} {i j : Fin (n + 1 + 1)} {h : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j} (t : (realLorentzTensor d).Tensor c) (b : TensorSpecies.Tensor.ComponentIdx (c ∘ TensorSpecies.Tensor.Pure.dropPairEmb i j)) : ((TensorSpecies.Tensor.basis (c ∘ TensorSpecies.Tensor.Pure.dropPairEmb i j)).repr ((TensorSpecies.Tensor.contrT n i j h) t)) b = ∑ x : Fin 1 ⊕ Fin d, ((TensorSpecies.Tensor.basis c).repr t) ↑((TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv ⋯ b) (x, x))

Contractions and to Field

theorem realLorentzTensor.contrPCoeff_basis {d n : ℕ} {c : Fin n → Color} (i j : Fin n) (hij : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j) (b : TensorSpecies.Tensor.ComponentIdx c) : TensorSpecies.Tensor.Pure.contrPCoeff i j hij (TensorSpecies.Tensor.Pure.basisVector c b) = if b i = b j then 1 else 0

theorem realLorentzTensor.contrT_eq_sum_evalT {n d : ℕ} (c : Fin (n + 1 + 1) → Color) (i j : Fin (n + 1 + 1)) (h : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j) (t : (realLorentzTensor d).Tensor c) : (TensorSpecies.Tensor.contrT n i j h) t = ∑ μ : Fin 1 ⊕ Fin d, (TensorSpecies.Tensor.permT id ⋯) ((TensorSpecies.Tensor.evalT ((Fin.predAbove 0 i).predAbove j) μ) ((TensorSpecies.Tensor.evalT i μ) t))

theorem realLorentzTensor.contrT_toField {d : ℕ} (c : Fin 2 → Color) (h : 0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1) (t : (realLorentzTensor d).Tensor c) : TensorSpecies.Tensor.toField ((TensorSpecies.Tensor.contrT 0 0 1 h) t) = ∑ μ : Fin 1 ⊕ Fin d, TensorSpecies.Tensor.toField ((TensorSpecies.Tensor.evalT 0 μ) ((TensorSpecies.Tensor.evalT 0 μ) (TensorSpecies.Tensorial.toTensor t)))