PhysLean Documentation

PhysLean.Relativity.Lorentz.ComplexTensor.OfRat

Basis for tensors in a tensor species #

source
noncomputable def complexLorentzTensor.ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.C} (f : ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) → PhysLean.RatComplexNum) :
↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk c)).V

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.
Instances For
    source
    @[simp]
    theorem complexLorentzTensor.ofRat_tensorBasis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTensor.C} (f : ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) → PhysLean.RatComplexNum) (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) :
    ((complexLorentzTensor.tensorBasis c).repr (ofRat f)) b = PhysLean.RatComplexNum.toComplexNum (f b)
    source
    theorem complexLorentzTensor.ofRat_add {n : ℕ} {c : Fin n → complexLorentzTensor.C} (f f1 : ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) → PhysLean.RatComplexNum) :
    ofRat (f + f1) = ofRat f + ofRat f1
    source
    theorem complexLorentzTensor.tensorBasis_eq_ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.C} (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) :
    (complexLorentzTensor.tensorBasis c) b = ofRat fun (b' : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) => if b = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }
    source
    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.k] (complexLorentzTensor.basis (complexLorentzTensor.τ c)) j)) = PhysLean.RatComplexNum.toComplexNum (if ↑i = ↑j then 1 else 0)
    source
    theorem complexLorentzTensor.prod_ofRat_ofRat {n n1 : ℕ} {c : Fin n → complexLorentzTensor.C} (f : ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) → PhysLean.RatComplexNum) {c1 : Fin n1 → complexLorentzTensor.C} (f1 : ((j : Fin n1) → Fin (complexLorentzTensor.repDim (c1 j))) → PhysLean.RatComplexNum) :
    ((TensorTree.tensorNode (ofRat f)).prod (TensorTree.tensorNode (ofRat f1))).tensor = (TensorTree.tensorNode (ofRat fun (b : (j : Fin (n + n1)) → Fin (complexLorentzTensor.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) => f (TensorSpecies.TensorBasis.prodEquiv b).1 * f1 (TensorSpecies.TensorBasis.prodEquiv b).2)).tensor
    source
    theorem complexLorentzTensor.contr_ofRat {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.C} {i : Fin (n + 1 + 1)} {j : Fin (n + 1)} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} (f : ((k : Fin (n + 1 + 1)) → Fin (complexLorentzTensor.repDim (c k))) → PhysLean.RatComplexNum) :
    (TensorTree.contr i j h (TensorTree.tensorNode (ofRat f))).tensor = (TensorTree.tensorNode (ofRat fun (b : (j_1 : Fin n) → Fin (complexLorentzTensor.repDim ((c ∘ i.succAbove ∘ j.succAbove) j_1))) => ∑ x : { x : (k : Fin n.succ.succ) → Fin (complexLorentzTensor.repDim (c k)) // x ∈ TensorSpecies.TensorBasis.ContrSection b }, f ↑x * if ↑(↑x i) = ↑(↑x (i.succAbove j)) then 1 else 0)).tensor
    source
    theorem complexLorentzTensor.smul_nat_ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.C} (n✝ : ℕ) (f1 : ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) → PhysLean.RatComplexNum) :
    (TensorTree.smul (↑n✝) (TensorTree.tensorNode (ofRat f1))).tensor = (TensorTree.tensorNode (ofRat fun (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) => ↑n✝ * f1 b)).tensor
    source
    theorem complexLorentzTensor.perm_ofRat {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} {σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1} (f : ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) → PhysLean.RatComplexNum) :
    (TensorTree.perm σ (TensorTree.tensorNode (ofRat f))).tensor = (TensorTree.tensorNode (ofRat fun (b : (j : Fin m) → Fin (complexLorentzTensor.repDim ((IndexNotation.OverColor.mk c1).hom j))) => f ((TensorSpecies.TensorBasis.congr (IndexNotation.OverColor.Hom.toEquiv σ) ⋯) b))).tensor
    source
    theorem complexLorentzTensor.add_ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.C} (f f1 : ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) → PhysLean.RatComplexNum) :
    ((TensorTree.tensorNode (ofRat f)).add (TensorTree.tensorNode (ofRat f1))).tensor = (TensorTree.tensorNode (ofRat fun (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) => f b + f1 b)).tensor