The cap functional recursion

The base and successor laws of the cap functional through the fibre functor: the zero cap is the identity class, and the successor cap evaluates through the peel rotation and the tensor split.

theorem RS.bundleCapClass_zero {R : ℕ} (f : EdgeRankParameter R) : bundleCapClass f 0 = CategoryTheory.CategoryStruct.id { arity := 0 }

The zero cap is the identity class.

theorem RS.omegaFun_cap_succ {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (m : ℕ) (v : (P.ω.obj { arity := m + 1 + (m + 1) }).even) : (omegaFun f P (bundleCapClass f (m + 1))) v = (omegaFun f P (((HomSpace.tensor f (m + m) 0 2 0) (bundleCapClass f m)) (evClass f))) ((P.ω.map (bundleMapClass f (capPeelRotation m))).evenMap v)

The cap functional successor law: evaluate through the peel rotation, then the split cap.

theorem RS.omegaFun_cap_zero {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (v : (P.ω.obj { arity := 0 }).even) : (omegaFun f P (bundleCapClass f 0)) v = (CategoryTheory.Functor.OplaxMonoidal.η P.ω).evenMap v

The zero cap functional is the unit evaluation.