Affine-coordinate formulas for refined staircase prisms

The refined staircase chart is assembled from linear barycentric-subdivision maps, the linear staircase spatial/time maps, and the linear realization chart of one strict Fox--Neuwirth simplex. This module packages that observation as explicit linear maps and proves that every chart coordinate is the barycentric interpolation of its values at the p + 1 vertices.

These formulas are used by the concrete common-level middle-prism constructor for the explicit relative collar.

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.staircaseSpatialLinear (p : ℕ) (k : Fin p) : (Fin (p + 1) → ℝ) →ₗ[ℝ] Fin p → ℝ

The staircase spatial-coordinate map, extended linearly to all coordinate vectors.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.staircaseTimeLinear {p : ℕ} (k : Fin p) : (Fin (p + 1) → ℝ) →ₗ[ℝ] ℝ

The staircase interval-coordinate map, extended linearly to all coordinate vectors.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.maximalCoordinateReindexLinear {p : ℕ} (hp : Nat.Prime p) : (Fin p → ℝ) →ₗ[ℝ] Fin (p - 1 + 1) → ℝ

Reindex maximal-simplex coordinate vectors along p - 1 + 1 = p.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.maximalCoordinateReindexLinear hp = { toFun := fun (u : Fin p → ℝ) (i : Fin (p - 1 + 1)) => u (Fin.cast ⋯ i), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.realizationCoordinateLinear {p : ℕ} (s : Simplex p (p - 1)) (c : BarredPermutation p) : (Fin (p - 1 + 1) → ℝ) →ₗ[ℝ] ℝ

One coordinate of the realization chart of a strict simplex, as a linear functional of its barycentric coordinates.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.linearMap_apply_eq_sum_vertices {n : ℕ} {E : Type} [AddCommMonoid E] [Module ℝ E] (f : (Fin (n + 1) → ℝ) →ₗ[ℝ] E) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : f ↑w = ∑ i : Fin (n + 1), w i • f (SphereOddDegree.BarycentricSubdivisionDiameter.stdVerts n i)

A linear map on barycentric coordinate vectors is determined by its values on the standard vertices.

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.prismSpatialCoordinateLinear {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (c : BarredPermutation p) : (Fin (p + 1) → ℝ) →ₗ[ℝ] ℝ

Linear functional computing one spatial realization coordinate of a fully refined prism chart.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.prismTimeCoordinateLinear {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) : (Fin (p + 1) → ℝ) →ₗ[ℝ] ℝ

Linear functional computing the interval coordinate of a fully refined prism chart.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.chart_spatial_eq_linear {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) (c : BarredPermutation p) : ↑((SubdivisionPrismCharts.chart hp N L q) w).1 c = (prismSpatialCoordinateLinear hp N L q c) ↑w

The spatial coordinate of the refined prism chart is the corresponding explicit linear functional of the source barycentric coordinate vector.

theorem NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.chart_time_eq_linear {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : ↑((SubdivisionPrismCharts.chart hp N L q) w).2 = (prismTimeCoordinateLinear hp N L q) ↑w

The interval coordinate of the refined prism chart is the corresponding explicit linear functional of the source barycentric coordinate vector.

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

Every spatial coordinate of the refined prism chart is the barycentric interpolation of its vertex coordinates.

theorem NRR.FoxNeuwirthOrderComplex.SubdivisionPrismAffine.chart_time_affine {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : ↑((SubdivisionPrismCharts.chart hp N L q) w).2 = ∑ i : Fin (p + 1), w i * ↑(SubdivisionPrismCharts.vertex hp N L q i).2

The interval coordinate of the refined prism chart is the barycentric interpolation of its vertex times.