Basis for tensors in a tensor species

noncomputable def complexLorentzTensor.ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.C} : (TensorSpecies.Tensor.ComponentIdx c → PhysLean.RatComplexNum) →ₛₗ[PhysLean.RatComplexNum.toComplexNum] complexLorentzTensor.Tensor c

A complex Lorentz tensor from a map (Π j, Fin (complexLorentzTensor.repDim (c j))) → RatComplexNum. All complex Lorentz tensors with rational coefficents with respect to the basis are of this form.

Equations

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

@[simp]

theorem complexLorentzTensor.ofRat_basis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTensor.C} (f : TensorSpecies.Tensor.ComponentIdx c → PhysLean.RatComplexNum) (b : TensorSpecies.Tensor.ComponentIdx c) : ((TensorSpecies.Tensor.basis c).repr (ofRat f)) b = PhysLean.RatComplexNum.toComplexNum (f b)

theorem complexLorentzTensor.basis_eq_ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.C} (b : TensorSpecies.Tensor.ComponentIdx c) : (TensorSpecies.Tensor.basis c) b = ofRat fun (b' : TensorSpecies.Tensor.ComponentIdx c) => if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }

theorem complexLorentzTensor.contr_basis_ratComplexNum {c : complexLorentzTensor.C} (i : Fin (complexLorentzTensor.repDim c)) (j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) : complexLorentzTensor.castToField ((CategoryTheory.ConcreteCategory.hom (complexLorentzTensor.contr.app { as := c }).hom) ((complexLorentzTensor.basis c) i ⊗ₜ[ℂ] (complexLorentzTensor.basis (complexLorentzTensor.τ c)) j)) = PhysLean.RatComplexNum.toComplexNum (if ↑i = ↑j then 1 else 0)

theorem complexLorentzTensor.prodT_ofRat_ofRat {n n1 : ℕ} {c : Fin n → complexLorentzTensor.C} (f : TensorSpecies.Tensor.ComponentIdx c → PhysLean.RatComplexNum) {c1 : Fin n1 → complexLorentzTensor.C} (f1 : TensorSpecies.Tensor.ComponentIdx c1 → PhysLean.RatComplexNum) : (TensorSpecies.Tensor.prodT (ofRat f)) (ofRat f1) = ofRat fun (b : TensorSpecies.Tensor.ComponentIdx (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)) => f (TensorSpecies.Tensor.ComponentIdx.splitEquiv b).1 * f1 (TensorSpecies.Tensor.ComponentIdx.splitEquiv b).2

theorem complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.C} {i j : Fin (n + 1 + 1)} {h : i ≠ j ∧ complexLorentzTensor.τ (c i) = c j} (f : TensorSpecies.Tensor.ComponentIdx c → PhysLean.RatComplexNum) : (TensorSpecies.Tensor.contrT n i j h) (ofRat f) = ofRat fun (b : TensorSpecies.Tensor.ComponentIdx (c ∘ TensorSpecies.Tensor.Pure.dropPairEmb i j)) => ∑ x : { x : TensorSpecies.Tensor.ComponentIdx c // x ∈ b.DropPairSection }, f ↑x * if ↑(↑x i) = ↑(↑x j) then 1 else 0

theorem complexLorentzTensor.contrT_ofRat {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.C} {i j : Fin (n + 1 + 1)} {h : i ≠ j ∧ complexLorentzTensor.τ (c i) = c j} (f : TensorSpecies.Tensor.ComponentIdx c → PhysLean.RatComplexNum) : (TensorSpecies.Tensor.contrT n i j h) (ofRat f) = ofRat fun (b : TensorSpecies.Tensor.ComponentIdx (c ∘ TensorSpecies.Tensor.Pure.dropPairEmb i j)) => ∑ x : Fin (complexLorentzTensor.repDim (c i)), f ↑((TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv ⋯ b) (x, Fin.cast ⋯ x))

theorem complexLorentzTensor.permT_ofRat {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} {σ : Fin m → Fin n} (h : TensorSpecies.Tensor.PermCond c c1 σ) (f : TensorSpecies.Tensor.ComponentIdx c → PhysLean.RatComplexNum) : (TensorSpecies.Tensor.permT σ h) (ofRat f) = ofRat fun (b : TensorSpecies.Tensor.ComponentIdx c1) => f fun (i : Fin n) => Fin.cast ⋯ (b (TensorSpecies.Tensor.PermCond.inv σ h i))