Finite equivariant parameter space for refined prism vertices

A perturbation used in the refined S6 prism argument must satisfy two compatibility conditions before any determinant or minor polynomial is considered:

• local copies of one geometric prism vertex must receive the same coordinate values;
• prime-symmetry translates must receive relabelled coordinate values.

This module builds a finite scalar parameter type on which both conditions hold by construction. First take the finite set of all symmetry translates of all local refined-prism vertex slots and identify translates which represent the same point of the realization cylinder. Then quotient the resulting point-coordinate pairs by the diagonal prime action. A real-valued function on that final orbit type reconstructs a globally shared, prime-equivariant vector value at every sampled prism vertex.

The zero-free homotopy itself determines the distinguished base assignment in this parameter space. Later genericity modules only need to define their determinant and codimension-two polynomials on this finite type.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint (p : ℕ) : Type

The realization cylinder, bundled so that prime symmetry acts only on the spatial coordinate.

• spatial : Realization p

  The spatial point in the order-complex realization.

• time : ↑(Set.Icc 0 1)

  The time coordinate in the closed unit interval.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.ofProd {p : ℕ} (z : Realization p × ↑(Set.Icc 0 1)) : CylinderPoint p

Convert the product representation used by the homotopy and prism charts.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.ofProd z = { spatial := z.1, time := z.2 }

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.toProd {p : ℕ} (z : CylinderPoint p) : Realization p × ↑(Set.Icc 0 1)

Convert back to the product representation used by the homotopy.

Equations

• z.toProd = (z.spatial, z.time)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.toProd_ofProd {p : ℕ} (z : Realization p × ↑(Set.Icc 0 1)) : (ofProd z).toProd = z

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.ofProd_toProd {p : ℕ} (z : CylinderPoint p) : ofProd z.toProd = z

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.instMulActionSubtypePermFinMemSubgroupPrimeSymmetry (p : ℕ) : MulAction (↥(PrimeSymmetry p)) (CylinderPoint p)

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.smul_spatial (p : ℕ) (g : ↥(PrimeSymmetry p)) (z : CylinderPoint p) : (g • z).spatial = g • z.spatial

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.smul_time (p : ℕ) (g : ↥(PrimeSymmetry p)) (z : CylinderPoint p) : (g • z).time = z.time

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CylinderPoint.toProd_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (z : CylinderPoint p) : (g • z).toProd = (g • z.spatial, z.time)

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.VertexSlot {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

One local vertex occurrence in the fully refined prism triangulation.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.VertexSlot hp N L = (NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.PrismCell hp N L × Fin (p + 1))

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.instFintypeVertexSlot {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (VertexSlot hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.instFintypeVertexSlot hp N L = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.instDecidableEqVertexSlot {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : DecidableEq (VertexSlot hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.instDecidableEqVertexSlot hp N L = inferInstance

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.slotPoint {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : VertexSlot hp N L) : CylinderPoint p

A local prism vertex occurrence as an actual point of the realization cylinder.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CoverVertexSlot {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

Add a symmetry element to a local vertex occurrence. This finite covering type contains all prime translates of the selected quotient-cell representatives.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.CoverVertexSlot hp N L = (↥(NRR.PrimeSymmetry p) × NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.VertexSlot hp N L)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.instFintypeCoverVertexSlot {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (CoverVertexSlot hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.instFintypeCoverVertexSlot hp N L = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.instDecidableEqCoverVertexSlot {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : DecidableEq (CoverVertexSlot hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.instDecidableEqCoverVertexSlot hp N L = inferInstance

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.coverPoint {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : CoverVertexSlot hp N L) : CylinderPoint p

Geometric point represented by one symmetry-decorated local vertex occurrence.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.coverPoint hp N L s = s.1 • NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.slotPoint hp N L s.2

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.coverVertexSetoid {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Setoid (CoverVertexSlot hp N L)

Two decorated local slots represent the same global sampled vertex when their cylinder points are equal.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.GlobalVertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

Finite global sampled vertices of the prism, after identifying all local copies of one geometric point.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.GlobalVertex hp N L = Quotient (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.coverVertexSetoid hp N L)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalVertexFintype {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (GlobalVertex hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalVertexFintype hp N L = Fintype.ofFinite (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.GlobalVertex hp N L)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalVertexDecidableEq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : DecidableEq (GlobalVertex hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalVertexDecidableEq hp N L = Classical.decEq (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.GlobalVertex hp N L)

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.actCoverVertex {p N L : ℕ} {hp : Nat.Prime p} (g : ↥(PrimeSymmetry p)) (s : CoverVertexSlot hp N L) : CoverVertexSlot hp N L

Left multiplication on the symmetry decoration.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.actCoverVertex g s = (g * s.1, s.2)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.coverPoint_actCoverVertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (g : ↥(PrimeSymmetry p)) (s : CoverVertexSlot hp N L) : coverPoint hp N L (actCoverVertex g s) = g • coverPoint hp N L s

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalVertexAction {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : MulAction (↥(PrimeSymmetry p)) (GlobalVertex hp N L)

Prime symmetry acts on global sampled vertices.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : GlobalVertex hp N L → CylinderPoint p

Actual cylinder point represented by a global sampled vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint hp N L = Quotient.lift (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.coverPoint hp N L) ⋯

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint_mk {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : CoverVertexSlot hp N L) : globalPoint hp N L ⟦s⟧ = coverPoint hp N L s

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint_smul {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex hp N L) : globalPoint hp N L (g • x) = g • globalPoint hp N L x

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.sampleVertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : VertexSlot hp N L) : GlobalVertex hp N L

The global sampled vertex represented by an undecorated local slot.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.sampleVertex hp N L s = ⟦(1, s)⟧

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint_sampleVertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : VertexSlot hp N L) : globalPoint hp N L (sampleVertex hp N L s) = slotPoint hp N L s

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.sampleVertex_eq_of_vertex_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {q q' : SubdivisionPrismCharts.PrismCell hp N L} {i i' : Fin (p + 1)} (h : SubdivisionPrismCharts.vertex hp N L q i = SubdivisionPrismCharts.vertex hp N L q' i') : sampleVertex hp N L (q, i) = sampleVertex hp N L (q', i')

Local copies of one geometric prism vertex determine the same global sampled vertex.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.ScalarSite {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

Point-coordinate pairs on which prime symmetry acts diagonally.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.ScalarSite hp N L = (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.GlobalVertex hp N L × Fin p)

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.Parameter {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

One independent real parameter per diagonal prime orbit of sampled point-coordinate pairs.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.parameterFintype {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (Parameter hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.parameterFintype hp N L = Fintype.ofFinite (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.Parameter hp N L)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.parameterDecidableEq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : DecidableEq (Parameter hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.parameterDecidableEq hp N L = Classical.decEq (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.Parameter hp N L)

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.Assignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

A global compatible equivariant assignment is an arbitrary scalar function on the finite orbit parameter type.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.Assignment hp N L = (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.Parameter hp N L → ℝ)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.scalarValue {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : Assignment hp N L) (x : GlobalVertex hp N L) (j : Fin p) : ℝ

Scalar value reconstructed at a sampled global vertex and coordinate label.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.scalarValue hp N L a x j = a ⟦(x, j)⟧

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.vectorValue {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : Assignment hp N L) (x : GlobalVertex hp N L) : Fin p → ℝ

Full coordinate vector reconstructed at a sampled global vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.vectorValue hp N L a x j = NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.scalarValue hp N L a x j

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.scalarValue_smul {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : Assignment hp N L) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex hp N L) (j : Fin p) : scalarValue hp N L a (g • x) (g • j) = scalarValue hp N L a x j

Scalar values are invariant under the diagonal action.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.vectorValue_smul {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : Assignment hp N L) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex hp N L) : vectorValue hp N L a (g • x) = g • vectorValue hp N L a x

Every parameter assignment reconstructs a prime-equivariant vector assignment.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.localVertexValue {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) : Fin p → ℝ

Vector value attached to one local prism vertex occurrence.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.localVertexValue_eq_of_vertex_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : Assignment hp N L) {q q' : SubdivisionPrismCharts.PrismCell hp N L} {i i' : Fin (p + 1)} (h : SubdivisionPrismCharts.vertex hp N L q i = SubdivisionPrismCharts.vertex hp N L q' i') : localVertexValue hp N L a q i = localVertexValue hp N L a q' i'

Shared geometric prism vertices receive identical local vector values.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.homotopySiteValue {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (s : ScalarSite hp N L) : ℝ

The scalar function on sites obtained by sampling an equivariant zero-free homotopy.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.homotopySiteValue hp N L H s = H.map (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.globalPoint hp N L s.1).toProd s.2

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.homotopySiteValue_eq_of_orbitRel {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) {a b : ScalarSite hp N L} (hab : (MulAction.orbitRel (↥(PrimeSymmetry p)) (ScalarSite hp N L)) a b) : homotopySiteValue hp N L H a = homotopySiteValue hp N L H b

Homotopy samples are constant on diagonal prime orbits.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.homotopyAssignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) : Assignment hp N L

Distinguished parameter assignment given by the original homotopy values at sampled vertices.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.vectorValue_homotopyAssignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (x : GlobalVertex hp N L) : vectorValue hp N L (homotopyAssignment hp N L H) x = H.map (globalPoint hp N L x).toProd

Reconstructing the homotopy assignment gives the original homotopy value at every sampled global vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.localVertexValue_homotopyAssignment {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) : localVertexValue hp N L (homotopyAssignment hp N L H) q i = H.map (SubdivisionPrismCharts.vertex hp N L q i)

On each local refined-prism vertex, the distinguished assignment is exactly the original homotopy sample.