Topological realization of the Fox--Neuwirth order complex

This file constructs the topological realization of the order complex. The global carrier introduced in OrderComplex is a closed subspace of the finite standard simplex: the additional chain-support condition is a finite intersection of unions of coordinate hyperplanes. Hence the carrier is compact.

Relabelling acts by permuting barycentric coordinates. The configuration map is the barycentric average of the canonical configurations attached to the barred-permutation vertices. Its collision-freeness is proved directly from the face order. For a realization point, choose a nonzero support cell of minimum dual dimension. That cell is a face of every other support cell. If two labels are in different blocks there, their first-coordinate order persists weakly and is strict at the chosen cell. If they are in the same block, their common block persists and their rank order persists strictly. The barycentric average therefore cannot identify the labels.

def NRR.FoxNeuwirthOrderComplex.relabelEquiv {p : ℕ} (sigma : Equiv.Perm (Fin p)) : BarredPermutation p ≃ BarredPermutation p

Relabelling is an equivalence of the finite barred-permutation vertex set.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.relabelEquiv_apply {p : ℕ} (sigma : Equiv.Perm (Fin p)) (c : BarredPermutation p) : (relabelEquiv sigma) c = BarredPermutation.relabel sigma c

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.relabel_symm_relabel {p : ℕ} (sigma : Equiv.Perm (Fin p)) (c : BarredPermutation p) : BarredPermutation.relabel (Equiv.symm sigma) (BarredPermutation.relabel sigma c) = c

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.relabel_relabel_symm {p : ℕ} (sigma : Equiv.Perm (Fin p)) (c : BarredPermutation p) : BarredPermutation.relabel sigma (BarredPermutation.relabel (Equiv.symm sigma) c) = c

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

Two vertices may simultaneously occur in a simplex exactly when they are equal or properly comparable.

Equations

• NRR.FoxNeuwirthOrderComplex.PairCompatible a b = (a = b ∨ NRR.FoxNeuwirthOrderComplex.ProperFace a b ∨ NRR.FoxNeuwirthOrderComplex.ProperFace b a)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.pairCompatibleDecidable {p : ℕ} (a b : BarredPermutation p) : Decidable (PairCompatible a b)

Equations

• NRR.FoxNeuwirthOrderComplex.pairCompatibleDecidable a b = Classical.propDecidable (NRR.FoxNeuwirthOrderComplex.PairCompatible a b)

def NRR.FoxNeuwirthOrderComplex.pairConstraint {p : ℕ} (a b : BarredPermutation p) : Set (BarredPermutation p → ℝ)

Closed coordinate condition attached to a pair of vertices. For an incompatible pair, at least one of the two barycentric coordinates must vanish.

Equations

• NRR.FoxNeuwirthOrderComplex.pairConstraint a b = {weight : NRR.BarredPermutation p → ℝ | NRR.FoxNeuwirthOrderComplex.PairCompatible a b ∨ weight a = 0 ∨ weight b = 0}

theorem NRR.FoxNeuwirthOrderComplex.isClosed_pairConstraint {p : ℕ} (a b : BarredPermutation p) : IsClosed (pairConstraint a b)

Every pair constraint is closed.

theorem NRR.FoxNeuwirthOrderComplex.chainSupported_set_eq {p : ℕ} : {weight : BarredPermutation p → ℝ | ChainSupported weight} = ⋂ (a : BarredPermutation p), ⋂ (b : BarredPermutation p), pairConstraint a b

Chain support is precisely the intersection of all pair constraints.

theorem NRR.FoxNeuwirthOrderComplex.isClosed_chainSupported {p : ℕ} : IsClosed {weight : BarredPermutation p → ℝ | ChainSupported weight}

The chain-support condition is closed in the finite coordinate space.

theorem NRR.FoxNeuwirthOrderComplex.realization_carrier_eq {p : ℕ} : {weight : BarredPermutation p → ℝ | (∀ (c : BarredPermutation p), 0 ≤ weight c) ∧ ∑ c : BarredPermutation p, weight c = 1 ∧ ChainSupported weight} = SphereOddDegree.finiteSimplex ℝ (BarredPermutation p) ∩ {weight : BarredPermutation p → ℝ | ChainSupported weight}

The underlying predicate of the realization is the intersection of the standard simplex with its closed chain-support locus.

theorem NRR.FoxNeuwirthOrderComplex.isCompact_realizationCarrier {p : ℕ} : IsCompact {weight : BarredPermutation p → ℝ | (∀ (c : BarredPermutation p), 0 ≤ weight c) ∧ ∑ c : BarredPermutation p, weight c = 1 ∧ ChainSupported weight}

Compactness of the global barycentric carrier.

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.Realization.instMetricSpace {p : ℕ} : MetricSpace (Realization p)

Equations

• NRR.FoxNeuwirthOrderComplex.Realization.instMetricSpace = MetricSpace.induced Subtype.val ⋯ inferInstance

instance NRR.FoxNeuwirthOrderComplex.Realization.instNonempty {p : ℕ} : Nonempty (Realization p)

instance NRR.FoxNeuwirthOrderComplex.Realization.instCompactSpace {p : ℕ} : CompactSpace (Realization p)

The order-complex realization is compact.

def NRR.FoxNeuwirthOrderComplex.Realization.relabel {p : ℕ} (sigma : Equiv.Perm (Fin p)) (x : Realization p) : Realization p

The coordinate permutation induced by relabelling.

Equations

• NRR.FoxNeuwirthOrderComplex.Realization.relabel sigma x = ⟨fun (c : NRR.BarredPermutation p) => ↑x (NRR.BarredPermutation.relabel (Equiv.symm sigma) c), ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Realization.relabel_apply {p : ℕ} (sigma : Equiv.Perm (Fin p)) (x : Realization p) (c : BarredPermutation p) : ↑(relabel sigma x) c = ↑x (BarredPermutation.relabel (Equiv.symm sigma) c)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Realization.relabel_one {p : ℕ} (x : Realization p) : relabel 1 x = x

theorem NRR.FoxNeuwirthOrderComplex.Realization.relabel_mul {p : ℕ} (sigma tau : Equiv.Perm (Fin p)) (x : Realization p) : relabel (sigma * tau) x = relabel sigma (relabel tau x)

Coordinate relabelling is a left action.

@[instance_reducible]

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

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Realization.prime_smul_apply (p : ℕ) (g : ↥(PrimeSymmetry p)) (x : Realization p) (c : BarredPermutation p) : ↑(g • x) c = ↑x (BarredPermutation.relabel (Equiv.symm ((PrimeSymmetry.toPerm p) g)) c)

theorem NRR.FoxNeuwirthOrderComplex.Realization.continuous_relabel {p : ℕ} (sigma : Equiv.Perm (Fin p)) : Continuous fun (x : Realization p) => relabel sigma x

Relabelling is continuous because it merely permutes finitely many coordinates.

theorem NRR.FoxNeuwirthOrderComplex.Realization.support_nonempty {p : ℕ} (x : Realization p) : x.support.Nonempty

Every realization point has a nonempty coordinate support.

theorem NRR.FoxNeuwirthOrderComplex.Realization.exists_minimal_support_cell {p : ℕ} (x : Realization p) : ∃ c ∈ x.support, ∀ d ∈ x.support, c.IsFace d

A realization support has a cell that is a face of every other support cell.

noncomputable def NRR.FoxNeuwirthOrderComplex.Realization.xCoord {p : ℕ} (x : Realization p) (i : Fin p) : ℝ

First coordinate of the barycentric configuration point.

Equations

• x.xCoord i = ∑ c : NRR.BarredPermutation p, ↑x c * ↑(c.blockIndex i)

noncomputable def NRR.FoxNeuwirthOrderComplex.Realization.yCoord {p : ℕ} (x : Realization p) (i : Fin p) : ℝ

Second coordinate of the barycentric configuration point.

Equations

• x.yCoord i = ∑ c : NRR.BarredPermutation p, ↑x c * ↑↑(c.rank i)

noncomputable def NRR.FoxNeuwirthOrderComplex.Realization.site {p : ℕ} (x : Realization p) (i : Fin p) : E2

Barycentric average of the canonical vertex configurations.

Equations

• x.site i = !₂[x.xCoord i, x.yCoord i]

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Realization.site_x {p : ℕ} (x : Realization p) (i : Fin p) : (x.site i).ofLp 0 = x.xCoord i

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Realization.site_y {p : ℕ} (x : Realization p) (i : Fin p) : (x.site i).ofLp 1 = x.yCoord i

theorem NRR.FoxNeuwirthOrderComplex.Realization.xCoord_lt_of_minimal_block_lt {p : ℕ} (x : Realization p) (c : BarredPermutation p) (hc : c ∈ x.support) (hface : ∀ d ∈ x.support, c.IsFace d) {i j : Fin p} (hij : c.blockIndex i < c.blockIndex j) : x.xCoord i < x.xCoord j

A minimal support cell forces strict first-coordinate order whenever two labels lie in separate blocks there.

theorem NRR.FoxNeuwirthOrderComplex.Realization.xCoord_eq_of_minimal_sameBlock {p : ℕ} (x : Realization p) (c : BarredPermutation p) (hface : ∀ d ∈ x.support, c.IsFace d) {i j : Fin p} (hij : c.SameBlock i j) : x.xCoord i = x.xCoord j

A minimal support cell forces equality of first coordinates whenever the labels lie in one block there.

theorem NRR.FoxNeuwirthOrderComplex.Realization.yCoord_lt_of_minimal_rank_lt {p : ℕ} (x : Realization p) (c : BarredPermutation p) (hc : c ∈ x.support) (hface : ∀ d ∈ x.support, c.IsFace d) {i j : Fin p} (hblock : c.SameBlock i j) (hij : ↑(c.rank i) < ↑(c.rank j)) : x.yCoord i < x.yCoord j

In a common minimal block, strict rank order persists through the whole support chain.

theorem NRR.FoxNeuwirthOrderComplex.Realization.site_injective {p : ℕ} (x : Realization p) : Function.Injective x.site

The barycentric site family is collision-free.

noncomputable def NRR.FoxNeuwirthOrderComplex.Realization.toConfig {p : ℕ} (x : Realization p) : Config p

The order-complex realization maps to the labelled configuration space.

Equations

• x.toConfig = ⟨x.site, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Realization.toConfig_pts {p : ℕ} (x : Realization p) (i : Fin p) : x.toConfig.pts i = x.site i

theorem NRR.FoxNeuwirthOrderComplex.Realization.continuous_xCoord {p : ℕ} (i : Fin p) : Continuous fun (x : Realization p) => x.xCoord i

The first barycentric coordinate sum is continuous.

theorem NRR.FoxNeuwirthOrderComplex.Realization.continuous_yCoord {p : ℕ} (i : Fin p) : Continuous fun (x : Realization p) => x.yCoord i

The second barycentric coordinate sum is continuous.

theorem NRR.FoxNeuwirthOrderComplex.Realization.continuous_site {p : ℕ} : Continuous fun (x : Realization p) => x.site

The barycentric site map is continuous.

theorem NRR.FoxNeuwirthOrderComplex.Realization.continuous_toConfig {p : ℕ} : Continuous toConfig

The configuration map is continuous.

theorem NRR.FoxNeuwirthOrderComplex.Realization.xCoord_relabel {p : ℕ} (sigma : Equiv.Perm (Fin p)) (x : Realization p) (i : Fin p) : (relabel sigma x).xCoord i = x.xCoord ((Equiv.symm sigma) i)

Barycentric first coordinates transform by relabelling.

theorem NRR.FoxNeuwirthOrderComplex.Realization.yCoord_relabel {p : ℕ} (sigma : Equiv.Perm (Fin p)) (x : Realization p) (i : Fin p) : (relabel sigma x).yCoord i = x.yCoord ((Equiv.symm sigma) i)

Barycentric second coordinates transform by relabelling.

theorem NRR.FoxNeuwirthOrderComplex.Realization.site_relabel {p : ℕ} (sigma : Equiv.Perm (Fin p)) (x : Realization p) (i : Fin p) : (relabel sigma x).site i = x.site ((Equiv.symm sigma) i)

The barycentric site family is equivariant under all label permutations.

theorem NRR.FoxNeuwirthOrderComplex.Realization.toConfig_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (x : Realization p) : (g • x).toConfig = g • x.toConfig

The configuration map is equivariant for the selected prime symmetry.

theorem NRR.FoxNeuwirthOrderComplex.Realization.continuous_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) : Continuous fun (x : Realization p) => g • x

Prime-symmetry actions on the realization are continuous.

theorem NRR.FoxNeuwirthOrderComplex.Realization.toConfig_vertex {p : ℕ} (c : BarredPermutation p) : (vertex c).toConfig = c.canonicalConfig

The barycentric map agrees with the canonical configuration at every order-complex vertex.

noncomputable def NRR.FoxNeuwirthOrderComplex.Realization.reference {p : ℕ} (hp : Nat.Prime p) (x : Realization p) : ZeroSum p

Reference vector obtained from the first coordinates of the barycentric configuration.

Equations

• NRR.FoxNeuwirthOrderComplex.Realization.reference hp x = (NRR.coordinateDeviation ⋯) fun (i : Fin p) => x.xCoord i

theorem NRR.FoxNeuwirthOrderComplex.Realization.continuous_reference {p : ℕ} (hp : Nat.Prime p) : Continuous (reference hp)

The reference map is continuous.

theorem NRR.FoxNeuwirthOrderComplex.Realization.reference_smul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (x : Realization p) : reference hp (g • x) = g • reference hp x

The reference vector is equivariant.

noncomputable def NRR.FoxNeuwirthOrderComplex.orderComplexModel {p : ℕ} (hp : Nat.Prime p) : PrimeConfigurationModel hp

The compact equivariant prime configuration model carried by the glued order complex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.orderComplexModel_nonempty {p : ℕ} (hp : Nat.Prime p) : Nonempty (PrimeConfigurationModel hp)

The order-complex realization produces a compact equivariant configuration model.