feat: Simple perm identities

HepLean/Tensors/ComplexLorentz/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import HepLean.Tensors.Tree.Elab
 import HepLean.Tensors.ComplexLorentz.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basis
+import HepLean.Tensors.Tree.NodeIdentities.Basic
 /-!
 
 ## Lemmas related to complex Lorentz tensors.
@@ -66,7 +67,6 @@ lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ :
     match i with
     | (0 : Fin 2) => rfl
     | (1 : Fin 2) => rfl
-
 /-
 lemma coMetric_prod_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V)
     (S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V)
@@ -84,7 +84,7 @@ lemma coMetric_prod_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr
     apply congrArg
     sorry
     sorry
--/
+    -/
 end Fermion
 
 end

HepLean/Tensors/Tree/Basic.lean

@@ -460,7 +460,7 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over
 -/
 
 @[simp]
-lemma tensoreNode_tensor {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
+lemma tensorNode_tensor {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
     (tensorNode T).tensor = T := rfl
 
 @[simp]

HepLean/Tensors/Tree/NodeIdentities/Basic.lean

@@ -79,4 +79,20 @@ lemma neg_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
     (perm σ (neg t)).tensor = (neg (perm σ t)).tensor := by
   simp only [perm_tensor, neg_tensor, map_neg]
 
+/-!
+
+## Basic perm identities
+
+-/
+
+/-- Applying two permutations is the same as applying the transitive permutation. -/
+lemma perm_perm {n : ℕ} {c : Fin n → S.C} {c1 : Fin n → S.C} {c2 : Fin n → S.C}
+    (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (σ2 : (OverColor.mk c1) ⟶ (OverColor.mk c2))
+    (t : TensorTree S c) : (perm σ2 (perm σ t)).tensor = (perm (σ ≫ σ2) t).tensor := by
+  simp [perm_tensor]
+
+/-- Applying the identity permutation is the same as not applying a permutation. -/
+lemma perm_id (t : TensorTree S c) : (perm (𝟙 (OverColor.mk c)) t).tensor = t.tensor := by
+  simp [perm_tensor]
+
 end TensorTree