The reference zero orbit in the Fox--Neuwirth top-cell model

The reference map is the first-coordinate vector modulo the diagonal. On the standard simplex it vanishes exactly at the uniform weight vector. Consequently the full permutation group acts transitively on its zeros: there is one zero in every top cell, and all of them are relabelings of the identity-cell zero.

Restricting that full permutation torsor to the prime symmetry group gives one orbit for p = 2 and two orbits for odd primes, because the chosen group is respectively S_2 and A_p. Giving each orbit local coefficient 1 produces the nonzero reference count used in the prime argument.

noncomputable def NRR.FoxNeuwirth.uniformWeights {p : ℕ} (hp : Nat.Prime p) : FoxNeuwirthWeights p

Uniform barycentric weights on the p labels.

Equations

• NRR.FoxNeuwirth.uniformWeights hp = ⟨fun (x : Fin p) => 1 / ↑p, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirth.uniformWeights_apply {p : ℕ} (hp : Nat.Prime p) (i : Fin p) : ↑(uniformWeights hp) i = 1 / ↑p

theorem NRR.FoxNeuwirth.uniformWeights_relabel {p : ℕ} (hp : Nat.Prime p) (sigma : Equiv.Perm (Fin p)) : FoxNeuwirthWeights.relabel sigma (uniformWeights hp) = uniformWeights hp

Uniform weights are fixed by every relabeling.

theorem NRR.FoxNeuwirth.coordinateMean_weights (p : ℕ) (w : FoxNeuwirthWeights p) : (coordinateMean p) ↑w = 1 / ↑p

Mean of any point of the standard simplex.

noncomputable def NRR.FoxNeuwirth.referenceZeroRepresentative {p : ℕ} (hp : Nat.Prime p) : FoxNeuwirthTopCellModelPoint p

Distinguished reference zero in the identity top cell.

Equations

• NRR.FoxNeuwirth.referenceZeroRepresentative hp = (NRR.FoxNeuwirthTopCell.identity p, NRR.FoxNeuwirth.uniformWeights hp)

theorem NRR.FoxNeuwirth.reference_eq_zero_iff_weights_eq_uniform {p : ℕ} (hp : Nat.Prime p) (z : FoxNeuwirthTopCellModelPoint p) : FoxNeuwirthTopCellModelPoint.reference hp z = 0 ↔ z.2 = uniformWeights hp

The reference map vanishes exactly at uniform weights.

def NRR.FoxNeuwirth.relabelPoint {p : ℕ} (sigma : Equiv.Perm (Fin p)) (z : FoxNeuwirthTopCellModelPoint p) : FoxNeuwirthTopCellModelPoint p

Relabel a top-cell model point by an arbitrary permutation.

Equations

• NRR.FoxNeuwirth.relabelPoint sigma z = (NRR.FoxNeuwirthTopCell.relabel sigma z.1, NRR.FoxNeuwirthWeights.relabel sigma z.2)

theorem NRR.FoxNeuwirth.reference_relabelPoint_zero {p : ℕ} (hp : Nat.Prime p) (sigma : Equiv.Perm (Fin p)) : FoxNeuwirthTopCellModelPoint.reference hp (relabelPoint sigma (referenceZeroRepresentative hp)) = 0

The distinguished zero remains a zero after arbitrary relabeling.

theorem NRR.FoxNeuwirth.reference_zero_in_full_permutation_orbit {p : ℕ} (hp : Nat.Prime p) (z : FoxNeuwirthTopCellModelPoint p) (hz : FoxNeuwirthTopCellModelPoint.reference hp z = 0) : ∃ (sigma : Equiv.Perm (Fin p)), z = relabelPoint sigma (referenceZeroRepresentative hp)

Every reference zero is in the full-permutation orbit of the distinguished zero.

noncomputable def NRR.FoxNeuwirth.referenceOrbitMultiplicity (p : ℕ) : ℕ

Number of prime-symmetry orbits obtained by restricting a full permutation torsor.

Equations

• NRR.FoxNeuwirth.referenceOrbitMultiplicity p = (NRR.primeSymmetrySubgroup p).index

theorem NRR.FoxNeuwirth.referenceOrbitMultiplicity_eq_one (p : ℕ) (h2 : p = 2) : referenceOrbitMultiplicity p = 1

For two labels the selected symmetry group is the full group, so the reference zero set has one orbit.

theorem NRR.FoxNeuwirth.referenceOrbitMultiplicity_eq_two {p : ℕ} (hp : Nat.Prime p) (h2 : p ≠ 2) : referenceOrbitMultiplicity p = 2

For an odd prime the selected symmetry group is alternating, hence has index two.

noncomputable def NRR.FoxNeuwirth.referenceSignedOrbitCount (p : ℕ) : ZMod p

Signed reference orbit count with local coefficient 1 on each restricted orbit.

Equations

• NRR.FoxNeuwirth.referenceSignedOrbitCount p = ↑(NRR.FoxNeuwirth.referenceOrbitMultiplicity p)

theorem NRR.FoxNeuwirth.referenceSignedOrbitCount_ne_zero {p : ℕ} (hp : Nat.Prime p) : referenceSignedOrbitCount p ≠ 0

The signed reference orbit count is nonzero modulo p.