Sorting a multi-star into blocks

An arbitrary vertex assignment of a multi-star is sorted into block form: the degree list records the fibre sizes in vertex order, and the sort equivalence regroups the slots fibre by fibre. Relabelling along the sort turns the multi-star into the block-assigned form, ready for the block factorization.

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

The degree list of an assignment: fibre sizes in vertex order.

Equations

• RS.degList assign = List.ofFn fun (v : Fin m) => Fintype.card { i : Fin n // assign i = v }

theorem RS.degList_length {n m : ℕ} (assign : Fin n → Fin m) : (degList assign).length = m

The degree list has one entry per vertex.

theorem RS.degList_get {n m : ℕ} (assign : Fin n → Fin m) (w : Fin (degList assign).length) : (degList assign).get w = Fintype.card { i : Fin n // assign i = (finCongr ⋯) w }

Each entry is that vertex's fibre size.

theorem RS.sum_card_fibres {n m : ℕ} (assign : Fin n → Fin m) : ∑ v : Fin m, Fintype.card { i : Fin n // assign i = v } = n

The fibre sizes sum to the total.

theorem RS.degList_sum {n m : ℕ} (assign : Fin n → Fin m) : (degList assign).sum = n

The degrees sum to the slot count: the fibres partition the slots.

theorem RS.degList_card_sigma {n m : ℕ} (assign : Fin n → Fin m) : Fintype.card ((w : Fin (degList assign).length) × Fin ((degList assign).get w)) = n

The block-form index space has the right cardinality.

noncomputable def RS.sortFun {n m : ℕ} (assign : Fin n → Fin m) (i : Fin n) : (w : Fin (degList assign).length) × Fin ((degList assign).get w)

The sort map: a slot goes to its vertex block at its enumerated offset within the fibre.

Equations

• RS.sortFun assign i = ⟨(finCongr ⋯) (assign i), (finCongr ⋯) ((Fintype.equivFin { i_1 : Fin n // assign i_1 = (finCongr ⋯) ((finCongr ⋯) (assign i)) }) ⟨i, ⋯⟩)⟩

noncomputable def RS.unsortFun {n m : ℕ} (assign : Fin n → Fin m) (p : (w : Fin (degList assign).length) × Fin ((degList assign).get w)) : Fin n

The unsort map: read the fibre element back off.

Equations

• RS.unsortFun assign p = ↑((Fintype.equivFin { i : Fin n // assign i = (finCongr ⋯) p.fst }).symm ((finCongr ⋯) p.snd))

theorem RS.unsort_sort {n m : ℕ} (assign : Fin n → Fin m) (i : Fin n) : unsortFun assign (sortFun assign i) = i

Unsorting undoes sorting.

theorem RS.sortFun_bijective {n m : ℕ} (assign : Fin n → Fin m) : Function.Bijective (sortFun assign)

So the sort is a bijection of slots.

noncomputable def RS.sortSigma {n m : ℕ} (assign : Fin n → Fin m) : Fin n ≃ (w : Fin (degList assign).length) × Fin ((degList assign).get w)

The sort equivalence onto the block index space.

Equations

• RS.sortSigma assign = Equiv.ofBijective (RS.sortFun assign) ⋯

theorem RS.sortSigma_fst {n m : ℕ} (assign : Fin n → Fin m) (i : Fin n) : ((sortSigma assign) i).fst = (finCongr ⋯) (assign i)

The sorted slot's block index is its vertex.

noncomputable def RS.multiStarCompRelabel {V V' : Type} [Fintype V] [Fintype V'] {n N : ℕ} (assign : Fin n → V) (c : ℕ) (σ : Fin n ≃ Fin N) (b : Fin N → V') (e : V ≃ V') (hb : ∀ (i : Fin n), b (σ i) = e (assign i)) : (multiStar assign c).Equiv ((multiStar b c).relabel σ.symm)

Sorting a multi-star: a slot equivalence intertwining the assignments (through a vertex identification) relabels one multi-star onto the other.

Equations

• RS.multiStarCompRelabel assign c σ b e hb = { flagEquiv := σ.sumCongr σ, vertexEquiv := e, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }