The star-tensor class and its recursion

The iterated vertex-star tensor as a Hom class, with its defining recursion at class level: the cons case is the monoidal tensor of the vertex-star class with the tail, composed with the sum cast.

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

The vertex-star class: a (0, d)-morphism.

Equations

• RS.vertexStarClass f d = RS.HomSpace.ofFragment f.val ((RS.vertexStar d).relabel (finCongr ⋯))

noncomputable def RS.starTensorClass {R : ℕ} (f : EdgeRankParameter R) (ds : List ℕ) : HomSpace f.val (0 + ds.sum)

The star-tensor class over a degree list.

Equations

• RS.starTensorClass f ds = RS.HomSpace.ofFragment f.val ((RS.starTensor ds).relabel (finCongr ⋯))

theorem RS.starTensorClass_nil {R : ℕ} (f : EdgeRankParameter R) : starTensorClass f [] = HomSpace.ofFragment f.val emptyClosedFragment

The empty star tensor is the empty class.

theorem RS.starTensorClass_cons {R : ℕ} (f : EdgeRankParameter R) (d : ℕ) (ds : List ℕ) : starTensorClass f (d :: ds) = ((HomSpace.comp f 0 (d + ds.sum) (d :: ds).sum) (((HomSpace.tensor f 0 d 0 ds.sum) (vertexStarClass f d)) (starTensorClass f ds))) (bundleMapClass f (finCongr ⋯))

The class recursion: the star tensor over a cons is the tensor of the head vertex-star class with the tail class, composed with the sum cast.

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)) (starTensorClass f (degList (starAssignEnum W)))) (bundleMapClass f (sortEquiv (starAssignEnum W)).symm)

The class-level star factorization, in terms of the star-tensor class.