Planar Fox--Neuwirth strata

The stratum of a barred permutation is described directly in the labelled configuration space. Labels in one block have equal first coordinate and occur in the recorded vertical order; labels in different blocks occur in the recorded left-to-right order.

theorem NRR.BarredPermutation.blockIndex_mono {p : ℕ} (c : BarredPermutation p) {i j : Fin p} (hij : ↑(c.rank i) ≤ ↑(c.rank j)) : c.blockIndex i ≤ c.blockIndex j

theorem NRR.BarredPermutation.blockIndex_lt_of_rank_lt_of_not_sameBlock {p : ℕ} (c : BarredPermutation p) {i j : Fin p} (hij : ↑(c.rank i) < ↑(c.rank j)) (hblock : ¬c.SameBlock i j) : c.blockIndex i < c.blockIndex j

def NRR.BarredPermutation.InStratum {p : ℕ} (c : BarredPermutation p) (s : Config p) : Prop

Membership in the open Fox--Neuwirth stratum represented by c.

Equations

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

theorem NRR.BarredPermutation.canonicalConfig_mem_stratum {p : ℕ} (c : BarredPermutation p) : c.InStratum c.canonicalConfig

theorem NRR.BarredPermutation.inStratum_relabel_iff {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) (s : Config p) : (relabel σ c).InStratum (Config.relabel σ s) ↔ c.InStratum s

Relabelling transports a stratum to the relabelled stratum.