The top two terms of the Fox--Neuwirth cellular incidence complex

The obstruction argument only uses the incidence map from top cells to codimension-one cells. It does not require a cellular differential in every lower degree. This distinction matters: FoxNeuwirth.signedIncidence is the orientation convention used for the top-cell cycle, but the same formula in all adjacent dimensions is not the full Fox--Neuwirth cellular differential.

This file packages the exact two-term complex needed downstream. The lower differential is the zero map, so the chain-complex identity is literal rather than an unproved assertion about lower Fox--Neuwirth incidences. The nontrivial statement is that the oriented top chain lies in the kernel of the genuine top-to-facet incidence map; this is supplied by the facet--shuffle theorem.

@[reducible, inline]

abbrev NRR.FoxNeuwirth.TopCellChain (p : ℕ) (R : Type u_2) : Type u_2

Coefficient vectors on top-dimensional Fox--Neuwirth cells.

Equations

• NRR.FoxNeuwirth.TopCellChain p R = (NRR.BarredPermutation.TopCell p → R)

@[reducible, inline]

abbrev NRR.FoxNeuwirth.FacetChain (p : ℕ) (R : Type u_2) : Type u_2

Coefficient vectors on all barred permutations. The incidence map is automatically supported in codimension one.

Equations

• NRR.FoxNeuwirth.FacetChain p R = (NRR.BarredPermutation p → R)

noncomputable def NRR.FoxNeuwirth.topIncidenceBoundary {p : ℕ} {R : Type u_1} [CommRing R] (chain : TopCellChain p R) : FacetChain p R

The genuine top-to-facet incidence map.

Equations

• NRR.FoxNeuwirth.topIncidenceBoundary chain a = ∑ c : NRR.BarredPermutation.TopCell p, ↑(NRR.FoxNeuwirth.signedIncidence a ↑c) * chain c

def NRR.FoxNeuwirth.zeroFacetBoundary {p : ℕ} {R : Type u_1} [CommRing R] (_chain : FacetChain p R) : PUnit.{0} → R

The next differential in the minimal two-term obstruction complex.

Equations

• NRR.FoxNeuwirth.zeroFacetBoundary _chain x✝ = 0

@[simp]

theorem NRR.FoxNeuwirth.zeroFacetBoundary_apply {p : ℕ} {R : Type u_1} [CommRing R] (chain : FacetChain p R) (u : PUnit.{0}) : zeroFacetBoundary chain u = 0

theorem NRR.FoxNeuwirth.zeroFacetBoundary_comp_topIncidenceBoundary {p : ℕ} {R : Type u_1} [CommRing R] (chain : TopCellChain p R) : zeroFacetBoundary (topIncidenceBoundary chain) = fun (x : PUnit.{0}) => 0

The minimal top-cell/facet incidence object is a chain complex in the only sense required by finite Stokes: the composite with the following zero differential vanishes.

noncomputable def NRR.FoxNeuwirth.orientedTopChain (p : ℕ) : TopCellChain p (ZMod p)

The oriented sum of all top cells.

Equations

• NRR.FoxNeuwirth.orientedTopChain p c = NRR.FoxNeuwirth.orientedTopCoefficient ↑c

@[simp]

theorem NRR.FoxNeuwirth.topIncidenceBoundary_orientedTopChain_apply (p : ℕ) (a : BarredPermutation p) : topIncidenceBoundary (orientedTopChain p) a = actualTopBoundaryCoefficient a

Applying the top incidence map to the oriented top chain is exactly the previously defined actual boundary coefficient.

theorem NRR.FoxNeuwirth.topIncidenceBoundary_orientedTopChain_eq_zero {p : ℕ} (hp : Nat.Prime p) : topIncidenceBoundary (orientedTopChain p) = 0

The oriented top chain is an unconditional cycle modulo every prime.