Barred permutations for the planar Fox--Neuwirth stratification

A barred permutation records a total vertical order of the labels and cuts that divide this order into consecutive blocks. A block represents labels with equal first coordinate; the block order is their strict first-coordinate order and the permutation order inside a block is their strict second-coordinate order.

The dual Fox--Neuwirth cell has dimension p - blockCount. Thus one-block symbols index top dual cells of dimension p - 1, while the all-singleton symbols index vertices.

structure NRR.BarredPermutation (p : ℕ) : Type

Exact finite combinatorial symbol for a planar Fox--Neuwirth stratum.

rank i is the position of label i in the displayed permutation. A member k of bars places a bar after position k.

• rank : Equiv.Perm (Fin p)

  The ordering of labels in the barred permutation.

• bars : Finset (Fin (p - 1))

  The positions at which bars divide the ordered labels into blocks.

@[instance_reducible]

instance NRR.instFintypeBarredPermutation {p✝ : ℕ} : Fintype (BarredPermutation p✝)

Equations

• NRR.instFintypeBarredPermutation = Fintype.ofEquiv ((_ : Equiv.Perm (Fin p✝)) × Finset (Fin (p✝ - 1))) (NRR.BarredPermutation.proxyTypeEquiv p✝)

def NRR.instDecidableEqBarredPermutation.decEq {p✝ : ℕ} (x✝ x✝¹ : BarredPermutation p✝) : Decidable (x✝ = x✝¹)

Equations

• NRR.instDecidableEqBarredPermutation.decEq { rank := a, bars := a_1 } { rank := b, bars := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance NRR.instDecidableEqBarredPermutation {p✝ : ℕ} : DecidableEq (BarredPermutation p✝)

Equations

• NRR.instDecidableEqBarredPermutation = NRR.instDecidableEqBarredPermutation.decEq

theorem NRR.BarredPermutation.ext {p : ℕ} {a b : BarredPermutation p} (hrank : a.rank = b.rank) (hbars : a.bars = b.bars) : a = b

theorem NRR.BarredPermutation.ext_iff {p : ℕ} {a b : BarredPermutation p} : a = b ↔ a.rank = b.rank ∧ a.bars = b.bars

def NRR.BarredPermutation.blockIndex {p : ℕ} (c : BarredPermutation p) (i : Fin p) : ℕ

Number of bars strictly before the rank of a label. This is the zero-based block number.

Equations

• c.blockIndex i = {k ∈ c.bars | ↑k < ↑(c.rank i)}.card

def NRR.BarredPermutation.SameBlock {p : ℕ} (c : BarredPermutation p) (i j : Fin p) : Prop

Two labels lie on the same vertical line in the represented stratum.

Equations

• c.SameBlock i j = (c.blockIndex i = c.blockIndex j)

@[instance_reducible]

instance NRR.BarredPermutation.instDecidableRelFinSameBlock {p : ℕ} (c : BarredPermutation p) : DecidableRel c.SameBlock

Equations

• c.instDecidableRelFinSameBlock i j = { decide := (c.blockIndex i).beq (c.blockIndex j), reflects_decide := ⋯ }

def NRR.BarredPermutation.blockCount {p : ℕ} (c : BarredPermutation p) : ℕ

Number of nonempty consecutive blocks. There are no blocks for p = 0.

Equations

• c.blockCount = if p = 0 then 0 else c.bars.card + 1

def NRR.BarredPermutation.dualDimension {p : ℕ} (c : BarredPermutation p) : ℕ

Dimension in the dual Fox--Neuwirth complex.

Equations

• c.dualDimension = p - c.blockCount

def NRR.BarredPermutation.IsTop {p : ℕ} (c : BarredPermutation p) : Prop

One-block symbols are the top-dimensional dual cells.

Equations

• c.IsTop = (c.bars = ∅)

@[instance_reducible]

instance NRR.BarredPermutation.isTopDecidable {p : ℕ} (c : BarredPermutation p) : Decidable c.IsTop

Equations

• c.isTopDecidable = id inferInstance

def NRR.BarredPermutation.IsVertex {p : ℕ} (c : BarredPermutation p) : Prop

All-singleton symbols are vertices of the dual complex.

Equations

• c.IsVertex = (c.bars = Finset.univ)

def NRR.BarredPermutation.relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) : BarredPermutation p

Relabel a symbol by precomposition with σ.symm, matching Config.relabel.

Equations

• NRR.BarredPermutation.relabel σ c = { rank := (Equiv.symm σ).trans c.rank, bars := c.bars }

@[simp]

theorem NRR.BarredPermutation.relabel_rank {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) (i : Fin p) : (relabel σ c).rank i = c.rank ((Equiv.symm σ) i)

@[simp]

theorem NRR.BarredPermutation.relabel_bars {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) : (relabel σ c).bars = c.bars

@[simp]

theorem NRR.BarredPermutation.relabel_one {p : ℕ} (c : BarredPermutation p) : relabel 1 c = c

theorem NRR.BarredPermutation.relabel_mul {p : ℕ} (σ τ : Equiv.Perm (Fin p)) (c : BarredPermutation p) : relabel (σ * τ) c = relabel σ (relabel τ c)

@[simp]

theorem NRR.BarredPermutation.blockIndex_relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) (i : Fin p) : (relabel σ c).blockIndex i = c.blockIndex ((Equiv.symm σ) i)

@[simp]

theorem NRR.BarredPermutation.sameBlock_relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) (i j : Fin p) : (relabel σ c).SameBlock i j ↔ c.SameBlock ((Equiv.symm σ) i) ((Equiv.symm σ) j)

@[simp]

theorem NRR.BarredPermutation.blockCount_relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) : (relabel σ c).blockCount = c.blockCount

@[simp]

theorem NRR.BarredPermutation.dualDimension_relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) : (relabel σ c).dualDimension = c.dualDimension

@[simp]

theorem NRR.BarredPermutation.isTop_relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) : (relabel σ c).IsTop ↔ c.IsTop

@[simp]

theorem NRR.BarredPermutation.isVertex_relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : BarredPermutation p) : (relabel σ c).IsVertex ↔ c.IsVertex

def NRR.BarredPermutation.IsFace {p : ℕ} (a b : BarredPermutation p) : Prop

Face relation in the dual complex.

a.IsFace b means that the stratum symbol a is a refinement of b: ordered blocks of a may be merged, but never reordered, and the vertical order inside every block of a is preserved. The final conjunct records the corresponding dual-dimension inequality explicitly.

Equations

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

theorem NRR.BarredPermutation.isFace_refl {p : ℕ} (a : BarredPermutation p) : a.IsFace a

theorem NRR.BarredPermutation.isFace_trans {p : ℕ} {a b c : BarredPermutation p} (hab : a.IsFace b) (hbc : b.IsFace c) : a.IsFace c

theorem NRR.BarredPermutation.isFace_relabel {p : ℕ} {a b : BarredPermutation p} (h : a.IsFace b) (σ : Equiv.Perm (Fin p)) : (relabel σ a).IsFace (relabel σ b)

def NRR.BarredPermutation.IsFacet {p : ℕ} (a b : BarredPermutation p) : Prop

Codimension-one face relation.

Equations

• a.IsFacet b = (a.IsFace b ∧ a.dualDimension + 1 = b.dualDimension)

@[instance_reducible]

noncomputable instance NRR.BarredPermutation.isFaceDecidable {p : ℕ} (a b : BarredPermutation p) : Decidable (a.IsFace b)

Equations

• a.isFaceDecidable b = Classical.dec (a.IsFace b)

@[instance_reducible]

noncomputable instance NRR.BarredPermutation.isFacetDecidable {p : ℕ} (a b : BarredPermutation p) : Decidable (a.IsFacet b)

Equations

• a.isFacetDecidable b = Classical.dec (a.IsFacet b)

theorem NRR.BarredPermutation.isFacet_relabel {p : ℕ} {a b : BarredPermutation p} (h : a.IsFacet b) (σ : Equiv.Perm (Fin p)) : (relabel σ a).IsFacet (relabel σ b)

theorem NRR.BarredPermutation.bars_card_le {p : ℕ} (c : BarredPermutation p) : c.bars.card ≤ p - 1

theorem NRR.BarredPermutation.blockCount_eq {p : ℕ} (c : BarredPermutation p) (hp0 : 0 < p) : c.blockCount = c.bars.card + 1

theorem NRR.BarredPermutation.dualDimension_eq {p : ℕ} (c : BarredPermutation p) (hp0 : 0 < p) : c.dualDimension = p - 1 - c.bars.card

theorem NRR.BarredPermutation.dualDimension_top {p : ℕ} (c : BarredPermutation p) (hp0 : 0 < p) (hc : c.IsTop) : c.dualDimension = p - 1

theorem NRR.BarredPermutation.dualDimension_vertex {p : ℕ} (c : BarredPermutation p) (hp0 : 0 < p) (hc : c.IsVertex) : c.dualDimension = 0

@[instance_reducible]

instance NRR.BarredPermutation.primeSymmetryAction (p : ℕ) : MulAction (↥(PrimeSymmetry p)) (BarredPermutation p)

The prime symmetry action on barred permutations.

Equations

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

@[simp]

theorem NRR.BarredPermutation.prime_smul_def (p : ℕ) (g : ↥(PrimeSymmetry p)) (c : BarredPermutation p) : g • c = relabel ((PrimeSymmetry.toPerm p) g) c