Documentation

LeanPool.RegtsSevenster.RS.Novel.Coordinates.CapClosed

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) :
capVal f P e m (evenBasisVec ⟨c, hc⟩) = betaDiag m c

The cap closed form.