Basic node identities

This file contains the basic node identities for tensor trees. More complicated identities appear in there own files.

Equality of constructors.

def TensorTree.constVecNode_eq_vecNode : InformalLemma

A constVecNode has equal tensor to the vecNode with the map evaluated at 1.

Equations

• TensorTree.constVecNode_eq_vecNode = { deps := [`TensorTree.constVecNode, `TensorTree.vecNode] }

def TensorTree.constTwoNode_eq_twoNode : InformalLemma

A constTwoNode has equal tensor to the twoNode with the map evaluated at 1.

Equations

• TensorTree.constTwoNode_eq_twoNode = { deps := [`TensorTree.constTwoNode, `TensorTree.twoNode] }

Tensornode

theorem TensorTree.tensorNode_of_tree {S : TensorSpecies} {n✝ : ℕ} {c : Fin n✝ → S.C} (t : TensorTree S c) : (tensorNode t.tensor).tensor = t.tensor

The tensor node of a tensor tree's tensor has a tensor which is the tensor tree's tensor.

Negation

@[simp]

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

Two neg nodes of a tensor tree cancel.

@[simp]

theorem TensorTree.neg_fst_prod {S : TensorSpecies} {n m : ℕ} {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1) (T2 : TensorTree S c2) : (T1.neg.prod T2).tensor = (T1.prod T2).neg.tensor

A neg node can be moved out of the LHS of a prod node.

@[simp]

theorem TensorTree.neg_snd_prod {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.neg).tensor = (T1.prod T2).neg.tensor

A neg node can be moved out of the RHS of a prod node.

@[simp]

theorem TensorTree.neg_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)} (t : TensorTree S c) : (contr i j h t.neg).tensor = (contr i j h t).neg.tensor

A neg node can be moved through a contr node.

theorem TensorTree.neg_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) : (perm σ t.neg).tensor = (perm σ t).neg.tensor

A neg node can be moved through a perm node.

@[simp]

theorem TensorTree.neg_add {S : TensorSpecies} {n✝ : ℕ} {c : Fin n✝ → S.C} (t : TensorTree S c) : (t.neg.add t).tensor = 0

The negation of a tensor tree plus itself is zero.

@[simp]

theorem TensorTree.add_neg {S : TensorSpecies} {n✝ : ℕ} {c : Fin n✝ → S.C} (t : TensorTree S c) : (t.add t.neg).tensor = 0

A tensor tree plus its negation is zero.

Basic perm identities

theorem TensorTree.perm_perm {S : TensorSpecies} {n n1 n2 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} {c2 : Fin n2 → S.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) (σ2 : IndexNotation.OverColor.mk c1 ⟶ IndexNotation.OverColor.mk c2) (t : TensorTree S c) : (perm σ2 (perm σ t)).tensor = (perm (CategoryTheory.CategoryStruct.comp σ σ2) t).tensor

Applying two permutations is the same as applying the transitive permutation.

theorem TensorTree.perm_id {S : TensorSpecies} {n✝ : ℕ} {c : Fin n✝ → S.C} (t : TensorTree S c) : (perm (CategoryTheory.CategoryStruct.id (IndexNotation.OverColor.mk c)) t).tensor = t.tensor

Applying the identity permutation is the same as not applying a permutation.

theorem TensorTree.perm_eq_id {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c) (h : σ = CategoryTheory.CategoryStruct.id (IndexNotation.OverColor.mk c)) (t : TensorTree S c) : (perm σ t).tensor = t.tensor

Applying a permutation which is equal to the identity permutation is the same as not applying a permutation.

theorem TensorTree.perm_eq_of_eq_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} {t2 : TensorTree S c1} (h : (perm σ.hom t).tensor = t2.tensor) : t.tensor = (perm σ.inv t2).tensor

Given an equality of tensors corresponding to tensor trees where the tensor tree on the left finishes with a permutation node, this permutation node can be moved to the tensor tree on the right. This lemma holds here for isomorphisms only, but holds in practice more generally.

theorem TensorTree.perm_eq_iff_eq_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} {t2 : TensorTree S c1} : (perm σ t).tensor = t2.tensor ↔ t.tensor = (perm (IndexNotation.OverColor.equivToHomEq (IndexNotation.OverColor.Hom.toEquiv σ).symm ⋯) t2).tensor

A permutation of a tensor tree t1 has equal tensor to a tensor tree t2 if and only if the inverse-permutation of t2 has equal tensor to t1.

Vector based identities

These identities are related to the fact that all the maps are linear.

theorem TensorTree.smul_smul {S : TensorSpecies} {n✝ : ℕ} {c : Fin n✝ → S.C} (t : TensorTree S c) (a b : S.k) : (smul a (smul b t)).tensor = (smul (a * b) t).tensor

Two smul nodes can be replaced with a single smul node with the product of the two scalars.

theorem TensorTree.smul_one {S : TensorSpecies} {n✝ : ℕ} {c : Fin n✝ → S.C} (t : TensorTree S c) : (smul 1 t).tensor = t.tensor

An smul-node with scalar 1 does nothing.

theorem TensorTree.smul_eq_one {S : TensorSpecies} {n✝ : ℕ} {c : Fin n✝ → S.C} (t : TensorTree S c) (a : S.k) (h : a = 1) : (smul a t).tensor = t.tensor

An smul-node with scalar equal to 1 does nothing.

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

The addition node is commutative.

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

The addition node is associative.

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

When the same permutation acts on both arguments of an addition, the permutation can be moved out of the addition.

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

When a perm acts on an add node, it can be moved through the add-node to act on each of the two parts.

theorem TensorTree.perm_smul {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) (a : S.k) (t : TensorTree S c) : (perm σ (smul a t)).tensor = (smul a (perm σ t)).tensor

A smul node can be moved through an perm node.

theorem TensorTree.add_eval {S : TensorSpecies} {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t t1 : TensorTree S c) : ((eval i e t).add (eval i e t1)).tensor = (eval i e (t.add t1)).tensor

When the same evaluation acts on both arguments of an addition, the evaluation can be moved out of the addition.

theorem TensorTree.contr_add {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)} (t1 t2 : TensorTree S c) : (contr i j h (t1.add t2)).tensor = ((contr i j h t1).add (contr i j h t2)).tensor

When a contr acts on an add node, it can be moved through the add-node to act on each of the two parts.

theorem TensorTree.contr_smul {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)} (a : S.k) (t : TensorTree S c) : (contr i j h (smul a t)).tensor = (smul a (contr i j h t)).tensor

A smul node can be moved through an contr node.

@[simp]

theorem TensorTree.add_prod {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t1 t2 : TensorTree S c) (t3 : TensorTree S c1) : ((t1.add t2).prod t3).tensor = ((t1.prod t3).add (t2.prod t3)).tensor

When a prod acts on an add node on the left, it can be moved through the add-node to act on each of the two parts.

@[simp]

theorem TensorTree.prod_add {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t1 : TensorTree S c) (t2 t3 : TensorTree S c1) : (t1.prod (t2.add t3)).tensor = ((t1.prod t2).add (t1.prod t3)).tensor

When a prod acts on an add node on the right, it can be moved through the add-node to act on each of the two parts.

theorem TensorTree.smul_prod {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) : ((smul a t1).prod t2).tensor = (smul a (t1.prod t2)).tensor

A smul node in the LHS of a prod node can be moved through that prod node.

theorem TensorTree.prod_smul {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) : (t1.prod (smul a t2)).tensor = (smul a (t1.prod t2)).tensor

A smul node in the RHS of a prod node can be moved through that prod node.

theorem TensorTree.prod_add_both {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t1 t2 : TensorTree S c) (t3 t4 : TensorTree S c1) : ((t1.add t2).prod (t3.add t4)).tensor = (((t1.prod t3).add (t1.prod t4)).add ((t2.prod t3).add (t2.prod t4))).tensor

When a prod node acts on an add node in both the LHS and RHS entries, it can be moved through both add nodes.

Nodes and the group action.

theorem TensorTree.smul_action {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (g : S.G) (a : S.k) (t : TensorTree S c) : (smul a (action g t)).tensor = (action g (smul a t)).tensor

An action node can be moved through a smul node.

theorem TensorTree.contr_action {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)} (g : S.G) (t : TensorTree S c) : (contr i j h (action g t)).tensor = (action g (contr i j h t)).tensor

An action node can be moved through a contr node.

theorem TensorTree.prod_action {S : TensorSpecies} {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S.G) (t : TensorTree S c) (t1 : TensorTree S c1) : ((action g t).prod (action g t1)).tensor = (action g (t.prod t1)).tensor

An action node can be moved through a prod node when acting on both elements.

theorem TensorTree.add_action {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (g : S.G) (t t1 : TensorTree S c) : ((action g t).add (action g t1)).tensor = (action g (t.add t1)).tensor

An action node can be moved through a add node when acting on both elements.

theorem TensorTree.perm_action {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1) (g : S.G) (t : TensorTree S c) : (perm σ (action g t)).tensor = (action g (perm σ t)).tensor

An action node can be moved through a perm node.

theorem TensorTree.neg_action {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (g : S.G) (t : TensorTree S c) : (action g t).neg.tensor = (action g t.neg).tensor

An action node can be moved through a neg node.

theorem TensorTree.action_action {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (g h : S.G) (t : TensorTree S c) : (action g (action h t)).tensor = (action (g * h) t).tensor

Two action nodes can be combined into a single action node.

theorem TensorTree.action_id {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (t : TensorTree S c) : (action 1 t).tensor = t.tensor

The action node for the identity leaves the tensor invariant.

theorem TensorTree.action_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 })) (g : S.G) : (action g (constTwoNode v)).tensor = (constTwoNode v).tensor

An action node on a constTwoNode leaves the tensor invariant.

theorem TensorTree.action_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 }))) (g : S.G) : (action g (constThreeNode v)).tensor = (constThreeNode v).tensor

An action node on a constThreeNode leaves the tensor invariant.