Products and contractions

Left contractions.

def TensorTree.ContrPair.leftContrEquivSuccSucc {n n1 : ℕ} : Fin (n.succ.succ + n1) ≃ Fin (n + n1).succ.succ

An equivalence needed to perform contraction. For specified n and n1 this reduces to an identity.

Equations

• TensorTree.ContrPair.leftContrEquivSuccSucc = (Fin.castOrderIso ⋯).toEquiv

def TensorTree.ContrPair.leftContrEquivSucc {n n1 : ℕ} : Fin (n.succ + n1) ≃ Fin (n + n1).succ

An equivalence needed to perform contraction. For specified n and n1 this reduces to an identity.

Equations

• TensorTree.ContrPair.leftContrEquivSucc = (Fin.castOrderIso ⋯).toEquiv

def TensorTree.ContrPair.leftContrI {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (n1 : ℕ) : Fin (n + n1).succ.succ

The new fst index of a contraction obtained on moving a contraction in the LHS of a product through the product.

Equations

• q.leftContrI n1 = TensorTree.ContrPair.leftContrEquivSuccSucc (Fin.castAdd n1 q.i)

def TensorTree.ContrPair.leftContrJ {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (n1 : ℕ) : Fin (n + n1).succ

The new snd index of a contraction obtained on moving a contraction in the LHS of a product through the product.

Equations

• q.leftContrJ n1 = TensorTree.ContrPair.leftContrEquivSucc (Fin.castAdd n1 q.j)

@[simp]

theorem TensorTree.ContrPair.leftContrJ_succAbove_leftContrI {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : (q.leftContrI n1).succAbove (q.leftContrJ n1) = leftContrEquivSuccSucc (Fin.castAdd n1 (q.i.succAbove q.j))

theorem TensorTree.ContrPair.succAbove_leftContrJ_leftContrI_castAdd {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (x : Fin n) : (q.leftContrI n1).succAbove ((q.leftContrJ n1).succAbove (Fin.castAdd n1 x)) = leftContrEquivSuccSucc (Fin.castAdd n1 (q.i.succAbove (q.j.succAbove x)))

theorem TensorTree.ContrPair.succAbove_leftContrJ_leftContrI_natAdd {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (x : Fin n1) : (q.leftContrI n1).succAbove ((q.leftContrJ n1).succAbove (Fin.natAdd n x)) = leftContrEquivSuccSucc (Fin.natAdd n.succ.succ x)

def TensorTree.ContrPair.leftContr {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) : ContrPair ((Sum.elim c c1 ∘ finSumFinEquiv.symm.toFun) ∘ ⇑leftContrEquivSuccSucc.symm)

The pair of contraction indices obtained on moving a contraction in the LHS of a product through the product.

Equations

• q.leftContr = { i := q.leftContrI n1, j := q.leftContrJ n1, h := ⋯ }

theorem TensorTree.ContrPair.leftContr_map_eq {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) : ((Sum.elim c (IndexNotation.OverColor.mk c1).hom ∘ finSumFinEquiv.symm.toFun) ∘ ⇑leftContrEquivSuccSucc.symm) ∘ q.leftContr.i.succAbove ∘ q.leftContr.j.succAbove = Sum.elim (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)).hom (IndexNotation.OverColor.mk c1).hom ∘ ⇑finSumFinEquiv.symm

theorem TensorTree.ContrPair.sum_inl_succAbove_leftContrI_leftContrJ {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (k : Fin n) : finSumFinEquiv.symm (leftContrEquivSuccSucc.symm (q.leftContr.i.succAbove (q.leftContr.j.succAbove (finSumFinEquiv (Sum.inl k))))) = Sum.map (q.i.succAbove ∘ q.j.succAbove) id (Sum.inl k)

theorem TensorTree.ContrPair.sum_inr_succAbove_leftContrI_leftContrJ {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (k : Fin n1) : finSumFinEquiv.symm (leftContrEquivSuccSucc.symm (q.leftContr.i.succAbove (q.leftContr.j.succAbove (finSumFinEquiv (Sum.inr k))))) = Sum.map (q.i.succAbove ∘ q.j.succAbove) id (Sum.inr k)

theorem TensorTree.ContrPair.contrMap_prod_tprod_aux {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (l : (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)).left ⊕ (IndexNotation.OverColor.mk c1).left) (l' : Fin n.succ.succ ⊕ Fin n1) (h : Sum.elim c c1 l' = Sum.elim (c ∘ q.i.succAbove ∘ q.j.succAbove) c1 l) (h' : l' = Sum.map (q.i.succAbove ∘ q.j.succAbove) id l) (p : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c).left) → CoeSort.coe (S.FD.obj { as := (IndexNotation.OverColor.mk c).hom i })) (q' : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c1).left) → CoeSort.coe (S.FD.obj { as := (IndexNotation.OverColor.mk c1).hom i })) : (IndexNotation.OverColor.lift.discreteSumEquiv' S.FD l) (PhysLean.PiTensorProduct.elimPureTensor (fun (k : Fin n) => p (q.i.succAbove (q.j.succAbove k))) q' l) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯)).hom) ((IndexNotation.OverColor.lift.discreteSumEquiv' S.FD l') (PhysLean.PiTensorProduct.elimPureTensor p q' l'))

theorem TensorTree.ContrPair.contrMap_prod_tprod_aux_2 {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {g✝ : Fin n1 → S.C} {q' : (i : Fin n1) → ↑(S.FD.obj { as := g✝ i }).V} (p : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c).left) → CoeSort.coe (S.FD.obj { as := (IndexNotation.OverColor.mk c).hom i })) (a : Fin n.succ.succ) (b : Fin (n + 1 + 1) ⊕ Fin n1) (h : b = Sum.inl a) : p a = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.Discrete.eqToHom ⋯)).hom) ((IndexNotation.OverColor.lift.discreteSumEquiv' S.FD b) (PhysLean.PiTensorProduct.elimPureTensor p q' b))

theorem TensorTree.ContrPair.contrMap_prod_tprod {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (p : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c).left) → CoeSort.coe (S.FD.obj { as := (IndexNotation.OverColor.mk c).hom i })) (q' : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c1).left) → CoeSort.coe (S.FD.obj { as := (IndexNotation.OverColor.mk c1).hom i })) : (CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (IndexNotation.OverColor.mk c1)).hom) ((CategoryTheory.ConcreteCategory.hom q.contrMap.hom) ((PiTensorProduct.tprod S.k) p) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q')) = (CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) ((CategoryTheory.ConcreteCategory.hom q.leftContr.contrMap.hom) ((CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.equivToIso leftContrEquivSuccSucc).hom).hom) ((CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk c) (IndexNotation.OverColor.mk c1)).hom) ((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q')))))

theorem TensorTree.ContrPair.contrMap_prod {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight q.contrMap (S.F.obj (IndexNotation.OverColor.mk c1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (IndexNotation.OverColor.mk c1)) (S.F.map (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk c) (IndexNotation.OverColor.mk c1)) (CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom) (CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.equivToIso leftContrEquivSuccSucc).hom) (CategoryTheory.CategoryStruct.comp q.leftContr.contrMap (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom))))

theorem TensorTree.ContrPair.contr_prod {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (t : TensorTree S c) (t1 : TensorTree S c1) : ((contr q.i q.j ⋯ t).prod t1).tensor = (perm (IndexNotation.OverColor.mkIso ⋯).hom (contr (q.leftContrI n1) (q.leftContrJ n1) ⋯ (perm (IndexNotation.OverColor.equivToIso leftContrEquivSuccSucc).hom (t.prod t1)))).tensor

Right contractions.

def TensorTree.ContrPair.rightContrI {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (n1 : ℕ) : Fin (n1 + n).succ.succ

The new fst index of a contraction obtained on moving a contraction in the RHS of a product through the product.

Equations

• q.rightContrI n1 = Fin.natAdd n1 q.i

def TensorTree.ContrPair.rightContrJ {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (n1 : ℕ) : Fin (n1 + n).succ

The new snd index of a contraction obtained on moving a contraction in the RHS of a product through the product.

Equations

• q.rightContrJ n1 = Fin.natAdd n1 q.j

@[simp]

theorem TensorTree.ContrPair.rightContrJ_succAbove_rightContrI {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) : (q.rightContrI n1).succAbove (q.rightContrJ n1) = Fin.natAdd n1 (q.i.succAbove q.j)

theorem TensorTree.ContrPair.succAbove_rightContrJ_rightContrI_castAdd {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (x : Fin n1) : (q.rightContrI n1).succAbove ((q.rightContrJ n1).succAbove (Fin.castAdd n x)) = Fin.castAdd n.succ.succ x

theorem TensorTree.ContrPair.succAbove_rightContrJ_rightContrI_natAdd {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} (q : ContrPair c) (x : Fin n) : (q.rightContrI n1).succAbove ((q.rightContrJ n1).succAbove (Fin.natAdd n1 x)) = Fin.natAdd n1 (q.i.succAbove (q.j.succAbove x))

def TensorTree.ContrPair.rightContr {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) : ContrPair (Sum.elim c1 c ∘ finSumFinEquiv.symm.toFun)

The new pair of indices obtained on moving a contraction in the RHS of a product through the product.

Equations

• q.rightContr = { i := q.rightContrI n1, j := q.rightContrJ n1, h := ⋯ }

theorem TensorTree.ContrPair.rightContr_map_eq {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) : (Sum.elim c1 (IndexNotation.OverColor.mk c).hom ∘ finSumFinEquiv.symm.toFun) ∘ q.rightContr.i.succAbove ∘ q.rightContr.j.succAbove = Sum.elim (IndexNotation.OverColor.mk c1).hom (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)).hom ∘ ⇑finSumFinEquiv.symm

theorem TensorTree.ContrPair.sum_inl_succAbove_rightContrI_rightContrJ {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (k : Fin n1) : finSumFinEquiv.symm (q.rightContr.i.succAbove (q.rightContr.j.succAbove (finSumFinEquiv (Sum.inl k)))) = Sum.map id (q.i.succAbove ∘ q.j.succAbove) (finSumFinEquiv.symm (finSumFinEquiv (Sum.inl k)))

theorem TensorTree.ContrPair.sum_inr_succAbove_rightContrI_rightContrJ {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (k : Fin n) : finSumFinEquiv.symm (q.rightContr.i.succAbove (q.rightContr.j.succAbove (finSumFinEquiv (Sum.inr k)))) = Sum.map id (q.i.succAbove ∘ q.j.succAbove) (finSumFinEquiv.symm (finSumFinEquiv (Sum.inr k)))

theorem TensorTree.ContrPair.prod_contrMap_tprod {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (p : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c1).left) → CoeSort.coe (S.FD.obj { as := (IndexNotation.OverColor.mk c1).hom i })) (q' : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c).left) → CoeSort.coe (S.FD.obj { as := (IndexNotation.OverColor.mk c).hom i })) : (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 (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom) ((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (CategoryTheory.ConcreteCategory.hom q.contrMap.hom) ((PiTensorProduct.tprod S.k) q'))) = (CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) ((CategoryTheory.ConcreteCategory.hom q.rightContr.contrMap.hom) ((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 c)).hom) ((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q'))))

theorem TensorTree.ContrPair.prod_contrMap {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.F.obj (IndexNotation.OverColor.mk c1)) q.contrMap) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk c1) (IndexNotation.OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))) (S.F.map (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk c1) (IndexNotation.OverColor.mk c)) (CategoryTheory.CategoryStruct.comp (S.F.map (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom) (CategoryTheory.CategoryStruct.comp q.rightContr.contrMap (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom)))

theorem TensorTree.ContrPair.prod_contr {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} (q : ContrPair c) (t1 : TensorTree S c1) (t : TensorTree S c) : (t1.prod (contr q.i q.j ⋯ t)).tensor = (perm (IndexNotation.OverColor.mkIso ⋯).hom (contr (q.rightContrI n1) (q.rightContrJ n1) ⋯ (t1.prod t))).tensor

theorem TensorTree.contr_prod {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (hij : c (i.succAbove j) = S.τ (c i)) (t : TensorTree S c) (t1 : TensorTree S c1) : ((contr i j hij t).prod t1).tensor = (perm (IndexNotation.OverColor.mkIso ⋯).hom (contr ({ i := i, j := j, h := hij }.leftContrI n1) ({ i := i, j := j, h := hij }.leftContrJ n1) ⋯ (perm (IndexNotation.OverColor.equivToIso ContrPair.leftContrEquivSuccSucc).hom (t.prod t1)))).tensor

Contraction in the LHS of a product can be moved out of that product.

theorem TensorTree.prod_contr {S : TensorSpecies} {n n1 : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n1 → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (hij : c (i.succAbove j) = S.τ (c i)) (t1 : TensorTree S c1) (t : TensorTree S c) : (t1.prod (contr i j hij t)).tensor = (perm (IndexNotation.OverColor.mkIso ⋯).hom (contr ({ i := i, j := j, h := hij }.rightContrI n1) ({ i := i, j := j, h := hij }.rightContrJ n1) ⋯ (t1.prod t))).tensor

Contraction in the RHS of a product can be moved out of that product.