From 57d08ffd40529e9f56d1fd6f6fe99a61d4f33406 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 30 Jul 2024 09:29:05 -0400
Subject: [PATCH] feat: Add vecAsTensor

---
 HepLean/SpaceTime/LorentzTensor/Basic.lean    |  2 +-
 HepLean/SpaceTime/LorentzTensor/Fin.lean      | 58 +++++++++++++++++++
 .../LorentzTensor/MulActionTensor.lean        |  2 +-
 3 files changed, 60 insertions(+), 2 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean
index eb592e3..5cf9def 100644
--- a/HepLean/SpaceTime/LorentzTensor/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean
@@ -34,7 +34,7 @@ open TensorProduct
 
 variable {R : Type} [CommSemiring R]
 
-/-- An auxillary function to contract the vector space `V1` and `V2` in  `V1 ⊗[R] V2 ⊗[R] V3`. -/
+/-- An auxillary function to contract the vector space `V1` and `V2` in `V1 ⊗[R] V2 ⊗[R] V3`. -/
 def contrDualLeftAux {V1 V2 V3 : Type} [AddCommMonoid V1] [AddCommMonoid V2] [AddCommMonoid V3]
     [Module R V1] [Module R V2] [Module R V3] (f : V1 ⊗[R] V2 →ₗ[R] R) :
     V1 ⊗[R] V2 ⊗[R] V3 →ₗ[R] V3 :=
diff --git a/HepLean/SpaceTime/LorentzTensor/Fin.lean b/HepLean/SpaceTime/LorentzTensor/Fin.lean
index 745e33b..f69396e 100644
--- a/HepLean/SpaceTime/LorentzTensor/Fin.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Fin.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.Basic
+import HepLean.SpaceTime.LorentzTensor.MulActionTensor
 /-!
 
 # Lorentz tensors indexed by Fin n
@@ -35,6 +36,11 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [
   {cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
   {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
 
+variable {G H : Type} [Group G] [Group H] [MulActionTensor G 𝓣]
+local infixl:101 " • " => 𝓣.rep
+
+open MulActionTensor
+
 /-- Casting a tensor defined on `Fin n` to `Fin m` where `n = m`. -/
 @[simp]
 def finCast (h : n = m) (hc : cn = cm ∘ Fin.castOrderIso h) : 𝓣.Tensor cn ≃ₗ[R] 𝓣.Tensor cm :=
@@ -47,6 +53,58 @@ def finSumEquiv : 𝓣.Tensor cn ⊗[R] 𝓣.Tensor cm ≃ₗ[R]
     𝓣.Tensor (Sum.elim cn cm ∘ finSumFinEquiv.symm) :=
   (𝓣.tensoratorEquiv cn cm).trans (𝓣.mapIso finSumFinEquiv (by funext a; simp))
 
+/-!
+
+## Vectors as tensors & singletons
+
+-/
+
+/-- Tensors on `Fin 1` are equivalent to a constant Pi tensor product. -/
+def tensorSingeletonEquiv : 𝓣.Tensor ![μ] ≃ₗ[R] ⨂[R] _ : (Fin 1), 𝓣.ColorModule μ := by
+  refine LinearEquiv.ofLinear (PiTensorProduct.map (fun i =>
+      match i with
+      | 0 => LinearMap.id)) (PiTensorProduct.map (fun i =>
+    match i with
+    | 0 => LinearMap.id)) ?_ ?_
+  all_goals
+    apply LinearMap.ext
+    refine fun x ↦
+      PiTensorProduct.induction_on' x ?_ (by
+        intro a b hx a
+        simp_all only [Nat.succ_eq_add_one, Matrix.cons_val_zero, LinearMap.coe_comp,
+          Function.comp_apply, LinearMap.id_coe, id_eq, map_add])
+    intro r x
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Matrix.cons_val_zero,
+      PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, LinearMap.coe_comp,
+      Function.comp_apply, LinearMap.id_coe, id_eq]
+    change r •
+      (PiTensorProduct.map _) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) x)) = _
+    rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
+    repeat apply congrArg
+    funext i
+    fin_cases i
+    rfl
+
+/-- An equivalence between the `ColorModule` for a color and a `Fin 1` tensor with that color. -/
+def vecAsTensor : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.Tensor ![μ] :=
+  ((PiTensorProduct.subsingletonEquiv 0).symm : _ ≃ₗ[R] ⨂[R] _ : (Fin 1), 𝓣.ColorModule μ)
+    ≪≫ₗ 𝓣.tensorSingeletonEquiv.symm
+
+/-- The equivalence `vecAsTensor` is equivariant with respect to `MulActionTensor`-actions. -/
+@[simp]
+lemma vecAsTensor_equivariant (g : G) (v : 𝓣.ColorModule μ) :
+    𝓣.vecAsTensor (repColorModule μ g v) = g • 𝓣.vecAsTensor v := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, vecAsTensor, Fin.isValue, tensorSingeletonEquiv,
+    Matrix.cons_val_zero, LinearEquiv.trans_apply, PiTensorProduct.subsingletonEquiv_symm_apply,
+    LinearEquiv.ofLinear_symm_apply]
+  change (PiTensorProduct.map _) ((PiTensorProduct.tprod R) _) =
+    (𝓣.rep g) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) fun _ => v))
+  rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod, rep_tprod]
+  apply congrArg
+  funext i
+  fin_cases i
+  rfl
+
 end TensorStructure
 
 end
diff --git a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
index 1589170..7116e7c 100644
--- a/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
+++ b/HepLean/SpaceTime/LorentzTensor/MulActionTensor.lean
@@ -87,7 +87,7 @@ def rep : Representation R G (𝓣.Tensor cX) where
     simp_all only [_root_.map_mul]
     exact PiTensorProduct.map_mul _ _
 
-local infixl:78 " • " => 𝓣.rep
+local infixl:101 " • " => 𝓣.rep
 
 lemma repColorModule_colorModuleCast_apply (h : μ = ν) (g : G) (x : 𝓣.ColorModule μ) :
     (repColorModule ν g) (𝓣.colorModuleCast h x) =