Transporting the star identity through the fibre functor

Applying a Deligne package's fibre functor to the categorical star identity: the images of the star-union and bundle classes compose to the parameter value times the identity of the image of the unit object.

theorem RS.empty_class_eq_id {R : ℕ} (f : EdgeRankParameter R) : HomSpace.ofFragment f.val emptyClosedFragment = CategoryTheory.CategoryStruct.id { arity := 0 }

The empty class is the identity of the unit object.

theorem RS.omega_star {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (W : ClosedFragment) : CategoryTheory.CategoryStruct.comp (P.ω.map (starClass f W)) (P.ω.map (bundleCapClass f (edgeCount W))) = f.val W • CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 0 })

The transported star identity: the fibre functor sends the star composite to the parameter value times the identity.

theorem RS.omega_star_scalar {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (W : ClosedFragment) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε P.ω) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (P.ω.map (starClass f W)) (P.ω.map (bundleCapClass f (edgeCount W)))) (CategoryTheory.Functor.OplaxMonoidal.η P.ω))).evenMap 1 = f.val W

The transported star identity, as a scalar: conjugating by the unit structure maps and evaluating the even part at 1 recovers the parameter value.

theorem RS.skein_std_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 ℓ)), e'.comp e = SuperVect.Hom.id (stdSuperPair k ℓ) ∧ e.comp e' = SuperVect.Hom.id (P.ω.obj { arity := 1 }) ∧ 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 ℓ ∧ (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 ℓ

The standard model of the skein category: any Deligne package yields dimensions k, ℓ and an isomorphism of the strand image with the standard super vector space carrying the evaluation to the standard form and the coevaluation to the standard copairing.