The parameter value over the model

Threading the transports through the factored parameter value: the argument of the cap functional becomes a model-side vector — the assembled star vector acted on by the sort's model permutation word and the degree-sum cast — pushed forward once.

noncomputable def RS.modelPermMap {k ℓ n : ℕ} (σ : Equiv.Perm (Fin n)) : superPow (stdSuperPair k ℓ) n ⟶ superPow (stdSuperPair k ℓ) n

The model action of a permutation: trivial at arity zero, the braiding word of the adjacent-transposition word above.

Equations

• RS.modelPermMap x_2 = CategoryTheory.CategoryStruct.id (RS.superPow (RS.stdSuperPair k ℓ) 0)
• RS.modelPermMap σ = RS.powBraidWord (RS.stdSuperPair k ℓ) (RS.adjWord σ)

theorem RS.stdToOmega_bmc_perm_all {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (n : ℕ) (σ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (stdToOmega f P e n) (P.ω.map (bundleMapClass f σ)) = CategoryTheory.CategoryStruct.comp (modelPermMap σ) (stdToOmega f P e n)

The permutation intertwining at every arity.

theorem RS.parameter_model {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (hee' : CategoryTheory.CategoryStruct.comp e' e = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 1 })) : f.val W = circleVal f ^ W.circles * (omegaFun f P (bundleCapClass f (edgeCount W))) ((stdToOmega f P e (edgeCount W + edgeCount W)).evenMap ((CategoryTheory.eqToHom ⋯).evenMap ((modelPermMap (sortSplitPerm W)).evenMap (modelStarVec f P e' (degList (starAssignEnum W))))))

The parameter value over the model: the cap functional evaluated on the transported model vector — the assembled star vector, permuted by the sort word and recast along the degree sum.