feat: Pure tensors

HepLean/Tensors/TensorSpecies/Contractions/Basic.lean

@@ -97,7 +97,7 @@ lemma smul_isNormZero_of_isNormZero {c : S.C} {ψ : S.FD.obj (Discrete.mk c)}
 
 /-- If a vector is norm-zero, then any vector in the orbit of that vector is also norm-zero. -/
 @[simp]
-lemma action_isNormZero_of_isNormZero {c : S.C} {ψ : S.FD.obj (Discrete.mk c)} (g : S.G) :
+lemma action_isNormZero_iff_isNormZero {c : S.C} {ψ : S.FD.obj (Discrete.mk c)} (g : S.G) :
     S.IsNormZero ((S.FD.obj (Discrete.mk c)).ρ g ψ) ↔ S.IsNormZero ψ := by
   simp only [IsNormZero, contractSelfField_equivariant]
 

HepLean/Tensors/TensorSpecies/Pure.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Tensors.TensorSpecies.DualRepIso
+/-!
+
+# Pure tensors
+-/
+
+open IndexNotation
+open CategoryTheory
+open MonoidalCategory
+
+noncomputable section
+
+namespace TensorSpecies
+open TensorTree
+variable (S : TensorSpecies)
+
+/-- The type of tensors specified by a map to colors `c : OverColor S.C`. -/
+def Pure (c : OverColor S.C) : Type := (i : c.left) → S.FD.obj (Discrete.mk (c.hom i))
+
+namespace Pure
+
+variable {S : TensorSpecies} {c : OverColor S.C}
+
+/-- The group action on a pure tensor. -/
+def ρ (g : S.G) (p : Pure S c) : Pure S c := fun i ↦ (S.FD.obj (Discrete.mk (c.hom i))).ρ g (p i)
+
+/-- The underlying tensor of a pure tensor. -/
+def tprod (p : Pure S c) : S.F.obj c := PiTensorProduct.tprod S.k p
+
+/-- The map `tprod` is equivariant with respect to the group action. -/
+lemma tprod_equivariant (g : S.G) (p : Pure S c) : (ρ g p).tprod = (S.F.obj c).ρ g p.tprod := by
+  simp only [F_def, OverColor.lift, OverColor.lift.obj', OverColor.lift.objObj',
+    OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj,
+    OverColor.instMonoidalCategoryStruct_tensorUnit_hom,
+    OverColor.instMonoidalCategoryStruct_tensorObj_left,
+    OverColor.instMonoidalCategoryStruct_tensorObj_hom, Rep.coe_of, tprod, Rep.of_ρ,
+    MonoidHom.coe_mk, OneHom.coe_mk, PiTensorProduct.map_tprod]
+  rfl
+
+end Pure
+
+/-- We say a tensor is pure if it is `⨂[S.k] i, p i` for some `p : Pure c`. -/
+def IsPure {c : OverColor S.C} (t : S.F.obj c) : Prop := ∃ p : Pure S c, t = p.tprod
+
+/-- As long as we are dealing with tensors with at least one index, then the zero
+  tensor is pure. -/
+lemma zero_isPure {c : OverColor S.C} [h : Nonempty c.left] : @IsPure S c 0 := by
+  refine ⟨fun i => 0, ?_⟩
+  simp only [Pure.tprod, Functor.id_obj]
+  change 0 = PiTensorProduct.tprodCoeff S.k 1 fun i => 0
+  symm
+  apply PiTensorProduct.zero_tprodCoeff' (1 : S.k)
+  rfl
+  exact (Classical.inhabited_of_nonempty h).default
+
+@[simp]
+lemma Pure.tprod_isPure {c : OverColor S.C} (p : Pure S c) : S.IsPure p.tprod := ⟨p, rfl⟩
+
+@[simp]
+lemma action_isPure_iff_isPure {c : OverColor S.C} {ψ : S.F.obj c} (g : S.G) :
+    S.IsPure ((S.F.obj c).ρ g ψ) ↔ S.IsPure ψ := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · obtain ⟨p, hp⟩ := h
+    have hp' := congrArg ((S.F.obj c).ρ g⁻¹) hp
+    simp only [Rep.ρ_inv_self_apply] at hp'
+    rw [← Pure.tprod_equivariant] at hp'
+    subst hp'
+    exact Pure.tprod_isPure S (Pure.ρ g⁻¹ p)
+  · obtain ⟨p, hp⟩ := h
+    subst hp
+    rw [← Pure.tprod_equivariant]
+    exact Pure.tprod_isPure S (Pure.ρ g p)
+
+end TensorSpecies
+
+end