feat: Add evaluation (#432)

* feat: Add evaluation

* Update Basic.lean

PhysLean.lean

@@ -234,6 +234,7 @@ import PhysLean.Relativity.Tensors.TensorSpecies.MetricTensor
 import PhysLean.Relativity.Tensors.TensorSpecies.OfInt
 import PhysLean.Relativity.Tensors.TensorSpecies.Tensor.Basic
 import PhysLean.Relativity.Tensors.TensorSpecies.Tensor.Contraction
+import PhysLean.Relativity.Tensors.TensorSpecies.Tensor.Evaluation
 import PhysLean.Relativity.Tensors.TensorSpecies.UnitTensor
 import PhysLean.Relativity.Tensors.Tree.Basic
 import PhysLean.Relativity.Tensors.Tree.Dot

PhysLean/Relativity/Tensors/TensorSpecies/Tensor/Basic.lean

@@ -95,6 +95,14 @@ lemma update_same {n : ℕ} {c : Fin n → S.C} [inst : DecidableEq (Fin n)] (p
     (x : S.FD.obj (Discrete.mk (c i))) : (update p i x) i = x := by
   simp [update]
 
+@[simp]
+lemma update_succAbove_apply {n : ℕ} {c : Fin (n + 1) → S.C} [inst : DecidableEq (Fin (n + 1))]
+    (p : Pure S c) (i : Fin (n + 1)) (j : Fin n) (x : S.FD.obj (Discrete.mk (c (i.succAbove j)))) :
+    update p (i.succAbove j) x i = p i := by
+  simp only [update]
+  rw [Function.update_of_ne]
+  exact Fin.ne_succAbove i j
+
 @[simp]
 lemma toTensor_update_add {n : ℕ} {c : Fin n → S.C} [inst : DecidableEq (Fin n)] (p : Pure S c)
     (i : Fin n) (x y : S.FD.obj (Discrete.mk (c i))) :

PhysLean/Relativity/Tensors/TensorSpecies/Tensor/Evaluation.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import PhysLean.Relativity.Tensors.TensorSpecies.Tensor.Basic
+/-!
+
+# Evaluation of tensor indices
+
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+
+namespace TensorSpecies
+open OverColor
+
+variable {k : Type} [CommRing k] {S : TensorSpecies k}
+
+namespace Tensor
+
+
+namespace Pure
+
+variable {n : ℕ} {c : Fin (n + 1) → S.C}
+
+/-!
+
+## The evaluation coefficent.
+
+-/
+
+/-- Given a `i : Fin (n + 1)`, a `b : Fin (S.repDim (c i))` and a pure tensor
+  `p : Pure S c`,  `evalPCoeff i b p` is the `b`th component of `p i`. -/
+def evalPCoeff (i : Fin (n + 1)) (b : Fin (S.repDim (c i))) (p : Pure S c) : k :=
+  (S.basis (c i)).repr (p i) b
+
+@[simp]
+lemma evalPCoeff_update_self (i : Fin (n + 1)) [inst : DecidableEq (Fin (n + 1))]
+    (b : Fin (S.repDim (c i))) (p : Pure S c)
+    (x : S.FD.obj (Discrete.mk (c i)))  :
+    evalPCoeff i b (p.update i x) = (S.basis (c i)).repr x b := by
+  simp [evalPCoeff]
+
+@[simp]
+lemma evalPCoeff_update_succAbove (i : Fin (n + 1))  [inst : DecidableEq (Fin (n + 1))]
+    (j : Fin n)
+    (b : Fin (S.repDim (c i))) (p : Pure S c)
+    (x : S.FD.obj (Discrete.mk (c (i.succAbove j)))) :
+    evalPCoeff i b (p.update (i.succAbove j) x) = evalPCoeff i b p := by
+  simp [evalPCoeff]
+
+/-!
+
+## Evaluation for a pure tensor.
+
+-/
+
+/-- Given a `i : Fin (n + 1)`, a `b : Fin (S.repDim (c i))` and a pure tensor
+  `p : Pure S c`, `evalP i b p` is the tensor formed by evaluating the `i`th index
+  of `p` at `b`. -/
+noncomputable def evalP (i : Fin (n + 1)) (b : Fin (S.repDim (c i))) (p : Pure S c) :
+  Tensor S (c ∘ i.succAbove) := evalPCoeff i b p • (drop p i).toTensor
+
+@[simp]
+lemma evalP_update_add  [inst : DecidableEq (Fin (n + 1))] (i j : Fin (n + 1))
+    (b : Fin (S.repDim (c i))) (p : Pure S c)
+    (x y: S.FD.obj (Discrete.mk (c j))) :
+    evalP i b (p.update j (x + y)) =
+    evalP i b (p.update j x) + evalP i b (p.update j y):= by
+  simp only [evalP]
+  rcases Fin.eq_self_or_eq_succAbove i j with rfl | ⟨j, rfl⟩
+  · simp [add_smul]
+  · simp
+
+@[simp]
+lemma evalP_update_smul [inst : DecidableEq (Fin (n + 1))] (i j : Fin (n + 1))
+    (b : Fin (S.repDim (c i))) (p : Pure S c)
+    (r : k)
+    (x : S.FD.obj (Discrete.mk (c j))) :
+    evalP i b (p.update j (r • x )) =
+    r • evalP i b (p.update j x):= by
+  simp only [evalP]
+  rcases Fin.eq_self_or_eq_succAbove i j with rfl | ⟨j, rfl⟩
+  · simp [smul_smul]
+  · simp [smul_smul, mul_comm]
+
+/-!
+
+## Evaluation for a pure tensor as multilinear map.
+
+-/
+
+/-- The multi-linear map formed by evaluation of an index of pure tensors. -/
+noncomputable def evalPMultilinear {n : ℕ} {c : Fin (n + 1)→ S.C}
+    (i : Fin (n + 1)) (b : Fin (S.repDim (c i))) :
+    MultilinearMap k (fun i => S.FD.obj (Discrete.mk (c i)))
+      (S.Tensor (c ∘ i.succAbove)) where
+  toFun p := evalP i b p
+  map_update_add' p m x y := by
+    change (update p m (x + y)).evalP i b = _
+    simp only [evalP_update_add]
+    rfl
+  map_update_smul' p k r y := by
+    change (update p k (r • y)).evalP i b = _
+    rw [Pure.evalP_update_smul]
+    rfl
+
+end Pure
+
+/-- Given a `i : Fin (n + 1)`, a `b : Fin (S.repDim (c i))` and a tensor
+  `t : Tensor S c`, `evalT i b t` is the tensor formed by evaluating the `i`th index
+  of `t` at `b`. -/
+noncomputable def evalT {n : ℕ} {c : Fin (n + 1) → S.C} (i : Fin (n + 1))
+      (b : Fin (S.repDim (c i))) :
+    Tensor S c →ₗ[k] Tensor S (c ∘ i.succAbove) :=
+  PiTensorProduct.lift (Pure.evalPMultilinear i b)
+
+TODO "Add lemmas related to the interaction of evalT and permT, prodT and contrT."
+
+end Tensor
+
+end TensorSpecies