Simplicial chains on the Fox--Neuwirth order complex

This module defines simplicial chains on the order complex. Chains are finite coefficient functions on the strict-chain simplices from OrderComplex. The simplicial boundary is defined by deleting one vertex with the usual alternating sign. The construction is deliberately concrete: all sums are over finite Fintype indices, so later cancellation arguments reduce to finite algebra.

The file also defines the first genuine Fox--Neuwirth top chain on maximal flags. Its coefficient is the product of the signed cellular incidences along consecutive vertices of the flag, reduced modulo the prime. Its simplicial boundary is expressed as an actual chain on the glued realization and is handled by the boundary-cancellation theorems.

def NRR.FoxNeuwirthOrderComplex.FaceMap.delete {d : ℕ} (k : Fin (d + 2)) : FaceMap d (d + 1)

The coface map that omits vertex k.

Equations

• NRR.FoxNeuwirthOrderComplex.FaceMap.delete k = { toFun := k.succAbove, strictMono := ⋯ }

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.FaceMap.delete_apply {d : ℕ} (k : Fin (d + 2)) (i : Fin (d + 1)) : (delete k).toFun i = k.succAbove i

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.SimplicialChain (R : Type u_1) (p d : ℕ) : Type u_1

Degree-d simplicial chains with coefficients in R. Since the simplex type is finite, an ordinary function is already finitely supported.

Equations

• NRR.FoxNeuwirthOrderComplex.SimplicialChain R p d = (NRR.FoxNeuwirthOrderComplex.Simplex p d → R)

def NRR.FoxNeuwirthOrderComplex.SimplicialChain.faceSign {d : ℕ} {R : Type u_1} [CommRing R] (k : Fin (d + 2)) : R

The alternating sign of the face obtained by deleting vertex k.

Equations

• NRR.FoxNeuwirthOrderComplex.SimplicialChain.faceSign k = (-1) ^ ↑k

noncomputable def NRR.FoxNeuwirthOrderComplex.SimplicialChain.faceContribution {p d : ℕ} {R : Type u_1} [CommRing R] (chain : SimplicialChain R p (d + 1)) (target : Simplex p d) (source : Simplex p (d + 1)) (k : Fin (d + 2)) : R

Coefficient contributed by one simplex and one deleted vertex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.SimplicialChain.boundary {p d : ℕ} {R : Type u_1} [CommRing R] (chain : SimplicialChain R p (d + 1)) : SimplicialChain R p d

Simplicial boundary, written as a finite double sum over source simplices and deleted vertices.

Equations

• chain.boundary target = ∑ source : NRR.FoxNeuwirthOrderComplex.Simplex p (d + 1), ∑ k : Fin (d + 2), chain.faceContribution target source k

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.boundary_apply {p d : ℕ} {R : Type u_1} [CommRing R] (chain : SimplicialChain R p (d + 1)) (target : Simplex p d) : chain.boundary target = ∑ source : Simplex p (d + 1), ∑ k : Fin (d + 2), chain.faceContribution target source k

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.boundary_zero {p d : ℕ} {R : Type u_1} [CommRing R] : boundary 0 = 0

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.boundary_add {p d : ℕ} {R : Type u_1} [CommRing R] (a b : SimplicialChain R p (d + 1)) : (a + b).boundary = a.boundary + b.boundary

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.boundary_smul {p d : ℕ} {R : Type u_1} [CommRing R] (r : R) (a : SimplicialChain R p (d + 1)) : (r • a).boundary = r • a.boundary

noncomputable def NRR.FoxNeuwirthOrderComplex.SimplicialChain.boundaryLinearMap {p d : ℕ} {R : Type u_1} [CommRing R] : SimplicialChain R p (d + 1) →ₗ[R] SimplicialChain R p d

Boundary as an R-linear map.

Equations

• NRR.FoxNeuwirthOrderComplex.SimplicialChain.boundaryLinearMap = { toFun := NRR.FoxNeuwirthOrderComplex.SimplicialChain.boundary, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NRR.FoxNeuwirthOrderComplex.SimplicialChain.single {p d : ℕ} {R : Type u_1} [CommRing R] (s : Simplex p d) : SimplicialChain R p d

Basis chain supported on one simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.SimplicialChain.single s t = if t = s then 1 else 0

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.single_self {p d : ℕ} {R : Type u_1} [CommRing R] (s : Simplex p d) : single s s = 1

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.single_apply_of_ne {p d : ℕ} {R : Type u_1} [CommRing R] {s t : Simplex p d} (h : t ≠ s) : single s t = 0

def NRR.FoxNeuwirthOrderComplex.SimplicialChain.relabel {p d : ℕ} {R : Type u_1} (sigma : Equiv.Perm (Fin p)) (chain : SimplicialChain R p d) : SimplicialChain R p d

Relabel a simplicial chain by precomposition with the inverse vertex action.

Equations

• NRR.FoxNeuwirthOrderComplex.SimplicialChain.relabel sigma chain s = chain (NRR.FoxNeuwirthOrderComplex.Simplex.relabel (Equiv.symm sigma) s)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.relabel_apply {p d : ℕ} {R : Type u_1} (sigma : Equiv.Perm (Fin p)) (chain : SimplicialChain R p d) (s : Simplex p d) : relabel sigma chain s = chain (Simplex.relabel (Equiv.symm sigma) s)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.relabel_one {p d : ℕ} {R : Type u_1} (chain : SimplicialChain R p d) : relabel 1 chain = chain

theorem NRR.FoxNeuwirthOrderComplex.SimplicialChain.relabel_mul {p d : ℕ} {R : Type u_1} (sigma tau : Equiv.Perm (Fin p)) (chain : SimplicialChain R p d) : relabel (sigma * tau) chain = relabel sigma (relabel tau chain)

Relabelling is a left action on chains.

noncomputable def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.incidenceProductCoefficient {p : ℕ} (s : Simplex p (p - 1)) : ZMod p

Auxiliary incidence-product coefficient for comparison with the determinant orientation.

The signed cellular incidence currently available in OrientedBoundary records only the product of independently chosen cell orientations. It is sufficient for the orbit-level top-facet count, but it is not the full incidence function of the barycentric subdivision. Consequently this coefficient must not be used as the simplicial fundamental chain.

Equations

• NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.incidenceProductCoefficient s = ∏ k : Fin (p - 1), ↑(NRR.FoxNeuwirth.signedIncidence (↑s k.castSucc) (↑s k.succ))

noncomputable def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.incidenceProductChain {p : ℕ} : SimplicialChain (ZMod p) p (p - 1)

Auxiliary incidence-product chain used to compare the two orientation formulas.

Equations

• NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.incidenceProductChain = NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.incidenceProductCoefficient

theorem NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.maximalIndex_eq {p : ℕ} (hp : Nat.Prime p) : p - 1 + 1 = p

Arithmetic equality identifying the maximal-simplex vertex index with Fin p.

def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.maximalIndexCast {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 1 + 1)) : Fin p

Cast a maximal-simplex index to a label index.

Equations

• NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.maximalIndexCast hp i = Fin.cast ⋯ i

def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.reducedBlockCoordinate {p : ℕ} (hp : Nat.Prime p) (c : BarredPermutation p) (i : Fin (p - 1)) : ℤ

Reduced block coordinate modulo the diagonal translation direction.

The first p - 1 labels are measured relative to the last label. This realizes the quotient ℤ^p / ℤ·(1,…,1) in explicit coordinates.

Equations

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

def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.affineBlockMatrix {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : Matrix (Fin (p - 1 + 1)) (Fin (p - 1 + 1)) ℤ

Affine coordinate matrix of a maximal strict flag.

Columns are the reduced block vectors of the p flag vertices; the final row consists of ones. Its determinant is the canonical affine orientation of that barycentric simplex.

Equations

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

def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.affineBlockDeterminant {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : ℤ

Integral affine orientation of a maximal flag. For genuine maximal Fox--Neuwirth flags this is expected to be 1 or -1; only its determinant algebra is needed for the cycle equation.

Equations

• NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.affineBlockDeterminant hp s = (NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.affineBlockMatrix hp s).det

def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.topChain {p : ℕ} (hp : Nat.Prime p) : SimplicialChain (ZMod p) p (p - 1)

Fox--Neuwirth top chain on maximal flags.

The coefficient orients each barycentric simplex by its affine block-coordinate determinant.

Equations

• NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.topChain hp s = ↑(NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.affineBlockDeterminant hp s)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.topChain_apply {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) : topChain hp s = ↑(affineBlockDeterminant hp s)

theorem NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.consecutive_properFace {p : ℕ} (s : Simplex p (p - 1)) (k : Fin (p - 1)) : ProperFace (↑s k.castSucc) (↑s k.succ)

Consecutive vertices of a maximal flag are properly comparable.

noncomputable def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.topBoundary {p : ℕ} (hp : Nat.Prime p) : SimplicialChain (ZMod p) p (p - 2)

The actual determinant-chain boundary.

Equations

• NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.topBoundary hp = (⋯ ▸ NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.topChain hp).boundary

def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.IsTopCycle {p : ℕ} (hp : Nat.Prime p) : Prop

Being a cycle is the ordinary simplicial boundary equation.

Equations

• NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.IsTopCycle hp = (NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.topBoundary hp = 0)

noncomputable def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.extensionCoefficient {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) (k : Fin (p - 2 + 2)) : ZMod p

Contribution to a fixed codimension-one flag from deleting one fixed vertex position.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.topBoundary_apply_eq_sum_extensionCoefficient {p : ℕ} (hp : Nat.Prime p) (target : Simplex p (p - 2)) : topBoundary hp target = ∑ k : Fin (p - 2 + 2), extensionCoefficient hp target k

The boundary coefficient is the sum of the fixed-deletion extension coefficients.

def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.InternalExtensionCancellation {p : ℕ} (hp : Nat.Prime p) : Prop

Internal deletion positions are all positions below the terminal top-cell vertex.

Equations

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

def NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.TerminalExtensionCancellation {p : ℕ} (hp : Nat.Prime p) : Prop

Terminal deletion is the unique position that removes the top-dimensional cell.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.extensionCancellation_of_internal_terminal {p : ℕ} (hp : Nat.Prime p) (hint : InternalExtensionCancellation hp) (hterminal : TerminalExtensionCancellation hp) (target : Simplex p (p - 2)) (k : Fin (p - 2 + 2)) : extensionCoefficient hp target k = 0

The two local cancellation statements cover every deletion position.

theorem NRR.FoxNeuwirthOrderComplex.FoxNeuwirthChain.isTopCycle_of_internal_terminal {p : ℕ} (hp : Nat.Prime p) (hint : InternalExtensionCancellation hp) (hterminal : TerminalExtensionCancellation hp) : IsTopCycle hp

Local internal-diamond cancellation plus terminal prime-orbit cancellation imply that the determinant chain is a genuine cycle.