The finite Fox--Neuwirth top-cell model

For a prime number p, the model in this file is a finite disjoint union of closed (p - 1)-simplices indexed by one-block barred permutations. A point consists of a top Fox--Neuwirth symbol together with barycentric coordinates indexed by the labels. The associated configuration uses the barycentric coordinate as first coordinate and the permutation rank as second coordinate. The second coordinates are pairwise distinct, so this is always a labelled configuration.

This module supplies the concrete compact equivariant configuration model required at the end of the finite model. The oriented mod-p cycle obtained by gluing boundary faces is constructed in the chain modules.

@[reducible, inline]

abbrev NRR.FoxNeuwirthTopCell (p : ℕ) : Type

One-block Fox--Neuwirth symbols, using the canonical top-cell type.

Equations

• NRR.FoxNeuwirthTopCell p = NRR.BarredPermutation.TopCell p

def NRR.FoxNeuwirthTopCell.identity (p : ℕ) : FoxNeuwirthTopCell p

The identity order with no bars.

Equations

• NRR.FoxNeuwirthTopCell.identity p = ⟨{ rank := 1, bars := ∅ }, ⋯⟩

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

@[instance_reducible]

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

Equations

• NRR.FoxNeuwirthTopCell.instMetricSpace = MetricSpace.induced (fun (c : NRR.FoxNeuwirthTopCell p) => ↑((Fintype.equivFin (NRR.FoxNeuwirthTopCell p)) c)) ⋯ inferInstance

def NRR.FoxNeuwirthTopCell.relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : FoxNeuwirthTopCell p) : FoxNeuwirthTopCell p

Relabelling preserves the one-block condition.

Equations

• NRR.FoxNeuwirthTopCell.relabel σ c = ⟨NRR.BarredPermutation.relabel σ ↑c, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthTopCell.relabel_val {p : ℕ} (σ : Equiv.Perm (Fin p)) (c : FoxNeuwirthTopCell p) : ↑(relabel σ c) = BarredPermutation.relabel σ ↑c

@[simp]

theorem NRR.FoxNeuwirthTopCell.relabel_one {p : ℕ} (c : FoxNeuwirthTopCell p) : relabel 1 c = c

theorem NRR.FoxNeuwirthTopCell.relabel_mul {p : ℕ} (σ τ : Equiv.Perm (Fin p)) (c : FoxNeuwirthTopCell p) : relabel (σ * τ) c = relabel σ (relabel τ c)

@[simp]

theorem NRR.FoxNeuwirthTopCell.prime_smul_val (p : ℕ) (g : ↥(PrimeSymmetry p)) (c : FoxNeuwirthTopCell p) : ↑(g • c) = BarredPermutation.relabel ((PrimeSymmetry.toPerm p) g) ↑c

def NRR.FoxNeuwirthWeights (p : ℕ) : Type

Barycentric coordinates on a top-dimensional Fox--Neuwirth cell.

Equations

• NRR.FoxNeuwirthWeights p = ↑(SphereOddDegree.finiteSimplex ℝ (Fin p))

@[instance_reducible]

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

Equations

• NRR.FoxNeuwirthWeights.instMetricSpace = MetricSpace.induced Subtype.val ⋯ inferInstance

@[instance_reducible]

instance NRR.FoxNeuwirthWeights.instCoeFunForallFinReal {p : ℕ} : CoeFun (FoxNeuwirthWeights p) fun (x : FoxNeuwirthWeights p) => Fin p → ℝ

Equations

• NRR.FoxNeuwirthWeights.instCoeFunForallFinReal = { coe := fun (w : NRR.FoxNeuwirthWeights p) => ↑w }

@[simp]

theorem NRR.FoxNeuwirthWeights.nonneg {p : ℕ} (w : FoxNeuwirthWeights p) (i : Fin p) : 0 ≤ ↑w i

@[simp]

theorem NRR.FoxNeuwirthWeights.sum_eq_one {p : ℕ} (w : FoxNeuwirthWeights p) : ∑ i : Fin p, ↑w i = 1

def NRR.FoxNeuwirthWeights.relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) (w : FoxNeuwirthWeights p) : FoxNeuwirthWeights p

Relabel barycentric coordinates by the established σ.symm convention.

Equations

• NRR.FoxNeuwirthWeights.relabel σ w = ⟨fun (i : Fin p) => ↑w ((Equiv.symm σ) i), ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthWeights.relabel_apply {p : ℕ} (σ : Equiv.Perm (Fin p)) (w : FoxNeuwirthWeights p) (i : Fin p) : ↑(relabel σ w) i = ↑w ((Equiv.symm σ) i)

@[simp]

theorem NRR.FoxNeuwirthWeights.relabel_one {p : ℕ} (w : FoxNeuwirthWeights p) : relabel 1 w = w

theorem NRR.FoxNeuwirthWeights.relabel_mul {p : ℕ} (σ τ : Equiv.Perm (Fin p)) (w : FoxNeuwirthWeights p) : relabel (σ * τ) w = relabel σ (relabel τ w)

@[instance_reducible]

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

Equations

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

@[simp]

theorem NRR.FoxNeuwirthWeights.prime_smul_apply (p : ℕ) (g : ↥(PrimeSymmetry p)) (w : FoxNeuwirthWeights p) (i : Fin p) : ↑(g • w) i = ↑w ((Equiv.symm ((PrimeSymmetry.toPerm p) g)) i)

theorem NRR.FoxNeuwirthWeights.continuous_relabel {p : ℕ} (σ : Equiv.Perm (Fin p)) : Continuous fun (w : FoxNeuwirthWeights p) => relabel σ w

Coordinate relabelling is continuous.

def NRR.FoxNeuwirthTopCellModelPoint (p : ℕ) : Type

Concrete finite polyhedron used as the prime configuration model.

Equations

• NRR.FoxNeuwirthTopCellModelPoint p = (NRR.FoxNeuwirthTopCell p × NRR.FoxNeuwirthWeights p)

instance NRR.FoxNeuwirthTopCellModelPoint.instCompactSpaceFoxNeuwirthWeights {p : ℕ} : CompactSpace (FoxNeuwirthWeights p)

instance NRR.FoxNeuwirthTopCellModelPoint.instCompactSpaceFoxNeuwirthTopCell {p : ℕ} : CompactSpace (FoxNeuwirthTopCell p)

@[instance_reducible]

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

Equations

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

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

theorem NRR.FoxNeuwirthTopCellModelPoint.nonempty {p : ℕ} (hp : Nat.Prime p) : Nonempty (FoxNeuwirthTopCellModelPoint p)

@[instance_reducible]

instance NRR.FoxNeuwirthTopCellModelPoint.instMulActionSubtypePermFinMemSubgroupPrimeSymmetry (p : ℕ) : MulAction (↥(PrimeSymmetry p)) (FoxNeuwirthTopCellModelPoint p)

Equations

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

noncomputable def NRR.FoxNeuwirthTopCellModelPoint.site {p : ℕ} (z : FoxNeuwirthTopCellModelPoint p) (i : Fin p) : E2

The labelled point associated with a top-cell symbol and barycentric coordinates.

Equations

• z.site i = !₂[↑z.2 i, ↑↑((↑z.1).rank i)]

@[simp]

theorem NRR.FoxNeuwirthTopCellModelPoint.site_x {p : ℕ} (z : FoxNeuwirthTopCellModelPoint p) (i : Fin p) : (z.site i).ofLp 0 = ↑z.2 i

@[simp]

theorem NRR.FoxNeuwirthTopCellModelPoint.site_y {p : ℕ} (z : FoxNeuwirthTopCellModelPoint p) (i : Fin p) : (z.site i).ofLp 1 = ↑↑((↑z.1).rank i)

theorem NRR.FoxNeuwirthTopCellModelPoint.site_injective {p : ℕ} (z : FoxNeuwirthTopCellModelPoint p) : Function.Injective z.site

The second coordinate records the permutation rank, hence the site map is injective.

noncomputable def NRR.FoxNeuwirthTopCellModelPoint.toConfig {p : ℕ} (z : FoxNeuwirthTopCellModelPoint p) : Config p

Embedded labelled configuration.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthTopCellModelPoint.toConfig_pts {p : ℕ} (z : FoxNeuwirthTopCellModelPoint p) (i : Fin p) : z.toConfig.pts i = z.site i

theorem NRR.FoxNeuwirthTopCellModelPoint.toConfig_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (z : FoxNeuwirthTopCellModelPoint p) : (g • z).toConfig = g • z.toConfig

Relabelling the model point relabels its configuration.

theorem NRR.FoxNeuwirthTopCellModelPoint.continuous_toConfig {p : ℕ} : Continuous toConfig

The configuration map is continuous.

noncomputable def NRR.FoxNeuwirthTopCellModelPoint.reference {p : ℕ} (hp : Nat.Prime p) (z : FoxNeuwirthTopCellModelPoint p) : ZeroSum p

Equivariant reference map: first-coordinate vector with its diagonal part removed.

Equations

• NRR.FoxNeuwirthTopCellModelPoint.reference hp z = (NRR.coordinateDeviation ⋯) ↑z.2

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

The reference map is continuous.

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

The reference map is equivariant.

theorem NRR.FoxNeuwirthTopCellModelPoint.continuous_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) : Continuous fun (z : FoxNeuwirthTopCellModelPoint p) => g • z

Group actions on the finite-cell model are continuous.

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

The concrete compact equivariant model produced by the Fox--Neuwirth top-cell atlas.

Equations

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

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

The construction gives a concrete compact prime configuration model for every prime.