The peel step in model form

The cap value successor law transported to the model: the peel rotation splits as a same-arity permutation followed by an arity cast (CapPerm), and the cap value at m + 1 is the split cap value of the permuted-and-cast vector. The colour action of the permutation is the only remaining ingredient of the closed form.

theorem RS.capPeelArity (m : ℕ) : m + 1 + (m + 1) = m + m + 2

The peel arity identity, pinned.

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

The split cap value: the smaller cap tensored with one evaluation, on a transported vector.

Equations

• RS.splitCapVal f P e m w = (RS.omegaFun f P (((RS.HomSpace.tensor f (m + m) 0 2 0) (RS.bundleCapClass f m)) (RS.evClass f))) ((RS.stdToOmega f P e (m + m + 2)).evenMap w)

theorem RS.splitCapVal_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 + 2)).even) : splitCapVal f P e m (∑ i ∈ s, g i) = ∑ i ∈ s, splitCapVal f P e m (g i)

The split cap value is additive over finite sums.

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

The split cap value is homogeneous.

theorem RS.splitCapVal_expansion {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) (w : (superPow (stdSuperPair k ℓ) (m + m + 2)).even) : splitCapVal f P e m w = ∑ c : { c : MixedColouring k ℓ (m + m + 2) // c.IsEven }, coordOf w ↑c * splitCapVal f P e m (evenBasisVec c)

The split cap value in coordinates.

theorem RS.splitCapVal_merge {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) (x : (superPow (stdSuperPair k ℓ) (m + m)).even) (y : (superPow (stdSuperPair k ℓ) 2).even) : splitCapVal f P e m ((powMerge (stdSuperPair k ℓ) (m + m) 2).evenMap (evenPair x y)) = capVal f P e m x * (omegaFun f P (evClass f)) ((stdToOmega f P e 2).evenMap y)

The split cap value on merges: CapSplit restated.

theorem RS.splitCapVal_oddMerge {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) (x : (superPow (stdSuperPair k ℓ) (m + m)).odd) (y : (superPow (stdSuperPair k ℓ) 2).odd) : splitCapVal f P e m ((powMerge (stdSuperPair k ℓ) (m + m) 2).evenMap (0, x ⊗ₜ[ℂ] y)) = 0

The split cap value vanishes on odd merges.

theorem RS.capVal_succ {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) (v : (superPow (stdSuperPair k ℓ) (m + 1 + (m + 1))).even) : capVal f P e (m + 1) v = splitCapVal f P e m ((CategoryTheory.CategoryStruct.comp (modelPermMap (capPeelPerm m)) (CategoryTheory.eqToHom ⋯)).evenMap v)

The cap value successor law in model form.