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.

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 ⋯

def realLorentzTensor (d : ℕ := 3) : TensorSpecies ℝ ↑(LorentzGroup 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.

instance realLorentzTensor.instDecidableEqCRealElemMatrixSumFinOfNatNatLorentzGroup (d : ℕ) : DecidableEq (realLorentzTensor d).C

Color for real Lorentz tensors is decidable.

Equations

• realLorentzTensor.instDecidableEqCRealElemMatrixSumFinOfNatNatLorentzGroup d = realLorentzTensor.instDecidableEqColor

@[simp]

theorem realLorentzTensor.C_eq_color {d : ℕ} : (realLorentzTensor d).C = Color

Simplyfing repDim

theorem realLorentzTensor.repDim_up {d : ℕ} : (realLorentzTensor d).repDim Color.up = 1 + d

theorem realLorentzTensor.repDim_down {d : ℕ} : (realLorentzTensor d).repDim Color.down = 1 + d

@[simp]

theorem realLorentzTensor.repDim_eq_one_plus_dim {d : ℕ} {c : (realLorentzTensor d).C} : (realLorentzTensor d).repDim c = 1 + d

Simplyfing τ

@[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 : (realLorentzTensor d).C} (i : Fin ((realLorentzTensor d).repDim c)) (j : Fin ((realLorentzTensor d).repDim ((realLorentzTensor d).τ c))) : (realLorentzTensor d).castToField ((CategoryTheory.ConcreteCategory.hom ((realLorentzTensor d).contr.app { as := c }).hom) (((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) → (realLorentzTensor d).C} {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 : { x : TensorSpecies.Tensor.ComponentIdx c // 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) → (realLorentzTensor d).C} {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 + d), ((TensorSpecies.Tensor.basis c).repr t) ↑((TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv ⋯ b) (Fin.cast ⋯ x, Fin.cast ⋯ x))