From 271745c11ae1f7a2d3481d47db05fd2b18331500 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 21 Oct 2024 12:24:17 +0000
Subject: [PATCH] refactor: Rename TensorSpeciesStruct to TensorSpecies

---
 HepLean/Tensors/ComplexLorentz/Basic.lean     |  2 +-
 HepLean/Tensors/ComplexLorentz/Lemmas.lean    |  2 +-
 HepLean/Tensors/Tree/Basic.lean               | 21 +++++++++----------
 HepLean/Tensors/Tree/Elab.lean                |  2 +-
 .../Tensors/Tree/NodeIdentities/Basic.lean    |  2 +-
 .../Tree/NodeIdentities/ContrContr.lean       |  8 +++----
 .../Tree/NodeIdentities/PermContr.lean        | 10 ++++-----
 .../Tensors/Tree/NodeIdentities/PermProd.lean |  2 +-
 .../Tensors/Tree/NodeIdentities/ProdComm.lean |  2 +-
 9 files changed, 25 insertions(+), 26 deletions(-)

diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean
index 62c3aaa..e90925f 100644
--- a/HepLean/Tensors/ComplexLorentz/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basic.lean
@@ -81,7 +81,7 @@ instance : DecidableEq Color := fun x y =>
 noncomputable section
 
 /-- The tensor structure for complex Lorentz tensors. -/
-def complexLorentzTensor : TensorSpeciesStruct where
+def complexLorentzTensor : TensorSpecies where
   C := Fermion.Color
   G := SL(2, ℂ)
   G_group := inferInstance
diff --git a/HepLean/Tensors/ComplexLorentz/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
index 86acd3e..e455e60 100644
--- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean
+++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
@@ -59,7 +59,7 @@ lemma coMetric_expand : {Lorentz.coMetric | μ ν}ᵀ.tensor =
 lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ := by
   simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, perm_tensor]
   rw [coMetric_expand]
-  simp only [TensorSpeciesStruct.F, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, Fin.isValue,
+  simp only [TensorSpecies.F, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, Fin.isValue,
     map_sub]
   congr 1
   congr 1
diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean
index 753b186..f79847b 100644
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@@ -18,9 +18,8 @@ open CategoryTheory
 open MonoidalCategory
 
 /-- The sturcture of a type of tensors e.g. Lorentz tensors, Einstien tensors,
-  complex Lorentz tensors.
-  Note: This structure is not fully defined yet. -/
-structure TensorSpeciesStruct where
+  complex Lorentz tensors. -/
+structure TensorSpecies where
   /-- The colors of indices e.g. up or down. -/
   C : Type
   /-- The symmetry group acting on these tensor e.g. the Lorentz group or SL(2,ℂ). -/
@@ -55,10 +54,10 @@ structure TensorSpeciesStruct where
 
 noncomputable section
 
-namespace TensorSpeciesStruct
+namespace TensorSpecies
 open OverColor
 
-variable (S : TensorSpeciesStruct)
+variable (S : TensorSpecies)
 
 instance : CommRing S.k := S.k_commRing
 
@@ -355,10 +354,10 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
       simp
     exact h1' h1
 
-end TensorSpeciesStruct
+end TensorSpecies
 
 /-- A syntax tree for tensor expressions. -/
-inductive TensorTree (S : TensorSpeciesStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Type where
+inductive TensorTree (S : TensorSpecies) : ∀ {n : ℕ}, (Fin n → S.C) → Type where
   /-- A general tensor node. -/
   | tensorNode {n : ℕ} {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : TensorTree S c
   /-- A node consisting of a single vector. -/
@@ -404,23 +403,23 @@ inductive TensorTree (S : TensorSpeciesStruct) : ∀ {n : ℕ}, (Fin n → S.C)
 
 namespace TensorTree
 
-variable {S : TensorSpeciesStruct} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c)
+variable {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c)
 
 open MonoidalCategory
 open TensorProduct
 
 /-- The node `twoNode` of a tensor tree, with all arguments explicit. -/
-abbrev twoNodeE (S : TensorSpeciesStruct) (c1 c2 : S.C)
+abbrev twoNodeE (S : TensorSpecies) (c1 c2 : S.C)
     (v : (S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)).V) :
     TensorTree S ![c1, c2] := twoNode v
 
 /-- The node `constTwoNodeE` of a tensor tree, with all arguments explicit. -/
-abbrev constTwoNodeE (S : TensorSpeciesStruct) (c1 c2 : S.C)
+abbrev constTwoNodeE (S : TensorSpecies) (c1 c2 : S.C)
     (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
     TensorTree S ![c1, c2] := constTwoNode v
 
 /-- The node `constThreeNodeE` of a tensor tree, with all arguments explicit. -/
-abbrev constThreeNodeE (S : TensorSpeciesStruct) (c1 c2 c3 : S.C)
+abbrev constThreeNodeE (S : TensorSpecies) (c1 c2 c3 : S.C)
     (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗
       S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3] :=
     constThreeNode v
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index 2a4e601..e221dbd 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -487,7 +487,7 @@ elab_rules (kind:=tensorExprSyntax) : term
     let tensorTree ← elaborateTensorNode e
     return tensorTree
 
-variable {S : TensorSpeciesStruct} {c4 : Fin 4 → S.C} (T4 : S.F.obj (OverColor.mk c4))
+variable {S : TensorSpecies} {c4 : Fin 4 → S.C} (T4 : S.F.obj (OverColor.mk c4))
   {c5 : Fin 5 → S.C} (T5 : S.F.obj (OverColor.mk c5)) (a : S.k)
 
 variable (𝓣 : TensorTree S c4)
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
index b35ea60..326cb3c 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean
@@ -22,7 +22,7 @@ open TensorProduct
 
 namespace TensorTree
 
-variable {S : TensorSpeciesStruct}
+variable {S : TensorSpecies}
 
 /-!
 
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
index bfca586..59bd184 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
@@ -21,7 +21,7 @@ open HepLean.Fin
 
 namespace TensorTree
 
-variable {S : TensorSpeciesStruct}
+variable {S : TensorSpecies}
 
 /-- A structure containing two pairs of indices (i, j) and (k, l) to be sequentially
   contracted in a tensor. -/
@@ -168,7 +168,7 @@ lemma contrSwapHom_contrMapSnd_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).
     (x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove q.swap.l))))))) •
     ((lift.obj S.FDiscrete).map q.contrSwapHom).hom ((PiTensorProduct.tprod S.k) fun k =>
     x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k)))))) := by
-  rw [contrMapSnd,TensorSpeciesStruct.contrMap_tprod]
+  rw [contrMapSnd,TensorSpecies.contrMap_tprod]
   change ((lift.obj S.FDiscrete).map q.contrSwapHom).hom
     (_ • ((PiTensorProduct.tprod S.k) fun k =>
         x (q.swap.i.succAbove (q.swap.j.succAbove
@@ -214,7 +214,7 @@ lemma contrMapFst_contrMapSnd_swap :
     (S.F.map q.contrSwapHom).hom
     (q.swap.contrMapSnd.hom ((S.contrMap c q.swap.i q.swap.j _).hom
     ((PiTensorProduct.tprod S.k) x)))
-  rw [TensorSpeciesStruct.contrMap_tprod, TensorSpeciesStruct.contrMap_tprod]
+  rw [TensorSpecies.contrMap_tprod, TensorSpecies.contrMap_tprod]
   simp only [Nat.succ_eq_add_one, Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V,
     Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
     Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as,
@@ -226,7 +226,7 @@ lemma contrMapFst_contrMapSnd_swap :
     ((lift.obj S.FDiscrete).map q.contrSwapHom).hom
       (q.swap.contrMapSnd.hom ((PiTensorProduct.tprod S.k)
       fun k => x (q.swap.i.succAbove (q.swap.j.succAbove k))))
-  rw [contrMapSnd, TensorSpeciesStruct.contrMap_tprod, q.contrSwapHom_contrMapSnd_tprod]
+  rw [contrMapSnd, TensorSpecies.contrMap_tprod, q.contrSwapHom_contrMapSnd_tprod]
   rw [smul_smul, smul_smul]
   congr 1
   /- The contractions. -/
diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
index 2fb2373..4efa9f2 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
@@ -8,7 +8,7 @@ import HepLean.Tensors.Tree.Basic
 
 # The commutativity of Permutations and contractions.
 
-There is very likely a better way to do this using `TensorSpeciesStruct.contrMap_tprod`.
+There is very likely a better way to do this using `TensorSpecies.contrMap_tprod`.
 
 -/
 
@@ -18,10 +18,10 @@ open MonoidalCategory
 open OverColor
 open HepLean.Fin
 
-namespace TensorSpeciesStruct
+namespace TensorSpecies
 noncomputable section
 
-variable (S : TensorSpeciesStruct)
+variable (S : TensorSpecies)
 
 lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
     {i : Fin n.succ.succ} {j : Fin n.succ} (h : c1 (i.succAbove j) = S.τ (c1 i))
@@ -236,11 +236,11 @@ lemma contrMap_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
   rfl
 
 end
-end TensorSpeciesStruct
+end TensorSpecies
 
 namespace TensorTree
 
-variable {S : TensorSpeciesStruct}
+variable {S : TensorSpecies}
 
 /-- Permuting indices, and then contracting is equivalent to contracting and then permuting,
   once care is taking about ensuring one is contracting the same idices. -/
diff --git a/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean b/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean
index 05d12ee..9d909f7 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/PermProd.lean
@@ -19,7 +19,7 @@ open HepLean.Fin
 
 namespace TensorTree
 
-variable {S : TensorSpeciesStruct} {n n' n2 : ℕ}
+variable {S : TensorSpecies} {n n' n2 : ℕ}
     {c : Fin n → S.C} {c' : Fin n' → S.C} (c2 : Fin n2 → S.C)
     (σ : OverColor.mk c ⟶ OverColor.mk c')
 
diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean
index 5150c1d..515583c 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean
@@ -19,7 +19,7 @@ open HepLean.Fin
 
 namespace TensorTree
 
-variable {S : TensorSpeciesStruct} {n n2 : ℕ}
+variable {S : TensorSpecies} {n n2 : ℕ}
     (c : Fin n → S.C) (c2 : Fin n2 → S.C)
 
 /-- The permutation that arises when moving a commuting terms in a `prod` node.