The cap closed form #
The peel induction: the cap value on colour basis vectors is the diagonal cap pairing.
theorem
RS.capVal_closed
{R : ℕ}
(f : EdgeRankParameter R)
(P : DelignePackage (SkeinObj f))
{k ℓ : ℕ}
(e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 })
(hform :
SuperVect.Hom.comp
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := 1 } { arity := 1 })
(CategoryTheory.CategoryStruct.comp (P.ω.map (ε_ { arity := 1 } { arity := 1 }))
(CategoryTheory.Functor.OplaxMonoidal.η P.ω)))
(SuperVect.tensorHom e e) = stdForm k ℓ)
(m : ℕ)
(c : MixedColouring k ℓ (m + m))
(hc : c.IsEven)
:
The cap closed form.