feat: Actions on tensors (#428)

* feat: Some properties of tensors

* feat: Actions on tensors

* feat: More work on tensors

* feat: New results related to contractions

* refactor: Properties of contractions

* feat: Properties of products

* feat: prod node identities

* feat: More results regarding contractions

* refactor: Style lint

* refactor: Free simps

* feat: Some doc strings

* refactor: More doc-strings

* refactor: Remaining doc strings

* refactor: Lint

PhysLean.lean

@@ -232,12 +232,12 @@ import PhysLean.Relativity.Tensors.TensorSpecies.Contractions.ContrMap
 import PhysLean.Relativity.Tensors.TensorSpecies.DualRepIso
 import PhysLean.Relativity.Tensors.TensorSpecies.MetricTensor
 import PhysLean.Relativity.Tensors.TensorSpecies.OfInt
-import PhysLean.Relativity.Tensors.TensorSpecies.Pure
+import PhysLean.Relativity.Tensors.TensorSpecies.Tensor.Basic
+import PhysLean.Relativity.Tensors.TensorSpecies.Tensor.Contraction
 import PhysLean.Relativity.Tensors.TensorSpecies.UnitTensor
 import PhysLean.Relativity.Tensors.Tree.Basic
 import PhysLean.Relativity.Tensors.Tree.Dot
 import PhysLean.Relativity.Tensors.Tree.Elab
-import PhysLean.Relativity.Tensors.Tree.EquivalenceClass.Basic
 import PhysLean.Relativity.Tensors.Tree.NodeIdentities.Assoc
 import PhysLean.Relativity.Tensors.Tree.NodeIdentities.Basic
 import PhysLean.Relativity.Tensors.Tree.NodeIdentities.Congr

PhysLean/Relativity/Lorentz/ComplexTensor/Lemmas.lean

@@ -23,11 +23,12 @@ open OverColor.Discrete
 noncomputable section
 
 namespace complexLorentzTensor
-
-set_option maxRecDepth 5000 in
+open PhysLean.Fin
+/-
 lemma antiSymm_contr_symm {A : ℂT[.up, .up]} {S : ℂT[.down, .down]}
     (hA : {A | μ ν = - (A | ν μ)}ᵀ) (hs : {S | μ ν = S | ν μ}ᵀ) :
     {A | μ ν ⊗ S | μ ν = - A | μ ν ⊗ S | μ ν}ᵀ := by
+
   conv =>
     lhs
     rw [contr_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <| hA]
@@ -43,7 +44,7 @@ lemma antiSymm_contr_symm {A : ℂT[.up, .up]} {S : ℂT[.down, .down]}
     rw [perm_tensor_eq <| contr_tensor_eq <| neg_contr _]
     rw [perm_tensor_eq <| neg_contr _]
   apply perm_congr _ rfl
-  decide
+  decide-/
 
 end complexLorentzTensor
 

PhysLean/Relativity/Tensors/OverColor/Discrete.lean

@@ -48,7 +48,7 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol
 /-- The isomorphism between `F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)` and
   `(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensor. -/
 def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ≅
-    (lift.obj F).obj (OverColor.mk (![c1 ,c2] : Fin 2 → C)) := by
+    (lift.obj F).obj (OverColor.mk (![c1, c2] : Fin 2 → C)) := by
   symm
   apply ((lift.obj F).mapIso fin2Iso).trans
   apply (Functor.Monoidal.μIso (lift.obj F).toFunctor _ _).symm.trans
@@ -68,7 +68,7 @@ def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)
 
 lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discrete.mk c2)) :
     ((pairIsoSep F).hom.hom :
-      (F.obj (Discrete.mk c1)).V ⊗ (F.obj (Discrete.mk c2)).V ⟶  _ ) (x ⊗ₜ[k] y) =
+      (F.obj (Discrete.mk c1)).V ⊗ (F.obj (Discrete.mk c2)).V ⟶ _) (x ⊗ₜ[k] y) =
     PiTensorProduct.tprod k (Fin.cases x (Fin.cases y (fun i => Fin.elim0 i))) := by
   conv_lhs =>
     simp only [Action.instMonoidalCategory_tensorObj_V, Nat.succ_eq_add_one, Nat.reduceAdd,

PhysLean/Relativity/Tensors/OverColor/Lift.lean

@@ -58,6 +58,14 @@ def discreteFunctorMapEqIso {c1 c2 : Discrete C} (h : c1.as = c2.as) :
   (by rw [← ModuleCat.hom_id, ← ModuleCat.hom_comp, Action.inv_hom_hom])
   (by rw [← ModuleCat.hom_id, ← ModuleCat.hom_comp, Action.hom_inv_hom])
 
+lemma discreteFunctorMapEqIso_eq_action {c1 c2 : Discrete C} (h : c1.as = c2.as) :
+    discreteFunctorMapEqIso F h = ((Action.forget _ _).mapIso
+    (F.mapIso (Discrete.eqToIso (by simp [h])))).toLinearEquiv := by
+  ext x
+  simp only [discreteFunctorMapEqIso, Functor.mapIso_hom, eqToIso.hom, Functor.mapIso_inv,
+    eqToIso.inv, LinearEquiv.ofLinear_apply, Action.forget_obj]
+  rfl
+
 lemma discreteFunctorMapEqIso_comm_ρ {c1 c2 : Discrete C} (h : c1.as = c2.as) (M : G)
     (x : F.obj c1) : discreteFunctorMapEqIso F h ((F.obj c1).ρ M x) =
     (F.obj c2).ρ M (discreteFunctorMapEqIso F h x) := by

PhysLean/Relativity/Tensors/TensorSpecies/Basic.lean

@@ -95,6 +95,9 @@ instance : Group S.G := S.G_group
 /-- The field `repDim` of a `TensorSpecies` is non-zero for all colors. -/
 instance (c : S.C) : NeZero (S.repDim c) := S.repDim_neZero c
 
+@[simp]
+lemma τ_τ_apply (c : S.C) : S.τ (S.τ c) = c := S.τ_involution c
+
 lemma FD_map_basis {c c1 : S.C} (h : c = c1) (i : Fin (S.repDim c)) :
     (S.FD.map (Discrete.eqToHom h)).hom.hom (S.basis c i)
     = S.basis c1 (Fin.cast (by simp [h]) i) := by
@@ -155,6 +158,20 @@ lemma castFin0ToField_tprod {c : Fin 0 → S.C}
 
 /-!
 
+## Some properties of contractions
+
+-/
+
+lemma contr_congr (c c' : S.C) (h : c = c') (x : S.FD.obj (Discrete.mk c))
+    (y : S.FD.obj (Discrete.mk (S.τ c))) :
+    (S.contr.app { as := c }).hom (x ⊗ₜ[k] y) =
+    (S.contr.app { as := c' }).hom
+    ((S.FD.map (Discrete.eqToHom (by simp [h]))).hom x ⊗ₜ
+    (S.FD.map (Discrete.eqToHom (by simp [h]))).hom y) := by
+  subst h
+  simp
+/-!
+
 ## Evalutation of indices.
 
 -/

PhysLean/Relativity/Tensors/TensorSpecies/Pure.lean

@@ -1,81 +0,0 @@
-/-
-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 PhysLean.Relativity.Tensors.TensorSpecies.Basic
-/-!
-
-# Pure tensors
-
-A pure tensor is one of the form `ψ1 ⊗ ψ2 ⊗ ... ⊗ ψn`.
-We say a tensor is pure if it is of this form.
-
--/
-
-open IndexNotation
-open CategoryTheory
-open MonoidalCategory
-
-noncomputable section
-
-namespace TensorSpecies
-variable {k : Type} [CommRing k] (S : TensorSpecies k)
-
-/-- 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 {k : Type} [CommRing k] {S : TensorSpecies k} {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 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', LaxBraidedFunctor.of_toFunctor,
-    OverColor.lift.objObj', Functor.id_obj, Rep.coe_of, tprod, Rep.of_ρ, MonoidHom.coe_mk,
-    OneHom.coe_mk, PiTensorProduct.map_tprod]
-  rfl
-
-end Pure
-
-/-- A tensor is pure if it is `⨂[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 k 1 fun i => 0
-  symm
-  apply PiTensorProduct.zero_tprodCoeff' (1 : 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

PhysLean/Relativity/Tensors/Tree/EquivalenceClass/Basic.lean

@@ -1,289 +0,0 @@
-/-
-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.Tree.Basic
-import PhysLean.Relativity.Tensors.Tree.NodeIdentities.Basic
-/-!
-
-## Equivalence class on Tensor Trees
-
-This file contains the basic node identities for tensor trees.
-More complicated identities appear in there own files.
-
--/
-
-open IndexNotation
-open CategoryTheory
-open MonoidalCategory
-open OverColor
-open PhysLean.Fin
-open TensorProduct
-
-namespace TensorTree
-
-variable {k : Type} [CommRing k] {S : TensorSpecies k}
-
-/-- The relation `tensorRel` on `TensorTree S c` is defined such that `tensorRel t1 t2` is true
-  if `t1` and `t2` have the same underlying tensors. -/
-def tensorRel {n} {c : Fin n → S.C} (t1 t2 : TensorTree S c) : Prop := t1.tensor = t2.tensor
-
-lemma tensorRel_refl {n} {c : Fin n → S.C} (t : TensorTree S c) : tensorRel t t := rfl
-
-lemma tensorRel_symm {n} {c : Fin n → S.C} {t1 t2 : TensorTree S c} :
-    tensorRel t1 t2 → tensorRel t2 t1 :=
-  Eq.symm
-
-lemma tensorRel_trans {n} {c : Fin n → S.C} {t1 t2 t3 : TensorTree S c} :
-    tensorRel t1 t2 → tensorRel t2 t3 → tensorRel t1 t3 := Eq.trans
-
-lemma tensorRel_equivalence {n} (c : Fin n → S.C) :
-    Equivalence (tensorRel (c := c) (S := S)) :=
-  { refl := tensorRel_refl,
-    symm := tensorRel_symm,
-    trans := tensorRel_trans}
-
-instance tensorTreeSetoid {n} (c : Fin n → S.C) : Setoid (TensorTree S c) :=
-  Setoid.mk (tensorRel (c := c) (S := S)) (tensorRel_equivalence c)
-
-/-- The equivalence classes of `TensorTree` under the relation `tensorRel`. -/
-def _root_.TensorSpecies.TensorTreeQuot (S : TensorSpecies k) {n} (c : Fin n → S.C) : Type :=
-    Quot (tensorRel (c := c))
-
-namespace TensorTreeQuot
-
-/-- The projection from `TensorTree` down to `TensorTreeQuot`. -/
-def ι {n} {c : Fin n → S.C} (t : TensorTree S c) : S.TensorTreeQuot c := Quot.mk _ t
-
-lemma ι_surjective {n} {c : Fin n → S.C} : Function.Surjective (ι (c := c)) := by
-  simp only [Function.Surjective]
-  exact fun b => Quotient.exists_rep b
-
-lemma ι_apply_eq_iff_tensorRel {n} {c : Fin n → S.C} {t1 t2 : TensorTree S c} :
-    ι t1 = ι t2 ↔ tensorRel t1 t2 := by
-  simp only [ι]
-  rw [Equivalence.quot_mk_eq_iff (tensorRel_equivalence c)]
-
-lemma ι_apply_eq_iff_tensor_apply_eq {n} {c : Fin n → S.C} {t1 t2 : TensorTree S c} :
-    ι t1 = ι t2 ↔ t1.tensor = t2.tensor := by
-  rw [ι_apply_eq_iff_tensorRel]
-  simp [tensorRel]
-
-/-!
-
-## Addition and smul
-
--/
-
-/-- The addition of two equivalence classes of tensor trees. -/
-def addQuot {n} {c : Fin n → S.C} :
-    S.TensorTreeQuot c → S.TensorTreeQuot c → S.TensorTreeQuot c := by
-  refine Quot.lift₂ (fun t1 t2 => ι (t1.add t2)) ?_ ?_
-  · intro t1 t2  t3 h1
-    simp only [tensorRel] at h1
-    simp only
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    rw [add_tensor, add_tensor, h1]
-  · intro t1 t2 t3 h1
-    simp only [tensorRel] at h1
-    simp only
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    rw [add_tensor, add_tensor, h1]
-
-lemma ι_add_eq_addQuot {n} {c : Fin n → S.C} (t1 t2 : TensorTree S c) :
-    ι (t1.add t2) = addQuot (ι t1) (ι t2) := rfl
-
-/-- The scalar multiplication of an equivalence classes of tensor trees. -/
-def smulQuot {n} {c : Fin n → S.C} (r : k) :
-    S.TensorTreeQuot c → S.TensorTreeQuot c := by
-  refine Quot.lift (fun t => ι (smul r t)) ?_
-  · intro t1 t2 h
-    simp only [tensorRel] at h
-    simp only
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    rw [smul_tensor, smul_tensor, h]
-
-lemma ι_smul_eq_smulQuot {n} {c : Fin n → S.C} (r : k) (t : TensorTree S c) :
-    ι (smul r t) = smulQuot r (ι t) := rfl
-
-noncomputable instance {n} (c : Fin n → S.C) : AddCommMonoid (S.TensorTreeQuot c) where
-  add := addQuot
-  zero := ι zeroTree
-  nsmul := fun n t => smulQuot (n : k) t
-  add_assoc := by
-    intro a b c
-    obtain ⟨a, rfl⟩ := ι_surjective a
-    obtain ⟨b, rfl⟩ := ι_surjective b
-    obtain ⟨c, rfl⟩ := ι_surjective c
-    change addQuot (addQuot (ι a) (ι b)) (ι c) = addQuot (ι a) (addQuot (ι b) (ι c))
-    rw [← ι_add_eq_addQuot, ← ι_add_eq_addQuot, ← ι_add_eq_addQuot, ← ι_add_eq_addQuot]
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    rw [add_assoc]
-  zero_add := by
-    intro a
-    obtain ⟨a, rfl⟩ := ι_surjective a
-    change addQuot (ι zeroTree) (ι a) = _
-    rw [← ι_add_eq_addQuot, ι_apply_eq_iff_tensor_apply_eq]
-    rw [TensorTree.zero_add]
-  add_zero := by
-    intro a
-    obtain ⟨a, rfl⟩ := ι_surjective a
-    change addQuot (ι a) (ι zeroTree) = _
-    rw [← ι_add_eq_addQuot, ι_apply_eq_iff_tensor_apply_eq]
-    rw [TensorTree.add_zero]
-  add_comm := by
-    intro a b
-    obtain ⟨a, rfl⟩ := ι_surjective a
-    obtain ⟨b, rfl⟩ := ι_surjective b
-    change addQuot (ι a) (ι b) = addQuot (ι b) (ι a)
-    rw [← ι_add_eq_addQuot, ← ι_add_eq_addQuot, ι_apply_eq_iff_tensor_apply_eq]
-    rw [add_comm]
-  nsmul_zero t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    simp only [Nat.cast_zero]
-    change smulQuot ((0 : k)) (ι t) = ι zeroTree
-    rw [← ι_smul_eq_smulQuot]
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    rw [zero_smul]
-  nsmul_succ n t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    simp only [Nat.cast_add, Nat.cast_one]
-    change smulQuot ((n: k) + 1) (ι t) = addQuot (smulQuot (n : k) (ι t)) (ι t)
-    rw [← ι_smul_eq_smulQuot, ← ι_smul_eq_smulQuot, ← ι_add_eq_addQuot,
-      ι_apply_eq_iff_tensor_apply_eq]
-    simp only [smul_tensor, add_tensor]
-    rw [add_smul]
-    simp
-
-instance {n} {c : Fin n → S.C} : Module k (S.TensorTreeQuot c) where
-  smul r t := smulQuot r t
-  one_smul t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    change smulQuot (1 : k) (ι t) = ι t
-    rw [← ι_smul_eq_smulQuot]
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    rw [TensorTree.smul_one]
-  mul_smul r s t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    change smulQuot (r * s) (ι t) = smulQuot r (smulQuot s (ι t))
-    rw [← ι_smul_eq_smulQuot, ← ι_smul_eq_smulQuot,  ← ι_smul_eq_smulQuot,
-      ι_apply_eq_iff_tensor_apply_eq]
-    simp [smul_tensor, mul_smul]
-  smul_add r t1 t2 := by
-    obtain ⟨t1, rfl⟩ := ι_surjective t1
-    obtain ⟨t2, rfl⟩ := ι_surjective t2
-    change smulQuot r (addQuot (ι t1) (ι t2)) = addQuot (smulQuot r (ι t1)) (smulQuot r (ι t2))
-    rw [← ι_smul_eq_smulQuot, ← ι_smul_eq_smulQuot,  ← ι_add_eq_addQuot, ← ι_add_eq_addQuot,
-      ← ι_smul_eq_smulQuot, ι_apply_eq_iff_tensor_apply_eq]
-    simp [smul_tensor, add_tensor]
-  smul_zero a := by
-    change smulQuot (a : k) (ι zeroTree) = ι zeroTree
-    rw [← ι_smul_eq_smulQuot]
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    simp [smul_tensor, zero_smul]
-  add_smul r s t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    change smulQuot (r + s) (ι t)  = addQuot (smulQuot r (ι t)) (smulQuot s (ι t))
-    rw [← ι_smul_eq_smulQuot, ← ι_smul_eq_smulQuot,    ← ι_smul_eq_smulQuot,
-      ← ι_add_eq_addQuot, ι_apply_eq_iff_tensor_apply_eq]
-    simp [smul_tensor, add_tensor, add_smul]
-  zero_smul t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    change smulQuot (0 : k) (ι t) = ι zeroTree
-    rw [← ι_smul_eq_smulQuot]
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    simp [smul_tensor, zero_smul]
-
-lemma add_eq_addQuot {n} {c : Fin n → S.C} (t1 t2 : S.TensorTreeQuot c) :
-    t1 + t2 = addQuot t1 t2 := rfl
-
-@[simp]
-lemma ι_add_eq_add {n} {c : Fin n → S.C} (t1 t2 : TensorTree S c) :
-    ι (t1.add t2) =  (ι t1) + (ι t2) := rfl
-
-lemma smul_eq_smulQuot {n} {c : Fin n → S.C} (r : k) (t : S.TensorTreeQuot c) :
-    r • t = smulQuot r t := rfl
-
-@[simp]
-lemma ι_smul_eq_smul {n} {c : Fin n → S.C} (r : k) (t : TensorTree S c) :
-    ι (smul r t) = r • (ι t) := rfl
-
-/-!
-
-## The group action
-
--/
-
-/-- The group action on an equivalence classes of tensor trees. -/
-def actionQuot {n} {c : Fin n → S.C} (g : S.G) :
-    S.TensorTreeQuot c → S.TensorTreeQuot c := by
-  refine Quot.lift (fun t => ι (action g t)) ?_
-  · intro t1 t2 h
-    simp only [tensorRel] at h
-    simp only
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    rw [action_tensor, action_tensor, h]
-
-lemma ι_action_eq_actionQuot {n} {c : Fin n → S.C} (g : S.G) (t : TensorTree S c) :
-    ι (action g t) = actionQuot g (ι t) := rfl
-
-noncomputable instance {n} {c : Fin n → S.C} : MulAction S.G (S.TensorTreeQuot c) where
-  smul := actionQuot
-  one_smul t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    change actionQuot (1 : S.G) (ι t) = ι t
-    rw [← ι_action_eq_actionQuot]
-    rw [ι_apply_eq_iff_tensor_apply_eq]
-    simp [action_tensor]
-  mul_smul g h t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    change actionQuot (g * h) (ι t) = actionQuot g (actionQuot h (ι t))
-    rw [← ι_action_eq_actionQuot, ← ι_action_eq_actionQuot,
-      ← ι_action_eq_actionQuot, ι_apply_eq_iff_tensor_apply_eq]
-    simp [action_tensor]
-
-@[simp]
-lemma ι_action_eq_mulAction {n} {c : Fin n → S.C} (g : S.G) (t : TensorTree S c) :
-    ι (action g t) = g • (ι t) := rfl
-
-/-!
-
-## To Tensors
-
--/
-
-/-- The underlying tensor for an equivalence class of tensor trees. -/
-noncomputable def tensorQuot {n} {c : Fin n → S.C} :
-    S.TensorTreeQuot c →ₗ[k] S.F.obj (OverColor.mk c) where
-  toFun := by
-    refine Quot.lift (fun t => t.tensor) ?_
-    intro t1 t2 h
-    simp only [tensorRel] at h
-    simp only
-    rw [h]
-  map_add' t1 t2 := by
-    obtain ⟨t1, rfl⟩ := ι_surjective t1
-    obtain ⟨t2, rfl⟩ := ι_surjective t2
-    rw [← ι_add_eq_add]
-    change ((t1.add t2)).tensor = (t1).tensor + (t2).tensor
-    simp [add_tensor]
-  map_smul' r t := by
-    obtain ⟨t, rfl⟩ := ι_surjective t
-    rw [← ι_smul_eq_smul]
-    change (smul r t).tensor = r • t.tensor
-    simp [smul_tensor]
-
-lemma tensor_eq_tensorQuot_apply {n} {c : Fin n → S.C} (t : TensorTree S c) :
-    (t).tensor = tensorQuot (ι t) := rfl
-
-lemma tensorQuot_surjective {n} {c : Fin n → S.C} : Function.Surjective (tensorQuot (c := c)) := by
-  simp only [Function.Surjective]
-  intro t
-  use ι (tensorNode t)
-  rw [← tensor_eq_tensorQuot_apply]
-  simp
-
-end TensorTreeQuot
-
-end TensorTree