Peeling the multi-star into vertex stars

The block-sorted multi-star over a degree list is the iterated tensor of vertex stars: blockAssign sends each slot to its block, starTensor is the iterated tensor, and the peel induction identifies them.

def RS.blockAssign (ds : List ℕ) : Fin ds.sum → Fin ds.length

The block of a slot in a degree list.

Equations

• RS.blockAssign [] i = i.elim0
• RS.blockAssign (d :: ds) i = if h : ↑i < d then ⟨0, ⋯⟩ else (RS.blockAssign ds ⟨↑i - d, ⋯⟩).succ

noncomputable def RS.starTensor (ds : List ℕ) : Fragment (Fin ds.sum)

The iterated tensor of vertex stars over a degree list.

Equations

• RS.starTensor [] = RS.emptyClosedFragment
• RS.starTensor (d :: ds) = (RS.tensorFragment ((RS.vertexStar d).relabel (finCongr ⋯)) ((RS.starTensor ds).relabel (finCongr ⋯))).relabel (finCongr ⋯)

noncomputable def RS.multiStarNil (c : ℕ) : (multiStar (blockAssign []) c).Equiv (addCircles (starTensor []) c)

The empty multi-star is the empty fragment.

Equations

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

def RS.peelVertexFun (n : ℕ) (v : Fin (n + 1)) : Unit ⊕ Fin n

The head-vertex splitting map.

Equations

• RS.peelVertexFun n v = if h : ↑v = 0 then Sum.inl () else Sum.inr ⟨↑v - 1, ⋯⟩

def RS.peelVertexInv (n : ℕ) : Unit ⊕ Fin n → Fin (n + 1)

The head-vertex merging map.

Equations

• RS.peelVertexInv n (Sum.inl val) = ⟨0, ⋯⟩
• RS.peelVertexInv n (Sum.inr j) = ⟨↑j + 1, ⋯⟩

def RS.peelVertexEquiv (n : ℕ) : Fin (n + 1) ≃ Unit ⊕ Fin n

The head-vertex split.

Equations

• RS.peelVertexEquiv n = { toFun := RS.peelVertexFun n, invFun := RS.peelVertexInv n, left_inv := ⋯, right_inv := ⋯ }

theorem RS.peelVertexEquiv_zero (n : ℕ) (h : 0 < n + 1) : (peelVertexEquiv n) ⟨0, h⟩ = Sum.inl ()

The peel splits off the first vertex.

theorem RS.peelVertexEquiv_succ (n : ℕ) (j : Fin n) : (peelVertexEquiv n) j.succ = Sum.inr j

And leaves the rest in order.

def RS.peelFlagEquiv (d S : ℕ) : Fin (d + S) ⊕ Fin (d + S) ≃ (Fin d ⊕ Fin d) ⊕ Fin S ⊕ Fin S

The slot shuffle of the peel.

Equations

• RS.peelFlagEquiv d S = (finSumFinEquiv.symm.sumCongr finSumFinEquiv.symm).trans (Equiv.sumSumSumComm (Fin d) (Fin S) (Fin d) (Fin S))

theorem RS.peelFlagEquiv_inl_low (d S : ℕ) (i : Fin d) : (peelFlagEquiv d S) (Sum.inl (Fin.castAdd S i)) = Sum.inl (Sum.inl i)

On the left side, the first block's flags go to the peeled star.

theorem RS.peelFlagEquiv_inl_high (d S : ℕ) (j : Fin S) : (peelFlagEquiv d S) (Sum.inl (Fin.natAdd d j)) = Sum.inr (Sum.inl j)

And the remaining left flags to the rest.

theorem RS.peelFlagEquiv_inr_low (d S : ℕ) (i : Fin d) : (peelFlagEquiv d S) (Sum.inr (Fin.castAdd S i)) = Sum.inl (Sum.inr i)

On the right side, the first block's flags go to the peeled star.

theorem RS.peelFlagEquiv_inr_high (d S : ℕ) (j : Fin S) : (peelFlagEquiv d S) (Sum.inr (Fin.natAdd d j)) = Sum.inr (Sum.inr j)

And the remaining right flags to the rest.

noncomputable def RS.multiStarPeel {n : ℕ} (d S c : ℕ) (rest : Fin S → Fin n) (a : Fin (d + S) → Fin (n + 1)) (ha_low : ∀ (i : Fin d), a (Fin.castAdd S i) = ⟨0, ⋯⟩) (ha_high : ∀ (j : Fin S), a (Fin.natAdd d j) = (rest j).succ) : (multiStar a c).Equiv ((tensorFragment ((vertexStar d).relabel (finCongr ⋯)) ((multiStar rest c).relabel (finCongr ⋯))).relabel (finCongr ⋯))

The peel step, generically: a multi-star whose assignment splits blockwise is the head vertex star tensored with the tail multi-star.

Equations

• RS.multiStarPeel d S c rest a ha_low ha_high = { flagEquiv := RS.peelFlagEquiv d S, vertexEquiv := RS.peelVertexEquiv n, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

noncomputable def RS.tensorAddCirclesRight {s t u v : ℕ} (A : Fragment (Fin (s + t))) (B : Fragment (Fin (u + v))) (c : ℕ) : (tensorFragment A (addCircles B c)).Equiv (addCircles (tensorFragment A B) c)

Circles migrate out of the second tensor factor.

Equations

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

noncomputable def RS.multiStarBlocks (ds : List ℕ) (c : ℕ) : (multiStar (blockAssign ds) c).Equiv (addCircles (starTensor ds) c)

The block factorization: a block-sorted multi-star is the iterated tensor of vertex stars with the circles split off.

Equations

• One or more equations did not get rendered due to their size.
• RS.multiStarBlocks [] x✝ = RS.multiStarNil x✝