Basis vectors associated with complex Lorentz tensors

The material in this file should slowly be replaced with tensorBasis.

def complexLorentzTensor.basisVector {n : ℕ} (c : Fin n → complexLorentzTensor.C) (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) : ↑(complexLorentzTensor.F.obj (IndexNotation.OverColor.mk c)).V

Basis vectors for complex Lorentz tensors.

Equations

• complexLorentzTensor.basisVector c b = (PiTensorProduct.tprod ℂ) fun (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c).left) => (complexLorentzTensor.basis (c i)) (b i)

theorem complexLorentzTensor.basisVector_eq_tensorBasis {n : ℕ} (c : Fin n → complexLorentzTensor.C) (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) : basisVector c b = (complexLorentzTensor.tensorBasis c) b

theorem complexLorentzTensor.perm_basisVector_cast {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) (i : Fin m) : complexLorentzTensor.repDim (c ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)) = complexLorentzTensor.repDim (c1 i)

theorem complexLorentzTensor.basis_eq_FD {c1 : complexLorentzTensor.C} {n : ℕ} (c : Fin n → complexLorentzTensor.C) (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) (i : Fin n) (h : { as := c i } = { as := c1 }) : (CategoryTheory.ConcreteCategory.hom (complexLorentzTensor.FD.map (CategoryTheory.eqToHom h)).hom) ((complexLorentzTensor.basis (c i)) (b i)) = (complexLorentzTensor.basis c1) (Fin.cast ⋯ (b i))

theorem complexLorentzTensor.perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) : (TensorTree.perm σ (TensorTree.tensorNode (basisVector c b))).tensor = basisVector c1 fun (i : Fin m) => Fin.cast ⋯ (b ((IndexNotation.OverColor.Hom.toEquiv σ).symm i))

The perm node acting on basis vectors corresponds to a basis vector.

theorem complexLorentzTensor.perm_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) (b : (j : Fin n) → Fin (complexLorentzTensor.repDim (c j))) : (TensorTree.perm σ (TensorTree.tensorNode (basisVector c b))).tensor = (TensorTree.tensorNode (basisVector c1 fun (i : Fin m) => Fin.cast ⋯ (b ((IndexNotation.OverColor.Hom.toEquiv σ).symm i)))).tensor

The perm node acting on basis vectors corresponds to a basis vector, as a tensor tree structure.

def complexLorentzTensor.contrBasisVectorMul {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} (i : Fin n.succ.succ) (j : Fin n.succ) (b : (k : Fin n.succ.succ) → Fin (complexLorentzTensor.repDim (c k))) : ℂ

The scalar determining if contracting two basis vectors together gives zero or not.

Equations

• complexLorentzTensor.contrBasisVectorMul i j b = if ↑(b i) = ↑(b (i.succAbove j)) then 1 else 0

theorem complexLorentzTensor.contrBasisVectorMul_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {b : (k : Fin n.succ.succ) → Fin (complexLorentzTensor.repDim (c k))} (h : ¬↑(b i) = ↑(b (i.succAbove j))) : contrBasisVectorMul i j b = 0

theorem complexLorentzTensor.contrBasisVectorMul_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {b : (k : Fin n.succ.succ) → Fin (complexLorentzTensor.repDim (c k))} (h : ↑(b i) = ↑(b (i.succAbove j))) : contrBasisVectorMul i j b = 1

theorem complexLorentzTensor.contr_basisVector {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} (b : (k : Fin n.succ.succ) → Fin (complexLorentzTensor.repDim (c k))) : (TensorTree.contr i j h (TensorTree.tensorNode (basisVector c b))).tensor = contrBasisVectorMul i j b • basisVector (c ∘ i.succAbove ∘ j.succAbove) fun (k : Fin n) => b (i.succAbove (j.succAbove k))

theorem complexLorentzTensor.contr_basisVector_tree {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} (b : (k : Fin n.succ.succ) → Fin (complexLorentzTensor.repDim (c k))) : (TensorTree.contr i j h (TensorTree.tensorNode (basisVector c b))).tensor = (TensorTree.smul (contrBasisVectorMul i j b) (TensorTree.tensorNode (basisVector (c ∘ i.succAbove ∘ j.succAbove) fun (k : Fin n) => b (i.succAbove (j.succAbove k))))).tensor

theorem complexLorentzTensor.contr_basisVector_tree_pos {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} (b : (k : Fin n.succ.succ) → Fin (complexLorentzTensor.repDim (c k))) (hn : ↑(b i) = ↑(b (i.succAbove j)) := by decide) : (TensorTree.contr i j h (TensorTree.tensorNode (basisVector c b))).tensor = (TensorTree.tensorNode (basisVector (c ∘ i.succAbove ∘ j.succAbove) fun (k : Fin n) => b (i.succAbove (j.succAbove k)))).tensor

theorem complexLorentzTensor.contr_basisVector_tree_neg {n : ℕ} {c : Fin n.succ.succ → complexLorentzTensor.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = complexLorentzTensor.τ (c i)} (b : (k : Fin n.succ.succ) → Fin (complexLorentzTensor.repDim (c k))) (hn : ¬↑(b i) = ↑(b (i.succAbove j)) := by decide) : (TensorTree.contr i j h (TensorTree.tensorNode (basisVector c b))).tensor = (TensorTree.tensorNode 0).tensor

def complexLorentzTensor.prodBasisVecEquiv {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (i : Fin n ⊕ Fin m) : Sum.elim (fun (i : Fin n) => Fin (complexLorentzTensor.repDim (c i))) (fun (i : Fin m) => Fin (complexLorentzTensor.repDim (c1 i))) i ≃ Fin (complexLorentzTensor.repDim (Sum.elim c c1 i))

Equivalence of Fin types appearing in the product of two basis vectors.

Equations

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

theorem complexLorentzTensor.prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (b : (k : Fin n) → Fin (complexLorentzTensor.repDim (c k))) (b1 : (k : Fin m) → Fin (complexLorentzTensor.repDim (c1 k))) : ((TensorTree.tensorNode (basisVector c b)).prod (TensorTree.tensorNode (basisVector c1 b1))).tensor = basisVector (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) fun (i : Fin (n + m)) => (prodBasisVecEquiv (finSumFinEquiv.symm i)) (PhysLean.PiTensorProduct.elimPureTensor b b1 (finSumFinEquiv.symm i))

The prod node acting on basis vectors corresponds to a basis vector.

theorem complexLorentzTensor.prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (b : (k : Fin n) → Fin (complexLorentzTensor.repDim (c k))) (b1 : (k : Fin m) → Fin (complexLorentzTensor.repDim (c1 k))) : ((TensorTree.tensorNode (basisVector c b)).prod (TensorTree.tensorNode (basisVector c1 b1))).tensor = (TensorTree.tensorNode (basisVector (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) fun (i : Fin (n + m)) => (prodBasisVecEquiv (finSumFinEquiv.symm i)) (PhysLean.PiTensorProduct.elimPureTensor b b1 (finSumFinEquiv.symm i)))).tensor

The prod node acting on a basis vectors is a basis vector, as a tensor tree structure.

theorem complexLorentzTensor.eval_basisVector {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C} {i : Fin n.succ} (j : Fin (complexLorentzTensor.repDim (c i))) (b : (k : Fin n.succ) → Fin (complexLorentzTensor.repDim (c k))) : (TensorTree.eval i (↑j) (TensorTree.tensorNode (basisVector c b))).tensor = (if j = b i then 1 else 0) • basisVector (c ∘ i.succAbove) fun (k : Fin n) => b (i.succAbove k)

The eval node acting on basis vectors corresponds to a basis vector.