docs: Node identities for tensor trees
This commit is contained in:
jstoobysmith
parent
20d3dc4dca
commit
d50481ee61
1 changed files with 41 additions and 1 deletions
|
|
@ -54,10 +54,12 @@ lemma tensorNode_of_tree (t : TensorTree S c) : (tensorNode t.tensor).tensor = t
|
|||
|
||||
-/
|
||||
|
||||
/-- Two `neg` nodes of a tensor tree cancle. -/
|
||||
@[simp]
|
||||
lemma neg_neg (t : TensorTree S c) : (neg (neg t)).tensor = t.tensor := by
|
||||
simp only [neg_tensor, _root_.neg_neg]
|
||||
|
||||
/-- A `neg` node can be moved out of the LHS of a `prod` node. -/
|
||||
@[simp]
|
||||
lemma neg_fst_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
|
||||
(T2 : TensorTree S c2) :
|
||||
|
|
@ -66,6 +68,7 @@ lemma neg_fst_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S
|
|||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, neg_tmul, map_neg]
|
||||
|
||||
/-- A `neg` node can be moved out of the RHS of a `prod` node. -/
|
||||
@[simp]
|
||||
lemma neg_snd_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
|
||||
(T2 : TensorTree S c2) :
|
||||
|
|
@ -74,22 +77,26 @@ lemma neg_snd_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S
|
|||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, tmul_neg, map_neg]
|
||||
|
||||
/-- A `neg` node can be moved through a `contr` node. -/
|
||||
@[simp]
|
||||
lemma neg_contr {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 (neg t)).tensor = (neg (contr i j h t)).tensor := by
|
||||
simp only [Nat.succ_eq_add_one, contr_tensor, neg_tensor, map_neg]
|
||||
|
||||
/-- A `neg` node can be moved through a `perm` node. -/
|
||||
lemma neg_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) :
|
||||
(perm σ (neg t)).tensor = (neg (perm σ t)).tensor := by
|
||||
simp only [perm_tensor, neg_tensor, map_neg]
|
||||
|
||||
/-- The negation of a tensor tree plus itself is zero. -/
|
||||
@[simp]
|
||||
lemma neg_add (t : TensorTree S c) : (add (neg t) t).tensor = 0 := by
|
||||
rw [add_tensor, neg_tensor]
|
||||
simp only [neg_add_cancel]
|
||||
|
||||
/-- A tensor tree plus its negation is zero. -/
|
||||
@[simp]
|
||||
lemma add_neg (t : TensorTree S c) : (add t (neg t)).tensor = 0 := by
|
||||
rw [add_tensor, neg_tensor]
|
||||
|
|
@ -117,6 +124,10 @@ lemma perm_eq_id {n : ℕ} {c : Fin n → S.C} (σ : (OverColor.mk c) ⟶ (OverC
|
|||
(h : σ = 𝟙 _) (t : TensorTree S c) : (perm σ t).tensor = t.tensor := by
|
||||
simp [perm_tensor, h]
|
||||
|
||||
/-- Given an equality of tensors corresponding to tensor trees where the tensor tree on the
|
||||
left finishes with a permution 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. -/
|
||||
lemma perm_eq_of_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(σ : (OverColor.mk c) ≅ (OverColor.mk c1))
|
||||
{t : TensorTree S c} {t2 : TensorTree S c1} (h : (perm σ.hom t).tensor = t2.tensor) :
|
||||
|
|
@ -125,6 +136,8 @@ lemma perm_eq_of_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
|||
change _ = (S.F.map σ.hom ≫ S.F.map σ.inv).hom _
|
||||
simp only [Iso.map_hom_inv_id, Action.id_hom, ModuleCat.id_apply]
|
||||
|
||||
/-- 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`. -/
|
||||
lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1))
|
||||
{t : TensorTree S c} {t2 : TensorTree S c1} :
|
||||
|
|
@ -162,15 +175,19 @@ These identities are related to the fact that all the maps are linear.
|
|||
|
||||
-/
|
||||
|
||||
/-- Two `smul` nodes can be replaced with a single `smul` node with
|
||||
the product of the two scalars. -/
|
||||
lemma smul_smul (t : TensorTree S c) (a b : S.k) :
|
||||
(smul a (smul b t)).tensor = (smul (a * b) t).tensor := by
|
||||
simp only [smul_tensor]
|
||||
exact _root_.smul_smul a b t.tensor
|
||||
|
||||
/-- An `smul`-node with scalar `1` does nothing. -/
|
||||
lemma smul_one (t : TensorTree S c) :
|
||||
(smul 1 t).tensor = t.tensor := by
|
||||
simp [smul_tensor]
|
||||
|
||||
/-- An `smul`-node with scalar equal to `1` does nothing. -/
|
||||
lemma smul_eq_one (t : TensorTree S c) (a : S.k) (h : a = 1) :
|
||||
(smul a t).tensor = t.tensor := by
|
||||
rw [h]
|
||||
|
|
@ -194,11 +211,14 @@ lemma add_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
|||
(add (perm σ t) (perm σ t1)).tensor = (perm σ (add t t1)).tensor := by
|
||||
simp only [add_tensor, perm_tensor, map_add]
|
||||
|
||||
/-- When a `perm` acts on an add node, it can be moved through the add-node
|
||||
to act on each of the two parts. -/
|
||||
lemma perm_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t t1 : TensorTree S c) :
|
||||
(perm σ (add t t1)).tensor = (add (perm σ t) (perm σ t1)).tensor := by
|
||||
simp only [add_tensor, perm_tensor, map_add]
|
||||
|
||||
/-- A `smul` node can be moved through an `perm` node. -/
|
||||
lemma perm_smul {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (a : S.k) (t : TensorTree S c) :
|
||||
(perm σ (smul a t)).tensor = (smul a (perm σ t)).tensor := by
|
||||
|
|
@ -210,16 +230,21 @@ lemma add_eval {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t
|
|||
(add (eval i e t) (eval i e t1)).tensor = (eval i e (add t t1)).tensor := by
|
||||
simp only [add_tensor, eval_tensor, Nat.succ_eq_add_one, map_add]
|
||||
|
||||
/-- When a `contr` acts on an add node, it can be moved through the add-node
|
||||
to act on each of the two parts. -/
|
||||
lemma contr_add {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 (add t1 t2)).tensor = (add (contr i j h t1) (contr i j h t2)).tensor := by
|
||||
simp [contr_tensor, add_tensor]
|
||||
|
||||
/-- A `smul` node can be moved through an `contr` node. -/
|
||||
lemma contr_smul {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 := by
|
||||
simp [contr_tensor, smul_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]
|
||||
lemma add_prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(t1 t2 : TensorTree S c) (t3 : TensorTree S c1) :
|
||||
|
|
@ -228,6 +253,8 @@ lemma add_prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
|||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, add_tensor, add_tmul, map_add]
|
||||
|
||||
/-- 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. -/
|
||||
@[simp]
|
||||
lemma prod_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(t1 : TensorTree S c) (t2 t3 : TensorTree S c1) :
|
||||
|
|
@ -236,16 +263,20 @@ lemma prod_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
|||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, add_tensor, tmul_add, map_add]
|
||||
|
||||
/-- A `smul` node in the LHS of a `prod` node can be moved through that `prod` node. -/
|
||||
lemma smul_prod {n m: ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) :
|
||||
((prod (smul a t1) t2)).tensor = (smul a (prod t1 t2)).tensor := by
|
||||
simp [prod_tensor, smul_tensor, tmul_smul, smul_tmul, map_smul]
|
||||
|
||||
/-- A `smul` node in the RHS of a `prod` node can be moved through that `prod` node. -/
|
||||
lemma prod_smul {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) :
|
||||
(prod t1 (smul a t2)).tensor = (smul a (prod t1 t2)).tensor := by
|
||||
simp [prod_tensor, smul_tensor, tmul_smul, smul_tmul, map_smul]
|
||||
|
||||
/-- When a `prod` node acts on an `add` node in both the LHS and RHS entries,
|
||||
it can be moved through both `add` nodes. -/
|
||||
lemma prod_add_both {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(t1 t2 : TensorTree S c) (t3 t4 : TensorTree S c1) :
|
||||
(prod (add t1 t2) (add t3 t4)).tensor = (add (add (prod t1 t3) (prod t1 t4))
|
||||
|
|
@ -260,11 +291,12 @@ lemma prod_add_both {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
|||
|
||||
-/
|
||||
|
||||
/-- The action of a group element can be brought though a scalar multiplication. -/
|
||||
/-- An `action` node can be moved through a `smul` node. -/
|
||||
lemma smul_action {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 := by
|
||||
simp only [smul_tensor, action_tensor, map_smul]
|
||||
|
||||
/-- An `action` node can be moved through a `contr` node. -/
|
||||
lemma contr_action {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 := by
|
||||
|
|
@ -273,6 +305,7 @@ lemma contr_action {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ}
|
|||
erw [(S.contrMap c i j h).comm g]
|
||||
rfl
|
||||
|
||||
/-- An `action` node can be moved through a `prod` node when acting on both elements. -/
|
||||
lemma prod_action {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S.G)
|
||||
(t : TensorTree S c) (t1 : TensorTree S c1) :
|
||||
(prod (action g t) (action g t1)).tensor = (action g (prod t t1)).tensor := by
|
||||
|
|
@ -290,10 +323,12 @@ lemma prod_action {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S.
|
|||
erw [← (S.F.μ (OverColor.mk c) (OverColor.mk c1)).comm g]
|
||||
rfl
|
||||
|
||||
/-- An `action` node can be moved through a `add` node when acting on both elements. -/
|
||||
lemma add_action {n : ℕ} {c : Fin n → S.C} (g : S.G) (t t1 : TensorTree S c) :
|
||||
(add (action g t) (action g t1)).tensor = (action g (add t t1)).tensor := by
|
||||
simp only [add_tensor, action_tensor, map_add]
|
||||
|
||||
/-- An `action` node can be moved through a `perm` node. -/
|
||||
lemma perm_action {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (g : S.G) (t : TensorTree S c) :
|
||||
(perm σ (action g t)).tensor = (action g (perm σ t)).tensor := by
|
||||
|
|
@ -302,18 +337,22 @@ lemma perm_action {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
|||
erw [(S.F.map σ).comm g]
|
||||
rfl
|
||||
|
||||
/-- An `action` node can be moved through a `neg` node. -/
|
||||
lemma neg_action {n : ℕ} {c : Fin n → S.C} (g : S.G) (t : TensorTree S c) :
|
||||
(neg (action g t)).tensor = (action g (neg t)).tensor := by
|
||||
simp only [neg_tensor, action_tensor, map_neg]
|
||||
|
||||
/-- Two `action` nodes can be combined into a single `action` node. -/
|
||||
lemma action_action {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 := by
|
||||
simp only [action_tensor, map_mul, LinearMap.mul_apply]
|
||||
|
||||
/-- The `action` node for the identity leaves the tensor invariant. -/
|
||||
lemma action_id {n : ℕ} {c : Fin n → S.C} (t : TensorTree S c) :
|
||||
(action 1 t).tensor = t.tensor := by
|
||||
simp only [action_tensor, map_one, LinearMap.one_apply]
|
||||
|
||||
/-- An `action` node on a `constTwoNode` leaves the tensor invariant. -/
|
||||
lemma action_constTwoNode {c1 c2 : S.C}
|
||||
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FD.obj (Discrete.mk c1) ⊗ S.FD.obj (Discrete.mk c2))
|
||||
(g : S.G) : (action g (constTwoNode v)).tensor = (constTwoNode v).tensor := by
|
||||
|
|
@ -327,6 +366,7 @@ lemma action_constTwoNode {c1 c2 : S.C}
|
|||
erw [← v.comm g]
|
||||
simp
|
||||
|
||||
/-- An `action` node on a `constThreeNode` leaves the tensor invariant. -/
|
||||
lemma action_constThreeNode {c1 c2 c3 : S.C}
|
||||
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FD.obj (Discrete.mk c1) ⊗ S.FD.obj (Discrete.mk c2) ⊗
|
||||
S.FD.obj (Discrete.mk c3))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue