The sorted factorization of a multi-star

Chaining the sort with the block enumeration and the block factorization: any multi-star is, up to relabelling along the sort, the iterated tensor of vertex stars over its degree list with the free circles split off. Specialised to the star union this is the fragment-level star factorization.

noncomputable def RS.sortEquiv {n m : ℕ} (assign : Fin n → Fin m) : Fin n ≃ Fin (degList assign).sum

The full sort: slots to the block-concatenated enumeration.

Equations

• RS.sortEquiv assign = (RS.sortSigma assign).trans (RS.blockSigmaEquiv (RS.degList assign))

theorem RS.blockAssign_sortEquiv {n m : ℕ} (assign : Fin n → Fin m) (i : Fin n) : blockAssign (degList assign) ((sortEquiv assign) i) = (finCongr ⋯) (assign i)

The sort intertwines the assignment with the block assignment.

noncomputable def RS.multiStarSorted {n m : ℕ} (assign : Fin n → Fin m) (c : ℕ) : (multiStar assign c).Equiv ((multiStar (blockAssign (degList assign)) c).relabel (sortEquiv assign).symm)

Sorting a multi-star into block-assigned form.

Equations

• RS.multiStarSorted assign c = RS.multiStarCompRelabel assign c (RS.sortEquiv assign) (RS.blockAssign (RS.degList assign)) (finCongr ⋯) ⋯

noncomputable def RS.multiStarFactor {n m : ℕ} (assign : Fin n → Fin m) (c : ℕ) : (multiStar assign c).Equiv ((addCircles (starTensor (degList assign)) c).relabel (sortEquiv assign).symm)

The sorted factorization: a multi-star is the iterated tensor of vertex stars over its degree list, with the circles split off, relabelled along the sort.

Equations

• RS.multiStarFactor assign c = (RS.multiStarSorted assign c).trans ((RS.multiStarBlocks (RS.degList assign) c).relabelCongr (RS.sortEquiv assign).symm)

noncomputable def RS.multiStarVertexMap {V V' : Type} [Fintype V] [Fintype V'] {n : ℕ} (assign : Fin n → V) (c : ℕ) (e : V ≃ V') : (multiStar assign c).Equiv (multiStar (⇑e ∘ assign) c)

Reindexing the vertices of a multi-star.

Equations

• RS.multiStarVertexMap assign c e = { flagEquiv := Equiv.refl (RS.multiStar assign c).Flag, vertexEquiv := e, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

noncomputable def RS.starAssignEnum (W : ClosedFragment) : Fin (edgeCount W + edgeCount W) → Fin (Fintype.card W.Vertex)

The star union's assignment, with vertices enumerated.

Equations

• RS.starAssignEnum W = ⇑(Fintype.equivFin W.Vertex) ∘ RS.starAssign W

noncomputable def RS.starUnionFactor (W : ClosedFragment) : (starUnion W).Equiv ((addCircles (starTensor (degList (starAssignEnum W))) W.circles).relabel (sortEquiv (starAssignEnum W)).symm)

The fragment-level star factorization: the star union of a closed fragment is the iterated tensor of its vertex stars over the degree list, with its free circles split off, relabelled along the sort.

Equations

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