The evaluation functional on odd pairs

The odd counterpart of the standard-form identification: on transported odd pairs the one-strand evaluation through the structure map is the standard form's odd block — the symplectic entries.

theorem RS.evFormOdd {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 ℓ).odd) : (omegaFun f P (ε_ { arity := 1 } { arity := 1 })) ((CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := 1 } { arity := 1 }).evenMap (oddPair (e.oddMap x) (e.oddMap y))) = (stdForm k ℓ).evenMap (oddPair x y)

The evaluation is the standard form on transported odd pairs.