The circle value in the model

The composite of the coevaluation and evaluation classes is the free circle: gluing the two strand ends creates exactly one free circle, so the categorical scalar of η_ ≫ ε_ is the circle value of the parameter. Transporting through the fibre functor and the standard model identifies it with the superdimension k − 2ℓ.

theorem RS.circleCompose_flag_empty : IsEmpty (coevFrag.compose evFrag).Flag

The circle composite has no flags: both strand ends are glued.

noncomputable def RS.circleComposeEquiv : (coevFrag.compose evFrag).Equiv (circlesClosed 1)

The strand closure is the free circle.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.coev_comp_ev {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.CategoryStruct.comp (η_ { arity := 1 } { arity := 1 }) (ε_ { arity := 1 } { arity := 1 }) = circleVal f • CategoryTheory.CategoryStruct.id { arity := 0 }

The categorical circle: composing coevaluation and evaluation is the circle value times the identity.

theorem RS.circleVal_model {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : (stdSuperPair k ℓ).Hom (P.ω.obj { arity := 1 })) (e' : (P.ω.obj { arity := 1 }).Hom (stdSuperPair k ℓ)) (hee' : e.comp e' = SuperVect.Hom.id (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 ℓ) (hcopair : (SuperVect.tensorHom e' e').comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε P.ω) (CategoryTheory.CategoryStruct.comp (P.ω.map (η_ { arity := 1 } { arity := 1 })) (CategoryTheory.Functor.OplaxMonoidal.δ P.ω { arity := 1 } { arity := 1 }))) = stdCopair k ℓ) : circleVal f = ↑k - 2 * ↑ℓ

The circle value is the superdimension k − 2ℓ under any standard-model identification.