Finite relative-collar cells and boundary-frozen parameters

A relative subdivision collar is stored as a singular chain. Before determinant polynomials can be restricted to its movable data, one needs a finite set of cell occurrences and one global quotient of all of their vertex-coordinate sites.

This module supplies that bridge in two stages.

• Every singular chain is represented by a finite list of scalar multiples of singular-simplex generators. Applying this to the relative collar gives a finite occurrence type.
• For a collar in the realization cylinder, all local vertex occurrences are identified by actual geometric equality and then quotiented by diagonal prime symmetry. Parameters represented by a point on either horizontal boundary are marked frozen; all remaining parameter orbits are the movable interior/side parameters.

The construction is deliberately independent of a particular generic perturbation. A base scalar assignment can be restricted relative to the boundary by replacing only values on the movable parameter subtype. Shared-vertex compatibility and prime equivariance continue to hold by construction.

The affine-cell layer upgrades the finite singular cells to explicit affine cell charts for the specific Fox--Neuwirth orbit cycle and identify their horizontal chains with the two supplied stable approximations.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.expansionValue {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (terms : List (R × SphereOddDegree.singularSimplices X n)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)

Value of a finite list of coefficient/simplex terms in the singular chain group.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.expansionValue_nil {R : Type} [CommRing R] {X : TopCat} {n : ℕ} : expansionValue [] = 0

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.expansionValue_cons {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (t : R × SphereOddDegree.singularSimplices X n) (terms : List (R × SphereOddDegree.singularSimplices X n)) : expansionValue (t :: terms) = t.1 • SphereOddDegree.AffineBarycentricSubdivision.chainGenerator R X n t.2 + expansionValue terms

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.expansionValue_append {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (a b : List (R × SphereOddDegree.singularSimplices X n)) : expansionValue (a ++ b) = expansionValue a + expansionValue b

Concatenating term lists adds the represented chains.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.scaleExpansion {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (r : R) (terms : List (R × SphereOddDegree.singularSimplices X n)) : List (R × SphereOddDegree.singularSimplices X n)

Scale every coefficient in a finite generator expansion.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.expansionValue_scaleExpansion {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (r : R) (terms : List (R × SphereOddDegree.singularSimplices X n)) : expansionValue (scaleExpansion r terms) = r • expansionValue terms

Scaling all coefficients scales the represented chain.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.FiniteChainRealization {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)) : Type

A proof-carrying finite generator representation of a singular chain.

• terms : List (R × SphereOddDegree.singularSimplices X n)

  A finite list of coefficient–simplex terms representing the singular chain.

• value_eq : expansionValue self.terms = c

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.exists_finiteChainRealization {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)) : Nonempty (FiniteChainRealization c)

Every singular chain has finite support in the singular-simplex generators.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.finiteChainRealization {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)) : FiniteChainRealization c

A chosen finite generator representation of a singular chain.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.finiteChainRealization c = Classical.choice ⋯

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.FiniteChainRealization.Occurrence {R : Type} [CommRing R] {X : TopCat} {n : ℕ} {c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)} (S : FiniteChainRealization c) : Type

Finite occurrence type of the terms in a chain realization.

Equations

• S.Occurrence = Fin S.terms.length

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.FiniteChainRealization.coefficient {R : Type} [CommRing R] {X : TopCat} {n : ℕ} {c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)} (S : FiniteChainRealization c) (i : S.Occurrence) : R

Coefficient of a finite chain occurrence.

Equations

• S.coefficient i = (S.terms.get i).1

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.FiniteChainRealization.simplex {R : Type} [CommRing R] {X : TopCat} {n : ℕ} {c : ↑(SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n)} (S : FiniteChainRealization c) (i : S.Occurrence) : SphereOddDegree.singularSimplices X n

Singular simplex carried by a finite chain occurrence.

Equations

• S.simplex i = (S.terms.get i).2

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.RelativeSubdivisionBoundary.collarRealization {R : Type} [CommRing R] {X : TopCat} {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary R X n) : FiniteChainRealization B.collarChain

Chosen finite support of the relative collar chain.

Equations

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

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.RelativeCylinder (p : ℕ) : TopCat

The topological realization cylinder used by the relative affine cobordism.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.RelativeCylinder p = ↧(NRR.FoxNeuwirthOrderComplex.Realization p × ↑(Set.Icc 0 1))

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.IsAffineCylinderSimplex {p n : ℕ} (σ : SphereOddDegree.singularSimplices (RelativeCylinder p) n) : Prop

A singular cylinder simplex is affine when every spatial barycentric coordinate and its time coordinate are the barycentric interpolation of their values at the simplex vertices.

Equations

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

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.CollarSupport {n : ℕ} (p : ℕ) (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : FiniteChainRealization B.collarChain

Chosen finite singular-cell support of a relative cylinder collar.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.VertexSlot {n : ℕ} (p : ℕ) (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

One vertex occurrence of one singular (n+1)-simplex in the finite collar support.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.vertexSlotFintype (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Fintype (VertexSlot p B)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.vertexSlotFintype p B = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.vertexSlotDecidableEq (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : DecidableEq (VertexSlot p B)

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.slotPoint (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (s : VertexSlot p B) : EquivariantPrismVertexParameters.CylinderPoint p

Geometric cylinder point at a vertex of one finite collar cell occurrence.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.CoverVertexSlot (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

Symmetry-decorated finite collar vertex occurrences.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.coverVertexSlotFintype (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Fintype (CoverVertexSlot p B)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.coverVertexSlotFintype p B = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.coverVertexSlotDecidableEq (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : DecidableEq (CoverVertexSlot p B)

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.coverPoint (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (s : CoverVertexSlot p B) : EquivariantPrismVertexParameters.CylinderPoint p

Geometric point represented by a symmetry-decorated collar vertex occurrence.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.coverVertexSetoid (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Setoid (CoverVertexSlot p B)

Decorated occurrences represent one global sampled vertex exactly when their cylinder points are equal.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.GlobalVertex (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

Finite global vertices of the relative collar support.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.globalVertexFintype (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Fintype (GlobalVertex p B)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.globalVertexDecidableEq (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : DecidableEq (GlobalVertex p B)

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.actCoverVertex (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (g : ↥(PrimeSymmetry p)) (s : CoverVertexSlot p B) : CoverVertexSlot p B

Left multiplication on the symmetry decoration.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.actCoverVertex p B g s = (g * s.1, s.2)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.coverPoint_actCoverVertex (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (g : ↥(PrimeSymmetry p)) (s : CoverVertexSlot p B) : coverPoint p B (actCoverVertex p B g s) = g • coverPoint p B s

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.globalVertexAction (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : MulAction (↥(PrimeSymmetry p)) (GlobalVertex p B)

Prime symmetry acts on the global relative-collar vertices.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.globalPoint (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : GlobalVertex p B → EquivariantPrismVertexParameters.CylinderPoint p

Actual cylinder point represented by a global relative-collar vertex.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.globalPoint_mk (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (s : CoverVertexSlot p B) : globalPoint p B ⟦s⟧ = coverPoint p B s

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.globalPoint_smul (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex p B) : globalPoint p B (g • x) = g • globalPoint p B x

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.sampleVertex (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (s : VertexSlot p B) : GlobalVertex p B

Global sampled vertex represented by an undecorated local collar slot.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.sampleVertex p B s = ⟦(1, s)⟧

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.globalPoint_sampleVertex (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (s : VertexSlot p B) : globalPoint p B (sampleVertex p B s) = slotPoint p B s

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.sampleVertex_eq_of_slotPoint_eq (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) {s t : VertexSlot p B} (h : slotPoint p B s = slotPoint p B t) : sampleVertex p B s = sampleVertex p B t

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.ScalarSite (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

Point-coordinate sites before quotienting by diagonal prime symmetry.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.Parameter (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

One scalar parameter per diagonal prime orbit of relative-collar vertex-coordinate sites.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.parameterFintype (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Fintype (Parameter p B)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.parameterDecidableEq (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : DecidableEq (Parameter p B)

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.IsHorizontalPoint {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) : Prop

A cylinder point lies on one of the two fixed horizontal boundaries.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.IsHorizontalPoint z = (↑z.time = 0 ∨ ↑z.time = 1)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.isHorizontalPoint_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (z : EquivariantPrismVertexParameters.CylinderPoint p) : IsHorizontalPoint (g • z) ↔ IsHorizontalPoint z

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.IsFrozenVertex (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (x : GlobalVertex p B) : Prop

A global relative-collar vertex lies on a fixed horizontal boundary.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.isFrozenVertex_smul (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex p B) : IsFrozenVertex p B (g • x) ↔ IsFrozenVertex p B x

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.IsFrozenParameter (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Parameter p B → Prop

Frozen status is well-defined on diagonal parameter orbits.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.FrozenParameter (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

Parameter orbits represented on the two fixed horizontal boundaries.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.MovableParameter (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

Parameter orbits represented only by movable interior or spatial-side vertices.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.frozenParameterFintype (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Fintype (FrozenParameter p B)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.movableParameterFintype (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Fintype (MovableParameter p B)

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.Assignment (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

A scalar assignment on all relative-collar parameter orbits.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.replaceMovable (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (base : Assignment p B) (move : MovableParameter p B → ℝ) : Assignment p B

Replace only movable parameter values, leaving every horizontal-boundary orbit fixed.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.replaceMovable_eq_base (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (base : Assignment p B) (move : MovableParameter p B → ℝ) {q : Parameter p B} (hq : IsFrozenParameter p B q) : replaceMovable p B base move q = base q

Relative replacement agrees with the base assignment on every frozen parameter.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.replaceMovable_eq_move (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (base : Assignment p B) (move : MovableParameter p B → ℝ) (q : MovableParameter p B) : replaceMovable p B base move ↑q = move q

Relative replacement takes the prescribed value on every movable parameter.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.FullPolynomialRing (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

Full polynomial ring before imposing the fixed-horizontal-boundary condition.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.MovablePolynomialRing (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) : Type

Polynomial ring in only the movable interior and spatial-side parameter orbits.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.relativeVariable (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (base : Assignment p B) (q : Parameter p B) : MovablePolynomialRing p B

Substitute a horizontal variable by its fixed base value and retain a movable variable as an indeterminate.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.restrictPolynomial (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (base : Assignment p B) : FullPolynomialRing p B →+* MovablePolynomialRing p B

Restriction homomorphism from all collar variables to movable variables with fixed horizontal boundary values.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.eval_relativeVariable (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (base : Assignment p B) (move : MovableParameter p B → ℝ) (q : Parameter p B) : (MvPolynomial.eval move) (relativeVariable p B base q) = replaceMovable p B base move q

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.eval_restrictPolynomial (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (base : Assignment p B) (move : MovableParameter p B → ℝ) (P : FullPolynomialRing p B) : (MvPolynomial.eval move) ((restrictPolynomial p B base) P) = (MvPolynomial.eval (replaceMovable p B base move)) P

Evaluating a restricted polynomial at movable data is the same as evaluating the original polynomial at the boundary-relative full assignment.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.scalarValue (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (a : Assignment p B) (x : GlobalVertex p B) (j : Fin p) : ℝ

Scalar value reconstructed at a global relative-collar vertex and coordinate.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.scalarValue p B a x j = a ⟦(x, j)⟧

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.vectorValue (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (a : Assignment p B) (x : GlobalVertex p B) : Fin p → ℝ

Full coordinate vector reconstructed at a global relative-collar vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.vectorValue_smul (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (a : Assignment p B) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex p B) : vectorValue p B a (g • x) = g • vectorValue p B a x

Relative-collar assignments are prime-equivariant by the diagonal orbit quotient.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.localValue_eq_of_slotPoint_eq (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (a : Assignment p B) {s t : VertexSlot p B} (h : slotPoint p B s = slotPoint p B t) : vectorValue p B a (sampleVertex p B s) = vectorValue p B a (sampleVertex p B t)

Values at geometrically equal local collar vertices agree.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionCellParameters.replaceMovable_horizontal_localValue (p : ℕ) {n : ℕ} (B : StableCollarRelativeSubdivision.RelativeSubdivisionBoundary (ZMod p) (RelativeCylinder p) n) (base : Assignment p B) (move : MovableParameter p B → ℝ) (s : VertexSlot p B) (hs : IsHorizontalPoint (slotPoint p B s)) : vectorValue p B (replaceMovable p B base move) (sampleVertex p B s) = vectorValue p B base (sampleVertex p B s)

Replacing movable parameters leaves every horizontal local vertex value unchanged.