Image functionals of tensors

The dual of the point-tensor coherence: the fibre functor sends tensor products of copoint morphisms to the product of their image functionals through the structure map. Abstract coherence first — every rewrite fires over generic instances — then the strict skein unit and the concrete SuperVect unitor.

theorem RS.point_cotensor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Monoidal] {A B : C} (q₁ : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (q₂ : B ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A B) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom q₁ q₂) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom)) (CategoryTheory.Functor.OplaxMonoidal.η F)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (F.map q₁) (CategoryTheory.Functor.OplaxMonoidal.η F)) (CategoryTheory.CategoryStruct.comp (F.map q₂) (CategoryTheory.Functor.OplaxMonoidal.η F))) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom

Copoints are monoidal: for a monoidal functor, the structure map followed by the image of a corrected tensor of copoints and the unit map is the tensor of the copoint images followed by the target unitor.

theorem RS.lambda_evenPair {V W : SuperVect} (g : V ⟶ SuperVect.tensorUnit) (h : W ⟶ SuperVect.tensorUnit) (v : V.even) (w : W.even) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect)).hom).evenMap (evenPair v w) = g.evenMap v * h.evenMap w

The tensor of functionals on an even pair evaluates to the product.

theorem RS.omegaFun_tensor {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {a b : ℕ} (q₁ : { arity := a } ⟶ { arity := 0 }) (q₂ : { arity := b } ⟶ { arity := 0 }) (v : (P.ω.obj { arity := a }).even) (w : (P.ω.obj { arity := b }).even) : (omegaFun f P (CategoryTheory.MonoidalCategoryStruct.tensorHom q₁ q₂)) ((CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := a } { arity := b }).evenMap (evenPair v w)) = (omegaFun f P q₁) v * (omegaFun f P q₂) w

Image functionals are monoidal: the image functional of a tensor of copoint morphisms, evaluated on a structure-map image of an even pair, is the product of the image functionals.

theorem RS.omegaFun_comp {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {a b : ℕ} (p : { arity := a } ⟶ { arity := b }) (q : { arity := b } ⟶ { arity := 0 }) (v : (P.ω.obj { arity := a }).even) : (omegaFun f P (CategoryTheory.CategoryStruct.comp p q)) v = (omegaFun f P q) ((P.ω.map p).evenMap v)

The image functional of a composite: precompose with the image of the first factor.