Image vectors of tensors

The fibre functor sends tensor products of point morphisms to the structure-map image of the tensor of their image vectors. The coherence is proved abstractly for any monoidal functor — where every rewrite fires — and the strictness of the skein unit is exploited only in two small concrete bridging steps.

def RS.evenPair {V W : SuperVect} (v : V.even) (w : W.even) : (V.tensorObj W).even

The even component of a tensor of even vectors.

Equations

• RS.evenPair v w = (v ⊗ₜ[ℂ] w, 0)

theorem RS.point_tensor {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} (p : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A) (q : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom p q))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map p)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map q))) (CategoryTheory.Functor.LaxMonoidal.μ F A B))

Points are monoidal: for a monoidal functor, the counit composed with the image of a corrected tensor of points is the tensor of the point images assembled by the structure map.

theorem RS.skein_leftUnitor_unit_inv {R : ℕ} (f : EdgeRankParameter R) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SkeinObj f))).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SkeinObj f))

The inverse left unitor of the skein category at the unit is the identity.

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

The image vector of a composite: apply the image of the second factor.

theorem RS.omegaVec_smul {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {a : ℕ} (r : ℂ) (p : { arity := 0 } ⟶ { arity := a }) : omegaVec f P (r • p) = r • omegaVec f P p

The image vector is homogeneous in the morphism.

theorem RS.tensorHom_evenPair {V₁ V₂ W₁ W₂ : SuperVect} (g : V₁ ⟶ V₂) (h : W₁ ⟶ W₂) (v : V₁.even) (w : W₁.even) : (CategoryTheory.MonoidalCategoryStruct.tensorHom g h).evenMap (evenPair v w) = evenPair (g.evenMap v) (h.evenMap w)

The tensor of morphisms on an even pair acts componentwise.

theorem RS.superVect_leftUnitor_inv_one : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect)).inv.evenMap 1 = evenPair 1 1

The inverse left unitor of SuperVect at the unit sends 1 to the even pair of units.

theorem RS.omegaVec_tensor {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {a b : ℕ} (p : { arity := 0 } ⟶ { arity := a }) (q : { arity := 0 } ⟶ { arity := b }) : have x := P.braided; omegaVec f P (((HomSpace.tensor f 0 a 0 b) p) q) = (CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := a } { arity := b }).evenMap (evenPair (omegaVec f P p) (omegaVec f P q))

Image vectors are monoidal: the image vector of a tensor of point morphisms is the structure-map image of the even pair of the image vectors.