The star composite in the category

The accompanying paper's (★) in categorical form: composing the star-union class Hom(0, 2m) with the strand-bundle class Hom(2m, 0) is the parameter value times the empty class — the identity that the fibre functor transports into the standard model.

noncomputable def RS.starClass {R : ℕ} (f : EdgeRankParameter R) (W : ClosedFragment) : HomSpace f.val (0 + (edgeCount W + edgeCount W))

The star-union class as a (0, 2m)-morphism.

Equations

• RS.starClass f W = RS.HomSpace.ofFragment f.val ((RS.starUnion W).relabel (finCongr ⋯))

noncomputable def RS.bundleCapClass {R : ℕ} (f : EdgeRankParameter R) (m : ℕ) : HomSpace f.val (m + m + 0)

The strand-bundle class as a (2m, 0)-morphism.

Equations

• RS.bundleCapClass f m = RS.HomSpace.ofFragment f.val ((RS.strandBundle m).relabel (finCongr ⋯))

theorem RS.star_comp_class {R : ℕ} (f : EdgeRankParameter R) (W : ClosedFragment) : ((HomSpace.comp f 0 (edgeCount W + edgeCount W) 0) (starClass f W)) (bundleCapClass f (edgeCount W)) = f.val W • HomSpace.ofFragment f.val emptyClosedFragment

The categorical (★): the star composite is the parameter value times the empty class.