The coordinate interface

A morphism ⟨0⟩ ⟶ ⟨d⟩ of the skein category has an image vector in the fibre of ⟨d⟩ (evaluate the unit-conjugated image at 1), and a morphism ⟨d⟩ ⟶ ⟨0⟩ has an image functional. The scalar of a composite is the functional applied to the vector — definitionally. Specialised to the star composite this expresses the parameter value as a pairing in the fibre, ready for the standard-model coordinates.

noncomputable def RS.omegaVec {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {d : ℕ} (p : { arity := 0 } ⟶ { arity := d }) : (P.ω.obj { arity := d }).even

The image vector of a ⟨0⟩ ⟶ ⟨d⟩ morphism.

Equations

• RS.omegaVec f P p = (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε P.ω) (P.ω.map p)).evenMap 1

noncomputable def RS.omegaFun {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {d : ℕ} (q : { arity := d } ⟶ { arity := 0 }) : (P.ω.obj { arity := d }).even →ₗ[ℂ] ℂ

The image functional of a ⟨d⟩ ⟶ ⟨0⟩ morphism.

Equations

• RS.omegaFun f P q = (CategoryTheory.CategoryStruct.comp (P.ω.map q) (CategoryTheory.Functor.OplaxMonoidal.η P.ω)).evenMap

theorem RS.omega_pairing {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {d : ℕ} (p : { arity := 0 } ⟶ { arity := d }) (q : { arity := d } ⟶ { arity := 0 }) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε P.ω) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (P.ω.map p) (P.ω.map q)) (CategoryTheory.Functor.OplaxMonoidal.η P.ω))).evenMap 1 = (omegaFun f P q) (omegaVec f P p)

The pairing split: the scalar of a composite is the functional applied to the vector.

theorem RS.star_pairing {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (W : ClosedFragment) : (omegaFun f P (bundleCapClass f (edgeCount W))) (omegaVec f P (starClass f W)) = f.val W

The parameter value as a fibre pairing.

def RS.vertexStar (d : ℕ) : Fragment (Fin d)

The single-vertex star with d legs: one internal vertex, d pendant edges.

Equations

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

noncomputable def RS.starVec {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (d : ℕ) : (P.ω.obj { arity := d }).even

The degree-d vertex functional data: the image vector of the vertex star read as a (0, d)-morphism.

Equations

• RS.starVec f P d = RS.omegaVec f P (RS.HomSpace.ofFragment f.val ((RS.vertexStar d).relabel (finCongr ⋯)))