The evaluation functional in standard coordinates

Under a standard-model identification, the one-strand evaluation functional composed with the structure map is the standard form: the pointwise consequence of the model transport equation.

theorem RS.evForm {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : (stdSuperPair k ℓ).Hom (P.ω.obj { arity := 1 })) (hform : SuperVect.Hom.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := 1 } { arity := 1 }) (CategoryTheory.CategoryStruct.comp (P.ω.map (ε_ { arity := 1 } { arity := 1 })) (CategoryTheory.Functor.OplaxMonoidal.η P.ω))) (SuperVect.tensorHom e e) = stdForm k ℓ) (x y : (stdSuperPair k ℓ).even) : (omegaFun f P (ε_ { arity := 1 } { arity := 1 })) ((CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := 1 } { arity := 1 }).evenMap (evenPair (e.evenMap x) (e.evenMap y))) = (stdForm k ℓ).evenMap (evenPair x y)

The evaluation is the standard form on transported even pairs.