The one-strand transport collapse

The transport at one strand is the left-unitor composite of the strand identification: the counit-tensor coherence with the strict skein unitor eliminated. Its even and odd evaluations on unit-padded vectors are the strand identification itself.

theorem RS.stdToOmega_one {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) : stdToOmega f P e 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft SuperVect.tensorUnit e) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (P.ω.obj { arity := 1 })).hom

The one-strand transport is the unitor composite.

theorem RS.stdToOmega_one_even {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (x : (stdSuperPair k ℓ).even) : (stdToOmega f P e 1).evenMap (evenPair 1 x) = e.evenMap x

The even evaluation of the one-strand transport on a unit-padded even vector.

def RS.oddUnitPad {V : SuperVect} (y : V.odd) : (SuperVect.tensorUnit.tensorObj V).odd

The unit-padded odd element.

Equations

• RS.oddUnitPad y = (1 ⊗ₜ[ℂ] y, 0)

theorem RS.stdToOmega_one_odd {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (y : (stdSuperPair k ℓ).odd) : (stdToOmega f P e 1).oddMap (oddUnitPad y) = e.oddMap y

The odd evaluation of the one-strand transport on a unit-padded odd vector.