The class-level star factorization #
Transporting the fragment-level star factorization to Hom classes: the star-union class of a closed fragment is the circle power times the iterated vertex-star tensor class composed with the bundle map of the sort.
theorem
RS.ofFragment_addCircles
{R : ℕ}
(f : EdgeRankParameter R)
{t : ℕ}
(Y : Fragment (Fin t))
(c : ℕ)
:
Free circles are a scalar on classes, at any arity.
theorem
RS.comp_bundleMapClass
{R : ℕ}
(f : EdgeRankParameter R)
{s n m : ℕ}
(e : Fin n ≃ Fin m)
(X : Fragment (Fin (s + n)))
:
((HomSpace.comp f s n m) (HomSpace.ofFragment f.val X)) (bundleMapClass f e) = HomSpace.ofFragment f.val
(X.relabel (finSumFinEquiv.symm.trans (((Equiv.refl (Fin s)).sumCongr e).trans finSumFinEquiv)))
Composing with a bundle-map class relabels the fragment along the outgoing transport.
theorem
RS.sort_transport_eq
{N M : ℕ}
(σ : Fin N ≃ Fin M)
:
(finCongr ⋯).trans (finSumFinEquiv.symm.trans (((Equiv.refl (Fin 0)).sumCongr σ).trans finSumFinEquiv)) = σ.trans (finCongr ⋯)
At source arity zero the outgoing transport is the map itself, up to padding casts.
theorem
RS.starClass_factor
{R : ℕ}
(f : EdgeRankParameter R)
(W : ClosedFragment)
:
starClass f W = circleVal f ^ W.circles • ((HomSpace.comp f 0 (degList (starAssignEnum W)).sum (edgeCount W + edgeCount W))
(HomSpace.ofFragment f.val ((starTensor (degList (starAssignEnum W))).relabel (finCongr ⋯))))
(bundleMapClass f (sortEquiv (starAssignEnum W)).symm)
The class-level star factorization: the star-union class is the circle power times the iterated vertex-star tensor class, composed with the bundle map of the sort.