Tensor trees

• Tensor trees provide an abstract way to represent tensor expressions.
• Their nodes are either tensors or operations between tensors.
• Every tensor tree has associated with an underlying tensor.
• This is not a one-to-one correspondence. Lots tensor trees represent the same tensor. In the same way that lots of tensor expressions represent the same tensor.
• Define a sub-tensor tree as a node of a tensor tree and all child nodes thereof. One can replace sub-tensor tree with another tensor tree which has the same underlying tensor without changing the underlying tensor of the parent tensor tree. These appear as the e.g. the lemmas contr_tensor_eq in what follows.

inductive TensorTree (S : TensorSpecies) {n : ℕ} : (Fin n → S.C) → Type

A syntax tree for tensor expressions.

• tensorNode {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (T : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V) : TensorTree S c

  A general tensor node.

• smul {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c

  A node corresponding to the scalar multiple of a tensor by a element of the field.

• neg {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c

  A node corresponding to negation of a tensor.

• add {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c → TensorTree S c

  A node corresponding to the addition of two tensors.

• action {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : S.G → TensorTree S c → TensorTree S c

  A node corresponding to the action of a group element on a tensor.

• perm {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) (t : TensorTree S c) : TensorTree S c1

  A node corresponding to the permutation of indices of a tensor.

• prod {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t : TensorTree S c) (t1 : TensorTree S c1) : TensorTree S (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)

  A node corresponding to the product of two tensors.

• contr {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : TensorTree S c → TensorTree S (c ∘ i.succAbove ∘ j.succAbove)

  A node corresponding to the contraction of indices of a tensor.

• eval {S : TensorSpecies} {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (x : ℕ) : TensorTree S c → TensorTree S (c ∘ i.succAbove)

  A node corresponding to the evaluation of an index of a tensor.

Composite nodes

def TensorTree.vecNode {S : TensorSpecies} {c : S.C} (v : ↑(S.FD.obj { as := c }).V) : TensorTree S ![c]

A node consisting of a single vector.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev TensorTree.vecNodeE (S : TensorSpecies) (c1 : S.C) (v : ↑(S.FD.obj { as := c1 }).V) : TensorTree S ![c1]

The node vecNode of a tensor tree, with all arguments explicit.

Equations

• TensorTree.vecNodeE S c1 v = TensorTree.vecNode v

def TensorTree.twoNode {S : TensorSpecies} {c1 c2 : S.C} (t : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })).V) : TensorTree S ![c1, c2]

A node consisting of a two tensor.

Equations

• TensorTree.twoNode t = TensorTree.tensorNode ((CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).hom.hom) t)

@[reducible, inline]

abbrev TensorTree.twoNodeE (S : TensorSpecies) (c1 c2 : S.C) (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })).V) : TensorTree S ![c1, c2]

The node twoNode of a tensor tree, with all arguments explicit.

Equations

• TensorTree.twoNodeE S c1 c2 v = TensorTree.twoNode v

def TensorTree.threeNode {S : TensorSpecies} {c1 c2 c3 : S.C} (t : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c2 }) (S.FD.obj { as := c3 }))).V) : TensorTree S ![c1, c2, c3]

A node consisting of a three tensor.

Equations

• TensorTree.threeNode t = TensorTree.tensorNode ((CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.tripleIsoSep S.FD).hom.hom) t)

@[reducible, inline]

abbrev TensorTree.threeNodeE (S : TensorSpecies) (c1 c2 c3 : S.C) (v : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c2 }) (S.FD.obj { as := c3 }))).V) : TensorTree S ![c1, c2, c3]

The node threeNode of a tensor tree, with all arguments explicit.

Equations

• TensorTree.threeNodeE S c1 c2 c3 v = TensorTree.threeNode v

def TensorTree.constNode {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (T : 𝟙_ (Rep S.k S.G) ⟶ S.F.obj (IndexNotation.OverColor.mk c)) : TensorTree S c

A general constant node.

Equations

• TensorTree.constNode T = TensorTree.tensorNode ((CategoryTheory.ConcreteCategory.hom T.hom) 1)

def TensorTree.constVecNode {S : TensorSpecies} {c : S.C} (v : 𝟙_ (Rep S.k S.G) ⟶ S.FD.obj { as := c }) : TensorTree S ![c]

A constant vector.

Equations

• TensorTree.constVecNode v = TensorTree.vecNode ((CategoryTheory.ConcreteCategory.hom v.hom) 1)

def TensorTree.constTwoNode {S : TensorSpecies} {c1 c2 : S.C} (v : 𝟙_ (Rep S.k S.G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })) : TensorTree S ![c1, c2]

A constant two tensor (e.g. metric and unit).

Equations

• TensorTree.constTwoNode v = TensorTree.twoNode ((CategoryTheory.ConcreteCategory.hom v.hom) 1)

@[reducible, inline]

abbrev TensorTree.constTwoNodeE (S : TensorSpecies) (c1 c2 : S.C) (v : 𝟙_ (Rep S.k S.G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })) : TensorTree S ![c1, c2]

The node constTwoNode of a tensor tree, with all arguments explicit.

Equations

• TensorTree.constTwoNodeE S c1 c2 v = TensorTree.constTwoNode v

def TensorTree.constThreeNode {S : TensorSpecies} {c1 c2 c3 : S.C} (v : 𝟙_ (Rep S.k S.G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c2 }) (S.FD.obj { as := c3 }))) : TensorTree S ![c1, c2, c3]

A constant three tensor (e.g. Pauli matrices).

Equations

• TensorTree.constThreeNode v = TensorTree.threeNode ((CategoryTheory.ConcreteCategory.hom v.hom) 1)

@[reducible, inline]

abbrev TensorTree.constThreeNodeE (S : TensorSpecies) (c1 c2 c3 : S.C) (v : 𝟙_ (Rep S.k S.G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c2 }) (S.FD.obj { as := c3 }))) : TensorTree S ![c1, c2, c3]

The node constThreeNode of a tensor tree, with all arguments explicit.

Equations

• TensorTree.constThreeNodeE S c1 c2 c3 v = TensorTree.constThreeNode v

Other operations.

def TensorTree.size {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : TensorTree S c → ℕ

The number of nodes in a tensor tree.

Equations

• (TensorTree.tensorNode T).size = 1
• (t1.add t2).size = t1.size + t2.size + 1
• (TensorTree.perm σ t).size = t.size + 1
• t.neg.size = t.size + 1
• (TensorTree.smul a t).size = t.size + 1
• (t1.prod t2).size = t1.size + t2.size + 1
• (TensorTree.contr i j h t).size = t.size + 1
• (TensorTree.eval i x_1 t).size = t.size + 1
• (TensorTree.action a t).size = t.size + 1

def TensorTree.tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : TensorTree S c → ↑(S.F.obj (IndexNotation.OverColor.mk c)).V

The underlying tensor a tensor tree corresponds to.

def TensorTree.field {S : TensorSpecies} {c : Fin 0 → S.C} (t : TensorTree S c) : S.k

Takes a tensor tree based on Fin 0, into the field S.k.

Equations

• t.field = S.castFin0ToField t.tensor

Tensor on different nodes.

@[simp]

theorem TensorTree.tensorNode_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (T : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V) : (tensorNode T).tensor = T

@[simp]

theorem TensorTree.constTwoNode_tensor {S : TensorSpecies} {c1 c2 : S.C} (v : 𝟙_ (Rep S.k S.G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })) : (constTwoNode v).tensor = (CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).hom.hom) ((CategoryTheory.ConcreteCategory.hom v.hom) 1)

@[simp]

theorem TensorTree.constThreeNode_tensor {S : TensorSpecies} {c1 c2 c3 : S.C} (v : 𝟙_ (Rep S.k S.G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c2 }) (S.FD.obj { as := c3 }))) : (constThreeNode v).tensor = (CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.tripleIsoSep S.FD).hom.hom) ((CategoryTheory.ConcreteCategory.hom v.hom) 1)

theorem TensorTree.prod_tensor {S : TensorSpecies} {n m : ℕ} {c1 : Fin n → S.C} {c2 : Fin m → S.C} (t1 : TensorTree S c1) (t2 : TensorTree S c2) : (t1.prod t2).tensor = (CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk c1) (IndexNotation.OverColor.mk c2)).hom) (t1.tensor ⊗ₜ[S.k] t2.tensor))

theorem TensorTree.add_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (t1 t2 : TensorTree S c) : (t1.add t2).tensor = t1.tensor + t2.tensor

theorem TensorTree.perm_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {n✝ : ℕ} {c1 : Fin n✝ → S.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) (t : TensorTree S c) : (perm σ t).tensor = (CategoryTheory.ConcreteCategory.hom (S.F.map σ).hom) t.tensor

theorem TensorTree.contr_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = S.τ (c i)} (t : TensorTree S c) : (contr i j h t).tensor = (CategoryTheory.ConcreteCategory.hom (S.contrMap c i j h).hom) t.tensor

theorem TensorTree.neg_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (t : TensorTree S c) : t.neg.tensor = -t.tensor

theorem TensorTree.eval_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t : TensorTree S c) : (eval i e t).tensor = (CategoryTheory.ConcreteCategory.hom (S.evalMap i (Fin.ofNat' (S.repDim (c i)) e))) t.tensor

theorem TensorTree.smul_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (a : S.k) (T : TensorTree S c) : (smul a T).tensor = a • T.tensor

theorem TensorTree.action_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (g : S.G) (T : TensorTree S c) : (action g T).tensor = ((S.F.obj (IndexNotation.OverColor.mk c)).ρ g) T.tensor

Equality of tensors and rewrites.

theorem TensorTree.contr_tensor_eq {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} {T1 T2 : TensorTree S c} (h : T1.tensor = T2.tensor) {i : Fin n.succ.succ} {j : Fin n.succ} {h' : c (i.succAbove j) = S.τ (c i)} : (contr i j h' T1).tensor = (contr i j h' T2).tensor

theorem TensorTree.prod_tensor_eq_fst {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} {T1 T1' : TensorTree S c} {T2 : TensorTree S c1} (h : T1.tensor = T1'.tensor) : (T1.prod T2).tensor = (T1'.prod T2).tensor

theorem TensorTree.prod_tensor_eq_snd {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} {T1 : TensorTree S c} {T2 T2' : TensorTree S c1} (h : T2.tensor = T2'.tensor) : (T1.prod T2).tensor = (T1.prod T2').tensor

theorem TensorTree.perm_tensor_eq {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} {σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1} {T1 T2 : TensorTree S c} (h : T1.tensor = T2.tensor) : (perm σ T1).tensor = (perm σ T2).tensor

theorem TensorTree.add_tensor_eq_fst {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 T1' T2 : TensorTree S c} (h : T1.tensor = T1'.tensor) : (T1.add T2).tensor = (T1'.add T2).tensor

theorem TensorTree.add_tensor_eq_snd {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 T2 T2' : TensorTree S c} (h : T2.tensor = T2'.tensor) : (T1.add T2).tensor = (T1.add T2').tensor

theorem TensorTree.add_tensor_eq {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 T1' T2 T2' : TensorTree S c} (h1 : T1.tensor = T1'.tensor) (h2 : T2.tensor = T2'.tensor) : (T1.add T2).tensor = (T1'.add T2').tensor

theorem TensorTree.neg_tensor_eq {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 T2 : TensorTree S c} (h : T1.tensor = T2.tensor) : T1.neg.tensor = T2.neg.tensor

theorem TensorTree.smul_tensor_eq {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 T2 : TensorTree S c} {a : S.k} (h : T1.tensor = T2.tensor) : (smul a T1).tensor = (smul a T2).tensor

theorem TensorTree.action_tensor_eq {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 T2 : TensorTree S c} {g : S.G} (h : T1.tensor = T2.tensor) : (action g T1).tensor = (action g T2).tensor

theorem TensorTree.smul_mul_eq {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 : TensorTree S c} {a b : S.k} (h : a = b) : (smul a T1).tensor = (smul b T1).tensor

theorem TensorTree.eq_tensorNode_of_eq_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 : TensorTree S c} {t : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V} (h : T1.tensor = t) : T1.tensor = (tensorNode t).tensor

Properties on basis.

theorem TensorTree.tensorNode_tensorBasis_repr {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (T : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V) : (S.tensorBasis c).repr (tensorNode T).tensor = (S.tensorBasis c).repr T

@[simp]

theorem TensorTree.add_tensorBasis_repr {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (t1 t2 : TensorTree S c) : (S.tensorBasis c).repr (t1.add t2).tensor = (S.tensorBasis c).repr t1.tensor + (S.tensorBasis c).repr t2.tensor

theorem TensorTree.prod_tensorBasis_repr_apply {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t : TensorTree S c) (t1 : TensorTree S c1) (b : (j : Fin (n + m)) → Fin (S.repDim ((Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm) j))) : ((S.tensorBasis (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)).repr (t.prod t1).tensor) b = ((S.tensorBasis c).repr t.tensor) (TensorSpecies.TensorBasis.prodEquiv b).1 * ((S.tensorBasis c1).repr t1.tensor) (TensorSpecies.TensorBasis.prodEquiv b).2

theorem TensorTree.contr_tensorBasis_repr_apply {S : TensorSpecies} {n : ℕ} {c : Fin (n + 1 + 1) → S.C} {i : Fin (n + 1 + 1)} {j : Fin (n + 1)} {h : c (i.succAbove j) = S.τ (c i)} (t : TensorTree S c) (b : (k : Fin n) → Fin (S.repDim (c (i.succAbove (j.succAbove k))))) : ((S.tensorBasis (c ∘ i.succAbove ∘ j.succAbove)).repr (contr i j h t).tensor) b = ∑ b' : { x : (k : Fin n.succ.succ) → Fin (S.repDim (c k)) // x ∈ TensorSpecies.TensorBasis.ContrSection b }, ((S.tensorBasis c).repr t.tensor) ↑b' * S.castToField ((CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c i }).hom) ((S.basis (c i)) (↑b' i) ⊗ₜ[S.k] (S.basis (S.τ (c i))) (Fin.cast ⋯ (↑b' (i.succAbove j)))))

theorem TensorTree.contr_tensorBasis_repr_apply_eq {S : TensorSpecies} {n : ℕ} {c : Fin (n + 1 + 1) → S.C} {i : Fin (n + 1 + 1)} {j : Fin (n + 1)} {h : c (i.succAbove j) = S.τ (c i)} (t : TensorTree S c) (b : (k : Fin n) → Fin (S.repDim (c (i.succAbove (j.succAbove k))))) (a : S.k) : ((S.tensorBasis (c ∘ i.succAbove ∘ j.succAbove)).repr (contr i j h t).tensor) b = a ↔ ∑ b' : { x : (k : Fin n.succ.succ) → Fin (S.repDim (c k)) // x ∈ TensorSpecies.TensorBasis.ContrSection b }, ((S.tensorBasis c).repr t.tensor) ↑b' * S.castToField ((CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c i }).hom) ((S.basis (c i)) (↑b' i) ⊗ₜ[S.k] (S.basis (S.τ (c i))) (Fin.cast ⋯ (↑b' (i.succAbove j))))) = a

@[simp]

theorem TensorTree.perm_tensorBasis_repr_apply {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} {σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1} (t : TensorTree S c) (b : (j : Fin m) → Fin (S.repDim (c1 j))) : ((S.tensorBasis c1).repr (perm σ t).tensor) b = ((S.tensorBasis c).repr t.tensor) ((TensorSpecies.TensorBasis.congr (IndexNotation.OverColor.Hom.toEquiv σ) ⋯) b)

@[simp]

theorem TensorTree.smul_tensorBasis_repr {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (a : S.k) (T : TensorTree S c) : (S.tensorBasis c).repr (smul a T).tensor = a • (S.tensorBasis c).repr T.tensor

theorem TensorTree.smul_tensorBasis_repr_apply {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (a : S.k) (T : TensorTree S c) (b : (j : Fin n) → Fin (S.repDim (c j))) : ((S.tensorBasis c).repr (smul a T).tensor) b = a * ((S.tensorBasis c).repr T.tensor) b

@[simp]

theorem TensorTree.neg_tensorBasis_repr {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (t : TensorTree S c) : (S.tensorBasis c).repr t.neg.tensor = -(S.tensorBasis c).repr t.tensor

The zero tensor tree

def TensorTree.zeroTree {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : TensorTree S c

The zero tensor tree.

Equations

• TensorTree.zeroTree = TensorTree.tensorNode 0

@[simp]

theorem TensorTree.zeroTree_tensor {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : zeroTree.tensor = 0

theorem TensorTree.zero_smul {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 : TensorTree S c} : (smul 0 T1).tensor = zeroTree.tensor

theorem TensorTree.smul_zero {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {a : S.k} : (smul a zeroTree).tensor = zeroTree.tensor

theorem TensorTree.zero_add {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 : TensorTree S c} : (zeroTree.add T1).tensor = T1.tensor

theorem TensorTree.add_zero {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} {T1 : TensorTree S c} : (T1.add zeroTree).tensor = T1.tensor

theorem TensorTree.perm_zero {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) : (perm σ zeroTree).tensor = zeroTree.tensor

theorem TensorTree.neg_zero {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} : zeroTree.neg.tensor = zeroTree.tensor

theorem TensorTree.contr_zero {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = S.τ (c i)} : (contr i j h zeroTree).tensor = zeroTree.tensor

theorem TensorTree.zero_prod {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t : TensorTree S c1) : (zeroTree.prod t).tensor = zeroTree.tensor

theorem TensorTree.prod_zero {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t : TensorTree S c) : (t.prod zeroTree).tensor = zeroTree.tensor

structure TensorTree.ContrPair {S : TensorSpecies} {n : ℕ} (c : Fin n.succ.succ → S.C) : Type

A structure containing a pair of indices (i, j) to be contracted in a tensor. This is used in some proofs of node identities for tensor trees.

• i : Fin n.succ.succ

  The first index in the pair, appearing on the left in the contraction node contr i j h _.

• j : Fin n.succ

  The second index in the pair, appearing on the right in the contraction node contr i j h _.

• h : c (self.i.succAbove self.j) = S.τ (c self.i)

  A proof that the two indices can be contracted.

theorem TensorTree.ContrPair.ext {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q q' : ContrPair c) (hi : q.i = q'.i) (hj : q.j = q'.j) : q = q'

def TensorTree.ContrPair.contrMap {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : S.F.obj (IndexNotation.OverColor.mk c) ⟶ S.F.obj (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))

The contraction map for a pair of indices.

Equations

• q.contrMap = S.contrMap c q.i q.j ⋯