The sorted-position key

The block enumeration is sorted under the sigma-position key, so the canonical index permutation's sign is the key-sortSign of the pair enumeration alone.

noncomputable def RS.sortKey (W : ClosedFragment) (f : W.Flag) : Fin (ds W).sum

The sorted-position key of a flag.

Equations

• RS.sortKey W f = (RS.sortEquiv (RS.starAssignEnum W)) ((RS.starFlagEnum W) f)

theorem RS.sortKey_injective (W : ClosedFragment) : Function.Injective (sortKey W)

The key is injective.

theorem RS.sortKey_blockFlag (W : ClosedFragment) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : sortKey W (blockFlag W v j) = (blockSigmaEquiv (ds W)) ⟨v, j⟩

The key of a block flag is its sigma position.

theorem RS.blockOddFlagList_key_sorted (W : ClosedFragment) (F : EdgeSubset W) (v : Fin (ds W).length) : List.Pairwise (fun (x1 x2 : Fin (ds W).sum) => x1 ≤ x2) (List.map (fun (f : ↥F.flags) => sortKey W ↑f) (blockOddFlagList W F v))

The block enumeration is sorted under the key.

theorem RS.blockOddFlagList_length_eq (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (v : Fin (ds W).length) : (blockOddFlagList W F v).length = (pairFlagList o (blockVertex W v)).length

The enumerations have equal length.

theorem RS.sortSign_pairFlagList_key (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (v : Fin (ds W).length) : sortSign (List.map (fun (f : ↥F.flags) => sortKey W ↑f) (pairFlagList o (blockVertex W v))) = ↑(Equiv.Perm.sign (listIndexPerm (blockOddFlagList W F v) (pairFlagList o (blockVertex W v)) ⋯ ⋯ ⋯ ⋯))

The per-vertex reindexing sign is the key-sortSign of the pair enumeration.