The canonical permutation of colour data

A mixed colouring of d slots splits into its even colours (a multiset, since they may repeat) and its odd colours (a list, whose order the summand's sign remembers). When the odd list is duplicate-free the colouring is a permutation of the canonical colouring at the same data — even colours sorted, odd colours in increasing order — and the permutation's odd inversion count is the odd list's own sorting sign.

That is what lets the mixed summand be read off the data alone: the functional sees only the multiset and the set, and the sign the reindexing costs is exactly the one the list carries.

Colour data extraction

noncomputable def RS.evenMultisetOf {k ℓ d : ℕ} (c : MixedColouring k ℓ d) : Multiset (Fin k)

The even colours of a mixed colouring, as a multiset: even colours may repeat.

Equations

• RS.evenMultisetOf c = ↑(List.filterMap Sum.getLeft? (List.ofFn c))

noncomputable def RS.oddListOf {k ℓ d : ℕ} (c : MixedColouring k ℓ d) : List (Fin (2 * ℓ))

The odd colours, in slot order: the list whose sorting sign the summand carries.

Equations

• RS.oddListOf c = List.filterMap Sum.getRight? (List.ofFn c)

noncomputable def RS.oddFinsetOf {k ℓ d : ℕ} (c : MixedColouring k ℓ d) : Finset (Fin (2 * ℓ))

The odd colours as a set — the index the functional is evaluated at.

Equations

• RS.oddFinsetOf c = (RS.oddListOf c).toFinset

Card bookkeeping

theorem RS.card_data {k ℓ d : ℕ} (c : MixedColouring k ℓ d) : d = (evenMultisetOf c).card + (oddListOf c).length

The two parts account for every slot.

theorem RS.card_oddFinset {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (hnodup : (oddListOf c).Nodup) : (oddFinsetOf c).card = (oddListOf c).length

When the odd list is duplicate-free its set has the same size.

Colour value rank

Colour rank for sorting

Monotonicity

Multiset decomposition

Canon list structure

Multiset equality between c and canon

Pair inversions

Inversions helpers

FilterMap structure lemma

theorem RS.filterMap_ofFn_sorted {β : Type u_1} {γ : Type u_2} {d n : ℕ} {f : Fin d → β} {g : β → Option γ} {ps : Fin n → Fin d} (hps : StrictMono ps) {vals : Fin n → γ} (hgfp : ∀ (t : Fin n), g (f (ps t)) = some (vals t)) (hgfn : ∀ (q : Fin d), (∀ (t : Fin n), ps t ≠ q) → g (f q) = none) : List.filterMap g (List.ofFn f) = List.ofFn vals

If g ∘ f is some (vals t) at positions ps t (strictly increasing) and none elsewhere, then filterMap g (ofFn f) equals ofFn vals.

Sign clause

Main theorem

theorem RS.exists_canonPerm {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (hnodup : (oddListOf c).Nodup) : ∃ (σ : Equiv.Perm (Fin d)) (h : d = (evenMultisetOf c).card + (oddFinsetOf c).card), c ∘ ⇑σ = canonColouring (evenMultisetOf c) (oddFinsetOf c) ∘ ⇑(finCongr h) ∧ (-1) ^ oddInversions σ c = ↑(sortSign (oddListOf c))

The canonical permutation: any colouring with a duplicate-free odd list is a permutation of the canonical one at its own data, and the permutation's odd inversion sign is exactly the odd list's sorting sign.