feat: Add prod_assoc lemma
This commit is contained in:
jstoobysmith
parent
30df80aa4e
commit
ebf5fe5d0f
2 changed files with 74 additions and 10 deletions
|
|
@ -122,4 +122,5 @@ import HepLean.Tensors.Tree.NodeIdentities.ContrContr
|
|||
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermProd
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
|
||||
|
|
|
|||
|
|
@ -22,23 +22,86 @@ namespace TensorTree
|
|||
variable {S : TensorSpecies} {n n2 n3 : ℕ}
|
||||
(c : Fin n → S.C) (c2 : Fin n2 → S.C) (c3 : Fin n3 → S.C )
|
||||
|
||||
|
||||
/-- The permutation that arises from assocativity of `prod` node.
|
||||
This permutation is defined using braiding and composition with `finSumFinEquiv`
|
||||
based-isomorphisms. -/
|
||||
def assocPerm : OverColor.mk (Sum.elim c (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm) ∘ ⇑finSumFinEquiv.symm) ≅
|
||||
OverColor.mk (Sum.elim (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm) c3 ∘ ⇑finSumFinEquiv.symm) :=
|
||||
def assocPerm : OverColor.mk (Sum.elim (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm) c3 ∘ ⇑finSumFinEquiv.symm) ≅
|
||||
OverColor.mk (Sum.elim c (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm) ∘ ⇑finSumFinEquiv.symm) :=
|
||||
(equivToIso finSumFinEquiv).symm.trans <|
|
||||
(whiskerLeftIso (OverColor.mk c) (equivToIso finSumFinEquiv).symm).trans <|
|
||||
(α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).symm.trans <|
|
||||
(whiskerRightIso (equivToIso finSumFinEquiv) (OverColor.mk c3)).trans <|
|
||||
(whiskerRightIso (equivToIso finSumFinEquiv).symm (OverColor.mk c3)).trans <|
|
||||
(α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).trans <|
|
||||
(whiskerLeftIso (OverColor.mk c) (equivToIso finSumFinEquiv)).trans <|
|
||||
(equivToIso finSumFinEquiv)
|
||||
|
||||
lemma finSumFinEquiv_comp_assocPerm :
|
||||
(equivToIso finSumFinEquiv).hom ≫ (assocPerm c c2 c3).hom =
|
||||
(whiskerRightIso (equivToIso finSumFinEquiv).symm (OverColor.mk c3)).hom ≫
|
||||
(α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom ≫
|
||||
(whiskerLeftIso (OverColor.mk c) (equivToIso finSumFinEquiv)).hom
|
||||
≫ (equivToIso finSumFinEquiv).hom := by
|
||||
rw [assocPerm]
|
||||
simp
|
||||
|
||||
/-- The arguments of a `prod` node can be commuted using braiding. -/
|
||||
/-- The `prod` obeys associativity. -/
|
||||
theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree S c3) :
|
||||
(prod (prod t t2) t3).tensor = (perm (assocPerm c c2 c3).hom (prod t (prod t2 t3))).tensor := by
|
||||
sorry
|
||||
|
||||
(prod t (prod t2 t3)).tensor = (perm (assocPerm c c2 c3).hom (prod (prod t t2) t3)).tensor := by
|
||||
rw [perm_tensor]
|
||||
nth_rewrite 2 [prod_tensor]
|
||||
change _ = ((S.F.map (equivToIso finSumFinEquiv).hom) ≫ S.F.map (assocPerm c c2 c3).hom).hom
|
||||
(((S.F.μ (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)).hom
|
||||
((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor)))
|
||||
rw [← S.F.map_comp, finSumFinEquiv_comp_assocPerm]
|
||||
simp only [Functor.id_obj, mk_hom, whiskerRightIso_hom, Iso.symm_hom, whiskerLeftIso_hom,
|
||||
Functor.map_comp, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply]
|
||||
rw [prod_tensor]
|
||||
apply congrArg
|
||||
change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom
|
||||
((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom
|
||||
((S.F.μ (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)
|
||||
≫ S.F.map ((equivToIso finSumFinEquiv).inv ▷ OverColor.mk c3)).hom
|
||||
(((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor))))
|
||||
rw [← S.F.μ_natural_left]
|
||||
simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Action.comp_hom,
|
||||
Action.instMonoidalCategory_whiskerRight_hom, ModuleCat.coe_comp, Function.comp_apply,
|
||||
ModuleCat.MonoidalCategory.whiskerRight_apply]
|
||||
nth_rewrite 2 [prod_tensor]
|
||||
simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj]
|
||||
change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom
|
||||
((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom
|
||||
((S.F.μ (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3)).hom
|
||||
((S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (equivToIso finSumFinEquiv).inv).hom
|
||||
(((S.F.μ (OverColor.mk c) (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k]
|
||||
t3.tensor)))
|
||||
simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Iso.map_hom_inv_id, Action.id_hom,
|
||||
ModuleCat.id_apply]
|
||||
change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom
|
||||
(((S.F.μ (OverColor.mk c) (OverColor.mk c2) ▷ S.F.obj (OverColor.mk c3)) ≫
|
||||
S.F.μ (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3) ≫
|
||||
S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom
|
||||
(((t.tensor ⊗ₜ[S.k] t2.tensor) ⊗ₜ[S.k] t3.tensor)))
|
||||
erw [S.F.associativity]
|
||||
simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
|
||||
Action.instMonoidalCategory_associator_hom_hom, Action.instMonoidalCategory_whiskerLeft_hom,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply,
|
||||
ModuleCat.MonoidalCategory.associator_hom_apply]
|
||||
rw [prod_tensor]
|
||||
change ((_ ◁ (S.F.map (equivToIso finSumFinEquiv).hom) ) ≫
|
||||
S.F.μ (OverColor.mk c) (OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom
|
||||
(t.tensor ⊗ₜ[S.k]
|
||||
((S.F.μ (OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _
|
||||
rw [S.F.μ_natural_right]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
ModuleCat.coe_comp, Function.comp_apply]
|
||||
rfl
|
||||
|
||||
end TensorTree
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue