Affine pullback values on one endpoint-subdivision cylinder

The earlier last-vertex convention is not stable under iteration: its upper values generally do not equal the lower values selected by the next one-step layer. The composable convention is the affine pullback of the same parent PL map.

For a parent simplex with vertex data V, every local cylinder vertex has a spatial barycentric coordinate in that parent simplex. We assign to it the affine value of V at that coordinate. Affine interpolation over a cylinder cell then recovers the parent affine map at the cell's spatial point exactly. Hence origin avoidance is inherited verbatim, and upper-boundary values are the ordinary barycentric-subdivision vertex values needed by the next layer.

This file proves the complete simplex-local statement. Global iteration only needs the standard face-gluing theorem saying that the parent PL values agree on shared refined faces.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.parentIndex (p : ℕ) : Fin (p - 1 + 1) → Fin (p - 1 + 1)

The identity correspondence between parent vertex indices.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.parentIndex p = id

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.cylinderIndex {p : ℕ} (hp : Nat.Prime p) : Fin (p + 1) → Fin (p - 1 + 2)

Cast cylinder vertex indices to the dimension convention for the endpoint stack.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.cylinderIndex hp = Fin.cast ⋯

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.pullbackVertexValue {n : ℕ} (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (V : Fin (d + 1) → Fin n → ℝ) (i : Fin (d + 2)) : Fin n → ℝ

Evaluate parent-simplex affine vertex data at the spatial point of one local cylinder vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.affine_pullbackVertexValue_eq_spatial {n : ℕ} (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (V : Fin (d + 1) → Fin n → ℝ) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) : (fun (c : Fin n) => ∑ i : Fin (d + 2), w i * pullbackVertexValue d q V i c) = fun (c : Fin n) => ∑ j : Fin (d + 1), (RelativeSubdivisionCylinderCombinatorics.spatialPoint d q w) j * V j c

Interpolating the pulled-back values over a cylinder cell is exactly evaluation of the parent affine map at the spatial barycentric image of the cell point.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.pullbackVertexValue_lower {n : ℕ} (d : ℕ) (V : Fin (d + 1) → Fin n → ℝ) (i : Fin (d + 1)) : pullbackVertexValue d (RelativeSubdivisionCylinderCombinatorics.lowerCell d) V i.succ = V i

The affine-pullback convention fixes every coarse lower-boundary vertex literally.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.pullbackVertexValue_upper {n : ℕ} (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (V : Fin (d + 1) → Fin n → ℝ) (i : Fin (d + 1)) : pullbackVertexValue d (RelativeSubdivisionCylinderCombinatorics.upperCell d pi) V i.succ = fun (c : Fin n) => ∑ j : Fin (d + 1), (SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter d pi i) j * V j c

On an upper barycentric facet, affine pullback gives the parent affine value at the corresponding prefix barycenter.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.affine_pullbackEndpointValue_eq_value {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (q : RefinedAffineMap.TopCell hp A.level) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : (fun (c : Fin p) => ∑ i : Fin (p + 1), w i * pullbackVertexValue (p - 1) r (fun (j : Fin (p - 1 + 1)) => A.map (RefinedAffineMap.vertex hp A.level q (parentIndex p j))) (cylinderIndex hp i) c) = RefinedAffineMap.value hp A.level A.map q (StandardSimplex.ofDelta (RelativeSubdivisionCylinderCombinatorics.spatialPoint (p - 1) r (RelativeSubdivisionOneStepCells.localWeight hp w)))

Endpoint specialization: the local affine interpolation is exactly the stored endpoint PL value at the spatial point of the one-step cylinder cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.affine_pullbackEndpointValue_ne_zero {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (q : RefinedAffineMap.TopCell hp A.level) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : (fun (c : Fin p) => ∑ i : Fin (p + 1), w i * pullbackVertexValue (p - 1) r (fun (j : Fin (p - 1 + 1)) => A.map (RefinedAffineMap.vertex hp A.level q (parentIndex p j))) (cylinderIndex hp i) c) ≠ 0

Every affine-pullback one-step endpoint cell avoids the origin because it is an exact restriction of the already zero-free endpoint PL map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackCore.pullbackEndpointValue_upper_eq_refinedVertexValue {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (q : RefinedAffineMap.TopCell hp A.level) (pi : Equiv.Perm (Fin p)) (i : Fin p) : pullbackVertexValue (p - 1) (RelativeSubdivisionCylinderCombinatorics.upperCell (p - 1) (⋯.mpr pi)) (fun (j : Fin (p - 1 + 1)) => A.map (RefinedAffineMap.vertex hp A.level q (parentIndex p j))) (cylinderIndex hp i.succ) = RefinedAffineMap.value hp A.level A.map q (StandardSimplex.ofDelta (SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter (p - 1) (⋯.mpr pi) (Fin.cast ⋯ i)))

Upper pullback values are exactly the parent affine values at the vertices of the appended barycentric-subdivision simplex.