Documentation

LeanPool.NandakumarRamanaRao.NRR.PrimePolyhedron.FoxNeuwirth.EndpointStackIteratedAffinePullback

Iterated affine-pullback endpoint stacks #

This module iterates the one-step assignment while keeping one fixed endpoint PL map as the semantic invariant. At layer k, the local formula uses K.refine k, but every decorated value still represents the original chart map K. Hence adjacent layers agree on their seam by chart compatibility, and the generic assignment-composition theorem glues them.

The lower horizontal values of the stack are the native samples of the supplied regular approximation. Reversing an upper stack therefore supplies the exact upper horizontal boundary of the final collar.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackIteratedAffinePullback.chartMap_refine_zero {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) :

K.refine 0 = K

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackIteratedAffinePullback.positiveWitness {p : ℕ} (hp : Nat.Prime p) (N k : ℕ) :

RelativeSubdivisionEndpointCollar.Witness hp N (N + (k + 1))

A nonempty forward stack with k+1 one-step layers.

Equations

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

Instances For

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackIteratedAffinePullback.oneStepAssignment_represents_base {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (K : CompatibleRefinedChartHomotopy.ChartMap hp N) (k : ℕ) :

ChartMapCollarRepresentation.Represents (RelativeSubdivisionOneStepCells.cellSystem hp (N + k)) K (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeSubdivisionOneStepCells.cellSystem hp (N + k)) (CompatibleChartMapOneStep.assignment hp (K.refine k)))

One layer using a refined representation of K still represents the original chart map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackIteratedAffinePullback.oneStep_originalPL_lowerFixed {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (s : (RelativeSubdivisionOneStepCells.cellSystem hp A.level).VertexSlot) :

↑((RelativeSubdivisionOneStepCells.cellSystem hp A.level).slotPoint s).time = 0 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeSubdivisionOneStepCells.cellSystem hp A.level) (CompatibleChartMapOneStep.assignment hp (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A)) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (RelativeSubdivisionOneStepCells.cellSystem hp A.level) s) = A.map ((RelativeSubdivisionOneStepCells.cellSystem hp A.level).slotPoint s).spatial

Exact native lower endpoint values for the first one-step layer.

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackIteratedAffinePullback.Data {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (k : ℕ) :

Complete data carried by a positive endpoint stack.

assignment : ExplicitAffineRelativeCollar.Parameters.Assignment hp (positiveWitness hp A.level k).collar.cells
The vertex assignment on the iterated collar witnessing the affine pullback.
represents : ChartMapCollarRepresentation.Represents (positiveWitness hp A.level k).collar.cells (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp (positiveWitness hp A.level k).collar.cells self.assignment)
avoidsOrigin (q : (positiveWitness hp A.level k).collar.cells.Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (positiveWitness hp A.level k).collar.cells self.assignment q).AvoidsOrigin
lowerFixed (s : (positiveWitness hp A.level k).collar.cells.VertexSlot) : ↑((positiveWitness hp A.level k).collar.cells.slotPoint s).time = 0 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (positiveWitness hp A.level k).collar.cells self.assignment (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (positiveWitness hp A.level k).collar.cells s) = A.map ((positiveWitness hp A.level k).collar.cells.slotPoint s).spatial

Instances For

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackIteratedAffinePullback.build {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (k : ℕ) :

Data hp A k

Construct the full positive stack by induction on the number of additional layers.

Equations

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

Instances For

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackIteratedAffinePullback.build_lowerFixed {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (k : ℕ) (s : (positiveWitness hp A.level k).collar.cells.VertexSlot) :

↑((positiveWitness hp A.level k).collar.cells.slotPoint s).time = 0 → ExplicitAffineRelativeCollar.Parameters.vectorValue hp (positiveWitness hp A.level k).collar.cells (build hp A k).assignment (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (positiveWitness hp A.level k).collar.cells s) = A.map ((positiveWitness hp A.level k).collar.cells.slotPoint s).spatial

A built stack starts at the exact stable endpoint samples.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackIteratedAffinePullback.reverse_build_upperFixed {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (k : ℕ) (s : (ExplicitAffineRelativeCollarReverse.reverseCells (positiveWitness hp A.level k).collar.cells).VertexSlot) :

Reversing a built stack gives exact values at its upper horizontal boundary.