The cap value on model vectors

The cap functional pulled back to the model: the scalar the final computation evaluates. Its base case: the zero cap reads off the scalar itself.

noncomputable def RS.capVal {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) (v : (superPow (stdSuperPair k ℓ) (m + m)).even) : ℂ

The cap value: the cap functional on the transported model vector.

Equations

• RS.capVal f P e m v = (RS.omegaFun f P (RS.bundleCapClass f m)) ((RS.stdToOmega f P e (m + m)).evenMap v)

theorem RS.capVal_zero {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (v : (superPow (stdSuperPair k ℓ) 0).even) : capVal f P e 0 v = v

The zero cap value is the scalar itself.

theorem RS.capVal_sum {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) {ι : Type u_1} (m : ℕ) (s : Finset ι) (g : ι → (superPow (stdSuperPair k ℓ) (m + m)).even) : capVal f P e m (∑ i ∈ s, g i) = ∑ i ∈ s, capVal f P e m (g i)

The cap value is additive over finite sums.

theorem RS.capVal_smul {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) (r : ℂ) (v : (superPow (stdSuperPair k ℓ) (m + m)).even) : capVal f P e m (r • v) = r * capVal f P e m v

The cap value is homogeneous.

theorem RS.parameter_capVal {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 * capVal f P e (edgeCount W) ((CategoryTheory.eqToHom ⋯).evenMap ((modelPermMap (sortSplitPerm W)).evenMap (modelStarVec f P e' (degList (starAssignEnum W)))))

The parameter value through the cap value: the final scalar shape.