Carrier coordinates for maximal Fox--Neuwirth charts

Every maximal order-complex simplex is ranked by dual dimension. Consequently, if two maximal simplices share a barred-permutation vertex, that vertex occurs at the same index in both flags. This elementary rank rigidity makes overlap in the global barycentric realization coordinatewise: at every rank, either the two maximal flags have the same vertex and the two barycentric coordinates agree, or the coordinate is zero on the first chart.

These statements isolate the Fox--Neuwirth-specific part of refined chart gluing. After applying them to the outputs of two iterated affine-subdivision maps, the compatibility statement reduces to barycentric subdivisions of one standard simplex.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.simplexIndex_stageIndex {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 1 + 1)) : MaximalFlagCode.simplexIndex hp (MaximalFlagCode.stageIndex hp i) = i

The arithmetic cast from a maximal-simplex index to a stage and back is the identity.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.maximal_vertex_dualDimension_raw {p : ℕ} (hp : Nat.Prime p) (s : Simplex p (p - 1)) (i : Fin (p - 1 + 1)) : (↑s i).dualDimension = ↑(MaximalFlagCode.stageIndex hp i)

The raw maximal-simplex index records the dual dimension of its barred-permutation vertex.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.maximal_raw_index_eq_of_vertex_eq {p : ℕ} (hp : Nat.Prime p) (s t : Simplex p (p - 1)) {i j : Fin (p - 1 + 1)} (h : ↑s i = ↑t j) : i = j

Shared vertices of two maximal flags occur at the same rank.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.chartWeight_at_maximal_vertex {p : ℕ} (hp : Nat.Prime p) (s t : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) (i : Fin (p - 1 + 1)) : t.chartWeight w (↑s i) = if ↑t i = ↑s i then ↑w i else 0

In a second maximal chart, the coordinate of a vertex of the first chart is either the coordinate at the same rank or zero.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.coordinate_eq_if_vertex_eq_of_realizationPoint_eq {p : ℕ} (hp : Nat.Prime p) (s t : Simplex p (p - 1)) (w v : StandardSimplex (p - 1)) (h : s.realizationPoint w = t.realizationPoint v) (i : Fin (p - 1 + 1)) : ↑w i = if ↑t i = ↑s i then ↑v i else 0

Equality of maximal-chart realization points gives the exact coordinate relation at each ranked vertex.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.vertex_eq_and_coordinate_eq_of_ne_zero {p : ℕ} (hp : Nat.Prime p) (s t : Simplex p (p - 1)) (w v : StandardSimplex (p - 1)) (h : s.realizationPoint w = t.realizationPoint v) (i : Fin (p - 1 + 1)) (hi : ↑w i ≠ 0) : ↑t i = ↑s i ∧ ↑v i = ↑w i

A nonzero coordinate of the first chart forces the same vertex and the same coordinate in the second maximal chart.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.vertex_eq_of_mem_support {p : ℕ} (hp : Nat.Prime p) (s t : Simplex p (p - 1)) (w v : StandardSimplex (p - 1)) (h : s.realizationPoint w = t.realizationPoint v) (i : Fin (p - 1 + 1)) (hi : ↑w i ≠ 0) : ↑t i = ↑s i

The support of the first coordinate vector is contained rankwise in the common face of the two maximal flags.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.coordinate_eq_of_ne_zero {p : ℕ} (hp : Nat.Prime p) (s t : Simplex p (p - 1)) (w v : StandardSimplex (p - 1)) (h : s.realizationPoint w = t.realizationPoint v) (i : Fin (p - 1 + 1)) (hi : ↑w i ≠ 0) : ↑v i = ↑w i

On every active rank, the two maximal-chart barycentric coordinates agree.

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.maximalRefinementWord {p : ℕ} (N : ℕ) (rho : RefinementWord p N) : Fin N → Equiv.Perm (Fin (p - 1 + 1))

Transport a label-indexed refinement word to the maximal-simplex vertex index type.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.maximalRefinementWord N rho k = NRR.FoxNeuwirthOrderComplex.Simplex.refinementIndexPerm (rho k)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.maximalRefinementWord_apply {p : ℕ} (N : ℕ) (rho : RefinementWord p N) (k : Fin N) : maximalRefinementWord N rho k = Simplex.refinementIndexPerm (rho k)

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.maximal_source_eq_of_realizationPoint_eq {p : ℕ} (hp : Nat.Prime p) (s t : Simplex p (p - 1)) (w v : StandardSimplex (p - 1)) (h : s.realizationPoint w = t.realizationPoint v) : w = v

Equality of global realization points in two maximal charts forces equality of their ranked standard-simplex coordinate vectors. Ranks where the maximal flags differ have zero coordinate in both charts.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.refined_innerPoint_eq_of_chart_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q r : RefinedAffineMap.TopCell hp N) (x y : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) (h : (RefinedAffineMap.chart hp N q) x = (RefinedAffineMap.chart hp N r) y) : (SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (p - 1) N (maximalRefinementWord N q.2)) x = (SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (p - 1) N (maximalRefinementWord N r.2)) y

Equal points in two refined Fox--Neuwirth charts have equal inner standard-simplex realization coordinates.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.refined_active_vertex_and_coefficient_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q r : RefinedAffineMap.TopCell hp N) (x y : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) (h : (RefinedAffineMap.chart hp N q) x = (RefinedAffineMap.chart hp N r) y) (i : Fin (p - 1 + 1)) (hi : 0 < x i) : RefinedAffineMap.vertex hp N q i = RefinedAffineMap.vertex hp N r i ∧ y i = x i

An active refined-chart source vertex and its coefficient are independent of the chosen maximal Fox--Neuwirth chart and refinement word.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierCore.refinedAffineValue_eq_of_chart_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : RefinedAffineMap.ContinuousCoordinateMap p) (q r : RefinedAffineMap.TopCell hp N) (w v : StandardSimplex (p - 1)) (h : (RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta w) = (RefinedAffineMap.chart hp N r) (StandardSimplex.toDelta v)) : RefinedAffineMap.value hp N F q w = RefinedAffineMap.value hp N F r v

The refined affine interpolation of one global sampling map is independent of the refined chart representing the point.