Prime shuffle coefficients in the Fox--Neuwirth boundary

Merging two consecutive blocks of sizes k and p-k produces one contribution for every order-preserving shuffle of the two blocks. The number of such shuffles is p.choose k. For a prime p and 0 < k < p, this coefficient is divisible by p; this is the arithmetic reason the sum of the top dual cells is a cycle modulo p.

def NRR.FoxNeuwirth.ShuffleIndex (p k : ℕ) : Type

A shuffle is encoded by the positions occupied by the first block.

Equations

• NRR.FoxNeuwirth.ShuffleIndex p k = { s : Finset (Fin p) // s.card = k }

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirth.ShuffleIndex.instFintype {p k : ℕ} : Fintype (ShuffleIndex p k)

Equations

• NRR.FoxNeuwirth.ShuffleIndex.instFintype = id inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirth.ShuffleIndex.instDecidableEq {p k : ℕ} : DecidableEq (ShuffleIndex p k)

Equations

• NRR.FoxNeuwirth.ShuffleIndex.instDecidableEq = Classical.decEq (NRR.FoxNeuwirth.ShuffleIndex p k)

@[simp]

theorem NRR.FoxNeuwirth.ShuffleIndex.card (p k : ℕ) : Fintype.card (ShuffleIndex p k) = p.choose k

def NRR.FoxNeuwirth.shuffleMultiplicity (p k : ℕ) : ℕ

Number of order-preserving shuffles of blocks of sizes k and p-k.

Equations

• NRR.FoxNeuwirth.shuffleMultiplicity p k = p.choose k

theorem NRR.FoxNeuwirth.card_shuffleIndex {p k : ℕ} : Fintype.card (ShuffleIndex p k) = shuffleMultiplicity p k

@[simp]

theorem NRR.FoxNeuwirth.shuffleMultiplicity_zero (p : ℕ) : shuffleMultiplicity p 0 = 1

@[simp]

theorem NRR.FoxNeuwirth.shuffleMultiplicity_self (p : ℕ) : shuffleMultiplicity p p = 1

theorem NRR.FoxNeuwirth.prime_dvd_shuffleMultiplicity {p k : ℕ} (hp : Nat.Prime p) (hk0 : 0 < k) (hkp : k < p) : p ∣ shuffleMultiplicity p k

theorem NRR.FoxNeuwirth.shuffleMultiplicity_mod_prime_eq_zero {p k : ℕ} (hp : Nat.Prime p) (hk0 : 0 < k) (hkp : k < p) : shuffleMultiplicity p k % p = 0

def NRR.FoxNeuwirth.unsignedFacetCoefficient (p leftSize : ℕ) : ℤ

The unsigned codimension-one boundary coefficient for a split into nonempty blocks.

Equations

• NRR.FoxNeuwirth.unsignedFacetCoefficient p leftSize = ↑(NRR.FoxNeuwirth.shuffleMultiplicity p leftSize)

theorem NRR.FoxNeuwirth.prime_dvd_unsignedFacetCoefficient {p k : ℕ} (hp : Nat.Prime p) (hk0 : 0 < k) (hkp : k < p) : ↑p ∣ unsignedFacetCoefficient p k