One-step collar assignments from compatible affine chart maps

This module removes RegularApproximation from the one-step endpoint-stack construction. The actual invariant carried through a stack is a compatible chart map which is affine on every chart. The original endpoint PL interpolation has this property, and further subdivision preserves it.

The assignment on a one-step cylinder evaluates the chart map at the spatial point represented by that cylinder vertex. Compatibility makes the value descend to global collar vertices. Affinity identifies the local affine interpolation with evaluation of the same chart map at the spatial image of the cell, so zero-freeness is inherited without a new estimate.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.localWeight_succ {m : ℕ} (hp : Nat.Prime (m + 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (m + 1))) : RelativeSubdivisionOneStepCells.localWeight hp w = w

When the prime is written as m + 1 the reindexing of a barycentric coordinate used by the local one-step cylinder is definitionally the identity.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.ChartMap.IsAffine {p : ℕ} {hp : Nat.Prime p} {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) : Prop

A chart map is affine when its value is reconstructed from its values on the standard vertices. This orientation is convenient for rewriting local affine collar values.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.baseOriginalPLMap_isAffine {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) : ChartMap.IsAffine (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A)

The endpoint PL chart map is affine by construction.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.ChartMap.IsAffine.refine {p : ℕ} {hp : Nat.Prime p} {N : ℕ} {K : CompatibleRefinedChartHomotopy.ChartMap hp N} (hK : IsAffine K) (k : ℕ) : IsAffine (K.refine k)

Affinity is preserved when a chart map is pulled back through further barycentric subdivision.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.originalPLMap_isAffine {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (k : ℕ) : ChartMap.IsAffine (CompatibleRefinedChartHomotopy.originalPLMap hp A k)

Every representation of the original endpoint PL map at a later subdivision level is affine.

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.Cells {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N (N + 1) (N + 1) 0

The one-step cell system at the level of a compatible chart map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.localSpatialWeight {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (Cells hp N).VertexSlot) : StandardSimplex (p - 1)

Spatial coordinate, in the current top-simplex chart, represented by one local cylinder vertex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.localVector {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (s : (Cells hp N).VertexSlot) : Fin p → ℝ

Local value supplied by a compatible chart map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.decoratedVector {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (Cells hp N)) : Fin p → ℝ

Prime-decorated local value.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.decoratedVector_eq_of_coverPoint_eq {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) {a b : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (Cells hp N)} (hab : ExplicitAffineRelativeCollar.Parameters.coverPoint hp (Cells hp N) a = ExplicitAffineRelativeCollar.Parameters.coverPoint hp (Cells hp N) b) : decoratedVector hp K a = decoratedVector hp K b

Equality of represented collar vertices implies equality of decorated chart-map values.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.globalVector {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (Cells hp N) → Fin p → ℝ

Global vector obtained by quotient descent.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.globalVector_mk {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (Cells hp N)) : globalVector hp K ⟦s⟧ = decoratedVector hp K s

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.globalVector_smul {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (g : ↥(PrimeSymmetry p)) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (Cells hp N)) : globalVector hp K (g • x) = g • globalVector hp K x

The descended vector is prime-equivariant.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.assignment {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (Cells hp N)

Canonical one-step assignment associated with a compatible chart map.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.vectorValue_assignment_sample {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (s : (Cells hp N).VertexSlot) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (Cells hp N) (assignment hp K) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (Cells hp N) s) = localVector hp K s

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.affineValue_localVertexMap_assignment {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (hK : ChartMap.IsAffine K) (q : (Cells hp N).Cell) (w : StandardSimplex p) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (Cells hp N) (assignment hp K) q).affineValue w = K.value q.1 (StandardSimplex.ofDelta (RelativeSubdivisionOneStepCells.localPoint hp q.2 (StandardSimplex.toDelta w)).1)

The local affine value of a one-step assignment is evaluation of the same affine chart map at the cell's represented spatial point.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.assignment_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (hK : ChartMap.IsAffine K) (q : (Cells hp N).Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (Cells hp N) (assignment hp K) q).AvoidsOrigin

Every one-step cell avoids the origin.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.lower_sample {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (q : RefinedAffineMap.TopCell hp N) (i : Fin p) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (Cells hp N) (assignment hp K) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (Cells hp N) ((q, RelativeSubdivisionCylinderCombinatorics.lowerCell (p - 1)), i.succ)) = K.value q (StandardSimplex.ofDelta (SphereOddDegree.FiniteSimplex.vertex (Fin.cast ⋯ i)))

Lower-boundary samples are the current chart-map values at native vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleChartMapOneStep.upper_sample_refine {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (q : RefinedAffineMap.TopCell hp N) (pi : Equiv.Perm (Fin p)) (i : Fin p) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (Cells hp N) (assignment hp K) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (Cells hp N) ((q, RelativeSubdivisionCylinderCombinatorics.upperCell (p - 1) (⋯.mpr pi)), i.succ)) = (K.refine 1).value (q.1, Fin.snoc q.2 pi) (StandardSimplex.ofDelta (SphereOddDegree.FiniteSimplex.vertex (Fin.cast ⋯ i)))

Upper-boundary samples are exactly the native vertex values of the refined chart map.