One-step relative subdivision cells over the Fox--Neuwirth cycle

This module lifts the recursive affine triangulation of Delta (p - 1) x I over every level-N refined Fox--Neuwirth top simplex. The resulting finite cell system has the exact coarse lower level N and barycentrically subdivided upper level N + 1.

The pointwise quotient-facet boundary formula is proved in the following module. Here we construct the genuine cells and prove all nondegeneracy and prime-orbit separation fields required by RelativeAffineCellSystem.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.Cell {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : Type

One global cell is a refined Fox--Neuwirth top simplex together with one cell of the recursive one-step cylinder of its standard-simplex domain.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.instFintypeCell {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : Fintype (Cell hp N)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.instFintypeCell hp N = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.instDecidableEqCell {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : DecidableEq (Cell hp N)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.instDecidableEqCell hp N = inferInstance

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.localWeight {p : ℕ} (hp : Nat.Prime p) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1 + 1))

Reinterpret a Delta p coordinate as the domain Delta ((p - 1) + 1) of the local cylinder. Primality gives 0 < p, hence (p - 1) + 1 = p.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.localWeight hp w = ⋯.mpr w

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.localPoint {p : ℕ} (hp : Nat.Prime p) (q : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) × ↑(Set.Icc 0 1)

Local recursive-cylinder point represented by a global source barycentric coordinate.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.liftPoint {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (z : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) × ↑(Set.Icc 0 1)) : EquivariantPrismVertexParameters.CylinderPoint p

Lift a local cylinder point through one refined Fox--Neuwirth chart.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.chart {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : EquivariantPrismVertexParameters.CylinderPoint p

Affine chart of one global one-step subdivision-cylinder cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.vertex {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) (i : Fin (p + 1)) : EquivariantPrismVertexParameters.CylinderPoint p

Geometric vertices are defined by restriction of the global affine chart.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.chart_vertex {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) (i : Fin (p + 1)) : chart hp N q (SphereOddDegree.FiniteSimplex.vertex i) = vertex hp N q i

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.refinedCoordinateLinear {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (c : BarredPermutation p) : (Fin (p - 1 + 1) → ℝ) →ₗ[ℝ] ℝ

One coordinate of a refined realization chart as a linear functional of its standard-simplex barycentric coordinate vector.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.refinedChart_coordinate_eq_linear {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) (c : BarredPermutation p) : ↑((RefinedAffineMap.chart hp N q) w) c = (refinedCoordinateLinear hp N q c) ↑w

Coordinate formula for the refined chart in terms of the explicit linear map above.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.refinedChart_barycentric {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) (v : Fin (p + 1) → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) (hx : ∀ (c : Fin (p - 1 + 1)), x c = ∑ i : Fin (p + 1), w i * (v i) c) (c : BarredPermutation p) : ↑((RefinedAffineMap.chart hp N q) x) c = ∑ i : Fin (p + 1), w i * ↑((RefinedAffineMap.chart hp N q) (v i)) c

A refined realization chart preserves every finite barycentric combination.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.chart_spatial_affine {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) (c : BarredPermutation p) : ↑(chart hp N q w).spatial c = ∑ i : Fin (p + 1), w i * ↑(vertex hp N q i).spatial c

The spatial component of the lifted chart is affine in the source barycentric coordinates.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.chart_time_affine {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : ↑(chart hp N q w).time = ∑ i : Fin (p + 1), w i * ↑(vertex hp N q i).time

The time component of the lifted chart is affine in the source barycentric coordinates.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.refinedChart_orbit_separated {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (x y : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) (g : ↥(PrimeSymmetry p)) (h : g • (RefinedAffineMap.chart hp N q) x = (RefinedAffineMap.chart hp N q) y) : g = 1

A prime translate of two points of the same refined spatial simplex can agree only for the identity symmetry.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.chart_injective {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) : Function.Injective (chart hp N q)

Every lifted one-step cell chart is injective.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.vertex_injective {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) : Function.Injective (vertex hp N q)

The ordered vertices of every lifted one-step cell are pairwise distinct.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.vertex_orbit_injective {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) (g : ↥(PrimeSymmetry p)) (i j : Fin (p + 1)) (h : g • vertex hp N q i = vertex hp N q j) : g = 1 ∧ i = j

No two vertices of a lifted cell lie in the same nontrivial prime orbit.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.coefficient {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : Cell hp N) : ZMod p

Coefficient of a lifted top cell: the refined orbit-cycle coefficient times the recursive one-step-cylinder orientation coefficient.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCells.cellSystem {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N (N + 1) (N + 1) 0

Explicit finite affine one-step cylinder between refinement levels N and N + 1.

Equations

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