Canonical configurations of barred permutations

Every barred permutation has a concrete labelled planar configuration: the first coordinate is the block number and the second coordinate is the permutation rank. This realizes every Fox--Neuwirth symbol by an actual collision-free configuration and is equivariant for relabelling.

@[instance_reducible]

instance NRR.BarredPermutation.instTopologicalSpace {p : ℕ} : TopologicalSpace (BarredPermutation p)

Discrete topology on the finite set of barred permutations.

Equations

• NRR.BarredPermutation.instTopologicalSpace = ⊥

instance NRR.BarredPermutation.instDiscreteTopology {p : ℕ} : DiscreteTopology (BarredPermutation p)

noncomputable def NRR.BarredPermutation.canonicalPoint {p : ℕ} (c : BarredPermutation p) (i : Fin p) : E2

Canonical point assigned to a label in a barred-permutation stratum.

Equations

• c.canonicalPoint i = !₂[↑(c.blockIndex i), ↑↑(c.rank i)]

@[simp]

theorem NRR.BarredPermutation.canonicalPoint_x {p : ℕ} (c : BarredPermutation p) (i : Fin p) : (c.canonicalPoint i).ofLp 0 = ↑(c.blockIndex i)

@[simp]

theorem NRR.BarredPermutation.canonicalPoint_y {p : ℕ} (c : BarredPermutation p) (i : Fin p) : (c.canonicalPoint i).ofLp 1 = ↑↑(c.rank i)

theorem NRR.BarredPermutation.canonicalPoint_injective {p : ℕ} (c : BarredPermutation p) : Function.Injective c.canonicalPoint

noncomputable def NRR.BarredPermutation.canonicalConfig {p : ℕ} (c : BarredPermutation p) : Config p

Concrete configuration representing the stratum symbol.

Equations

• c.canonicalConfig = ⟨c.canonicalPoint, ⋯⟩

@[simp]

theorem NRR.BarredPermutation.canonicalConfig_pts {p : ℕ} (c : BarredPermutation p) (i : Fin p) : c.canonicalConfig.pts i = c.canonicalPoint i

theorem NRR.BarredPermutation.canonicalConfig_relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) : (relabel σ c).canonicalConfig = Config.relabel σ c.canonicalConfig

noncomputable def NRR.BarredPermutation.canonicalConfigMap {p : ℕ} : C(BarredPermutation p, Config p)

The finite canonical-configuration map is continuous for the discrete domain topology.

Equations

• NRR.BarredPermutation.canonicalConfigMap = { toFun := NRR.BarredPermutation.canonicalConfig, continuous_toFun := ⋯ }