feat: Get evaluation working.

HepLean/Tensors/ComplexLorentz/Basic.lean

@@ -143,6 +143,14 @@ def complexLorentzTensor : TensorSpecies where
     | Color.downR => 2
     | Color.up => 4
     | Color.down => 4
+  repDim_neZero := fun c =>
+    match c with
+    | Color.upL => inferInstance
+    | Color.downL => inferInstance
+    | Color.upR => inferInstance
+    | Color.downR => inferInstance
+    | Color.up => inferInstance
+    | Color.down => inferInstance
   basis := fun c =>
     match c with
     | Color.upL => Fermion.leftBasis

HepLean/Tensors/ComplexLorentz/Lemmas.lean

@@ -146,6 +146,9 @@ lemma symm_contr_antiSymm {S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V}
   rw [antiSymm_contr_symm hA hs]
   rfl
 
+lemma contr_rank_1_expand (p : Lorentz.complexCo) (q : Lorentz.complexContr) :
+    {(p | μ ⊗ q | μ) = p | 0}ᵀ := by
+  sorry
 end Fermion
 
 end

HepLean/Tensors/Tree/Basic.lean

@@ -46,6 +46,8 @@ structure TensorSpecies where
   /-- A specification of the dimension of each color in C. This will be used for explicit
     evaluation of tensors. -/
   repDim : C → ℕ
+  /-- repDim is not zero for any color. This allows casting of `ℕ` to `Fin (S.repDim c)`. -/
+  repDim_neZero (c : C) : NeZero (repDim c)
   /-- A basis for each Module, determined by the evaluation map. -/
   basis : (c : C) → Basis (Fin (repDim c)) k (FDiscrete.obj (Discrete.mk c)).V
   /-- Contraction is symmetric with respect to duals. -/
@@ -65,6 +67,8 @@ instance : CommRing S.k := S.k_commRing
 
 instance : Group S.G := S.G_group
 
+instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c
+
 /-- The lift of the functor `S.F` to a monoidal functor. -/
 def F : BraidedFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FDiscrete
 
@@ -528,7 +532,7 @@ inductive TensorTree (S : TensorSpecies) : ∀ {n : ℕ}, (Fin n → S.C) → Ty
     (j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c →
     TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
   | eval {n : ℕ} {c : Fin n.succ → S.C} :
-    (i : Fin n.succ) → (x : Fin (S.repDim (c i))) → TensorTree S c →
+    (i : Fin n.succ) → (x : ℕ) → TensorTree S c →
     TensorTree S (c ∘ Fin.succAbove i)
 
 namespace TensorTree
@@ -538,6 +542,11 @@ variable {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c)
 open MonoidalCategory
 open TensorProduct
 
+/-- The node `vecNode` of a tensor tree, with all arguments explicit. -/
+abbrev vecNodeE (S : TensorSpecies) (c1 : S.C)
+    (v : (S.FDiscrete.obj (Discrete.mk c1)).V) :
+    TensorTree S ![c1] := vecNode v
+
 /-- The node `twoNode` of a tensor tree, with all arguments explicit. -/
 abbrev twoNodeE (S : TensorSpecies) (c1 c2 : S.C)
     (v : (S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)).V) :
@@ -587,7 +596,7 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over
   | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
     ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor))
   | contr i j h t => (S.contrMap _ i j h).hom t.tensor
-  | eval i e t => (S.evalMap i e) t.tensor
+  | eval i e t => (S.evalMap i (Fin.ofNat' e Fin.size_pos')) t.tensor
   | _ => 0
 
 /-!
@@ -623,8 +632,8 @@ lemma contr_tensor {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ}
 
 lemma neg_tensor (t : TensorTree S c) : (neg t).tensor = - t.tensor := rfl
 
-lemma eval_tensor {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : Fin (S.repDim (c i)))
-    (t : TensorTree S c) : (eval i e t).tensor = (S.evalMap i e) t.tensor := rfl
+lemma eval_tensor {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ)
+    (t : TensorTree S c) : (eval i e t).tensor = (S.evalMap i (Fin.ofNat' e Fin.size_pos')) t.tensor := rfl
 
 /-!
 

HepLean/Tensors/Tree/Elab.lean

@@ -96,8 +96,11 @@ declare_syntax_cat tensorExpr
 /-- The syntax for a tensor node. -/
 syntax term "|" (ppSpace indexExpr)* : tensorExpr
 
+/-- Equality. -/
+syntax:40 tensorExpr "=" tensorExpr:41 : tensorExpr
+
 /-- The syntax for tensor prod two tensor nodes. -/
-syntax tensorExpr "⊗" tensorExpr : tensorExpr
+syntax:70 tensorExpr "⊗" tensorExpr:71 : tensorExpr
 
 /-- The syntax for tensor addition. -/
 syntax tensorExpr "+" tensorExpr : tensorExpr
@@ -111,9 +114,6 @@ syntax term "•" tensorExpr : tensorExpr
 /-- Negation of a tensor tree. -/
 syntax "-" tensorExpr : tensorExpr
 
-/-- Equality. -/
-syntax tensorExpr "=" tensorExpr : tensorExpr
-
 namespace TensorNode
 
 /-!
@@ -129,7 +129,7 @@ We also want to ensure the number of indices is correct.
 
 -/
 
-/-- The indices of a tensor node. Before contraction, dualisation, and evaluation. -/
+/-- The indices of a tensor node. Before contraction, and evaluation. -/
 partial def getIndices (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
   match stx with
   | `(tensorExpr| $_:term | $[$args]*) => do
@@ -183,6 +183,16 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
   let strType := toString type
   let n := (String.splitOn strType "CategoryTheory.MonoidalCategoryStruct.tensorObj").length
   let const := (String.splitOn strType "Quiver.Hom").length
+  match ← isDefEq type (← stringToType "CoeSort.coe Lorentz.complexCo") with
+  | true =>
+    return Syntax.mkApp (mkIdent ``TensorTree.vecNodeE) #[mkIdent ``Fermion.complexLorentzTensor,
+      mkIdent ``Fermion.Color.down, T]
+  | _ =>
+  match ← isDefEq type (← stringToType "CoeSort.coe Lorentz.complexContr") with
+  | true =>
+    return Syntax.mkApp (mkIdent ``TensorTree.vecNodeE) #[mkIdent ``Fermion.complexLorentzTensor,
+      mkIdent ``Fermion.Color.up, T]
+  | _ =>
   match n, const with
   | 1, 1 =>
     match type with
@@ -235,13 +245,24 @@ def termNodeSyntax (T : Term) : TermElabM Term := do
       return Syntax.mkApp (mkIdent ``TensorTree.constThreeNode) #[T]
   | _, _ => throwError "Could not create terminal node syntax (termNodeSyntax). "
 
+/-- Adjusts a list `List ℕ` by subtracting from each natrual number the number
+  of elements before it in the list which are less then itself. This is used
+  to form a list of pairs which can be used for evaluating indices. -/
+def evalAdjustPos (l : List ℕ) : List ℕ  :=
+  let l' := List.mapAccumr
+    (fun x (prev : List ℕ) =>
+      let e := prev.countP (fun y => y < x)
+      (x :: prev, x - e)) l.reverse []
+  l'.2.reverse
+
 /-- The positions in getIndicesNode which get evaluated, and the value they take. -/
 partial def getEvalPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do
   let ind ← getIndices stx
   let indEnum := ind.enum
   let evals := indEnum.filter (fun x => indexExprIsNum x.2)
   let evals2 ← (evals.mapM (fun x => indexToNum x.2))
-  return List.zip (evals.map (fun x => x.1)) evals2
+  let pos :=  evalAdjustPos (evals.map (fun x => x.1))
+  return List.zip pos evals2
 
 /-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.eval` to the given term. -/
 def evalSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
@@ -259,11 +280,11 @@ partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do
     throwError "To many contractions"
   return filt
 
-/-- The list of indices after contraction. -/
+/-- The list of indices after contraction or evaluation. -/
 def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
   let ind ← getIndices stx
   let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x)
-  return ind.filter (fun x => indFilt.count x ≤ 1)
+  return indFilt.filter (fun x => indFilt.count x ≤ 1)
 
 /-- Takes a list and puts conseutive elements into pairs.
   e.g. [0, 1, 2, 3] becomes [(0, 1), (2, 3)]. -/
@@ -460,7 +481,8 @@ partial def syntaxFull (stx : Syntax) : TermElabM Term := do
   match stx with
   | `(tensorExpr| $_:term | $[$args]*) =>
     ProdNode.syntaxFull stx
-  | `(tensorExpr| $_:tensorExpr ⊗ $_:tensorExpr) => ProdNode.syntaxFull stx
+  | `(tensorExpr| $_:tensorExpr ⊗ $_:tensorExpr) => do
+      return ← ProdNode.syntaxFull stx
   | `(tensorExpr| ($a:tensorExpr)) => do
       return (← syntaxFull a)
   | `(tensorExpr| -$a:tensorExpr) => do
@@ -476,6 +498,7 @@ partial def syntaxFull (stx : Syntax) : TermElabM Term := do
 
 /-- An elaborator for tensor nodes. This is to be generalized. -/
 def elaborateTensorNode (stx : Syntax) : TermElabM Expr := do
+  println! "{(← syntaxFull stx)}"
   let tensorExpr ← elabTerm (← syntaxFull stx) none
   return tensorExpr