Equivariant refined-chart carrier compatibility

This module upgrades the raw overlap theorem for refined maximal charts to symmetry-decorated occurrences. It is the exact compatibility statement needed by the endpoint-stack quotient: when two decorated refined charts represent the same global realization point, the corresponding affine interpolants of one equivariant sampling map are related by the same decorations.

def NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.maximalCoordinateIndex {p : ℕ} (i : Fin p) : Fin (p - 1 + 1)

Reindex a label by the vertex-coordinate type of a maximal simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.maximalCoordinateIndex i = Fin.cast ⋯ i

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.realizationPoint_prime_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) : (g • s).realizationPoint w = g • s.realizationPoint w

Relabelling a maximal simplex commutes with its realization chart.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.refinedPoint_prime_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) (w : StandardSimplex (p - 1)) : (g • s).refinedPoint N rho w = g • s.refinedPoint N rho w

Prime relabelling commutes with every iterated refined chart.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.refinedVertex_prime_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) (i : Fin p) : (g • s).refinedVertex N rho i = g • s.refinedVertex N rho i

Prime relabelling commutes with every represented refined vertex.

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.simplexValue {p : ℕ} (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) (F : RefinedAffineMap.ContinuousCoordinateMap p) (w : StandardSimplex (p - 1)) : Fin p → ℝ

Affine interpolation of samples of F on an arbitrary refined maximal simplex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.simplex_active_vertex_and_coefficient_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s t : Simplex p (p - 1)) (rho sigma : RefinementWord p N) (x y : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))) (h : s.refinedPoint N rho (StandardSimplex.ofDelta x) = t.refinedPoint N sigma (StandardSimplex.ofDelta y)) (i : Fin p) (hi : 0 < x (maximalCoordinateIndex i)) : s.refinedVertex N rho i = t.refinedVertex N sigma i ∧ y (maximalCoordinateIndex i) = x (maximalCoordinateIndex i)

Active refined vertices and their source coefficients are independent of the maximal chart.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.simplexValue_eq_of_refinedPoint_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s t : Simplex p (p - 1)) (rho sigma : RefinementWord p N) (F : RefinedAffineMap.ContinuousCoordinateMap p) (w v : StandardSimplex (p - 1)) (h : s.refinedPoint N rho w = t.refinedPoint N sigma v) : simplexValue s N rho F w = simplexValue t N sigma F v

Affine interpolation of globally sampled values agrees on arbitrary overlapping refined maximal charts.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.simplexValue_prime_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) (F : RefinedAffineMap.ContinuousCoordinateMap p) (hF : IsEquivariantCoordinateMap p F) (w : StandardSimplex (p - 1)) : simplexValue (g • s) N rho F w = g • simplexValue s N rho F w

Sampling an equivariant map after relabelling the whole refined simplex relabels the affine interpolant by the same prime symmetry.

theorem NRR.FoxNeuwirthOrderComplex.RefinedChartCarrierEquivariant.decorated_value_eq_of_decorated_chart_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : RefinedAffineMap.ContinuousCoordinateMap p) (hF : IsEquivariantCoordinateMap p F) (q r : RefinedAffineMap.TopCell hp N) (g h : ↥(PrimeSymmetry p)) (w v : StandardSimplex (p - 1)) (hpoint : g • (RefinedAffineMap.chart hp N q) (StandardSimplex.toDelta w) = h • (RefinedAffineMap.chart hp N r) (StandardSimplex.toDelta v)) : g • RefinedAffineMap.value hp N F q w = h • RefinedAffineMap.value hp N F r v

Symmetry-decorated refined affine values agree whenever the decorated chart points agree.