The assembled star vector in the model

The star vectors pull back along the model transport and assemble by the block merge entirely inside the monoidal powers of the standard space; transporting forward recovers the fibre-side assembled vector. This is the form on which the colouring coordinates evaluate.

noncomputable def RS.modelStarVec {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (ds : List ℕ) : (superPow (stdSuperPair k ℓ) ds.sum).even

The assembled star vector, in the model.

Equations

• One or more equations did not get rendered due to their size.
• RS.modelStarVec f P e' [] = 1

theorem RS.stdToOmega_modelStarVec {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (hee' : CategoryTheory.CategoryStruct.comp e' e = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 1 })) (ds : List ℕ) : (stdToOmega f P e ds.sum).evenMap (modelStarVec f P e' ds) = omegaStarVec f P ds

The model star vector transports to the assembled star vector.