Barycentric subdivision charts for the Fox--Neuwirth order complex

This module connects the compact global order-complex realization to the affine barycentric-subdivision infrastructure already developed in the sphere-degree part of the repository.

A strict chain s : Simplex p d gives a canonical affine chart from the standard simplex into the global barycentric carrier. Precomposing this chart with an iterated affine subdivision map gives the refined simplex charts used in the S6 approximation theorem.

def NRR.FoxNeuwirthOrderComplex.StandardSimplex.toDelta {d : ℕ} (w : StandardSimplex d) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)

The project standard simplex and Mathlib's topological standard simplex have the same coordinate predicate.

Equations

• NRR.FoxNeuwirthOrderComplex.StandardSimplex.toDelta w = ⟨↑w, ⋯⟩

def NRR.FoxNeuwirthOrderComplex.StandardSimplex.ofDelta {d : ℕ} (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) : StandardSimplex d

Conversion back from the topological standard simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.StandardSimplex.ofDelta w = ⟨↑w, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.StandardSimplex.ofDelta_toDelta {d : ℕ} (w : StandardSimplex d) : ofDelta (toDelta w) = w

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.StandardSimplex.toDelta_ofDelta {d : ℕ} (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) : toDelta (ofDelta w) = w

def NRR.FoxNeuwirthOrderComplex.StandardSimplex.equivDelta {d : ℕ} : StandardSimplex d ≃ ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)

Canonical equivalence between the two simplex presentations.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.Simplex.chartWeight {p d : ℕ} (s : Simplex p d) (w : StandardSimplex d) (c : BarredPermutation p) : ℝ

Coordinate weight of a point in the affine chart of a strict chain.

Equations

• s.chartWeight w c = ∑ i : Fin (d + 1), if ↑s i = c then ↑w i else 0

theorem NRR.FoxNeuwirthOrderComplex.Simplex.exists_vertex_of_chartWeight_ne_zero {p d : ℕ} (s : Simplex p d) (w : StandardSimplex d) (c : BarredPermutation p) (h : s.chartWeight w c ≠ 0) : ∃ (i : Fin (d + 1)), ↑s i = c

A nonzero chart coordinate comes from a vertex of the strict chain.

noncomputable def NRR.FoxNeuwirthOrderComplex.Simplex.realizationPoint {p d : ℕ} (s : Simplex p d) (w : StandardSimplex d) : Realization p

Affine chart of an order-complex simplex into the global barycentric realization.

Equations

• s.realizationPoint w = ⟨s.chartWeight w, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.realizationPoint_apply {p d : ℕ} (s : Simplex p d) (w : StandardSimplex d) (c : BarredPermutation p) : ↑(s.realizationPoint w) c = s.chartWeight w c

theorem NRR.FoxNeuwirthOrderComplex.Simplex.realizationPoint_vertex {p d : ℕ} (s : Simplex p d) (i : Fin (d + 1)) : s.realizationPoint (StandardSimplex.ofDelta (SphereOddDegree.FiniteSimplex.vertex i)) = Realization.vertex (↑s i)

A chart sends a standard vertex to the corresponding realization vertex.

theorem NRR.FoxNeuwirthOrderComplex.Simplex.continuous_realizationPoint {p d : ℕ} (s : Simplex p d) : Continuous s.realizationPoint

The affine chart is continuous.

noncomputable def NRR.FoxNeuwirthOrderComplex.Simplex.realizationContinuousMap {p d : ℕ} (s : Simplex p d) : C(↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d), Realization p)

Bundled continuous simplex chart.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.RefinementWord (p N : ℕ) : Type

A word indexing one affine simplex of an N-fold barycentric subdivision.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinementWord p N = (Fin N → Equiv.Perm (Fin p))

noncomputable def NRR.FoxNeuwirthOrderComplex.Simplex.refinementIndexPerm {p : ℕ} (sigma : Equiv.Perm (Fin p)) : Equiv.Perm (Fin (p - 1 + 1))

Convert a label permutation to the simplex-index permutation. For p = 0, the source permutation is vacuous and the target is the identity.

Equations

• NRR.FoxNeuwirthOrderComplex.Simplex.refinementIndexPerm sigma = if hp0 : 0 < p then have hdim := ⋯; ((Equiv.cast ⋯).trans sigma).trans (Equiv.cast ⋯) else 1

noncomputable def NRR.FoxNeuwirthOrderComplex.Simplex.refinedContinuousMap {p : ℕ} (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) : C(↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)), Realization p)

Refined chart obtained by precomposing a maximal-chain chart with an iterated affine barycentric subdivision map.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.Simplex.refinedPoint {p : ℕ} (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) (w : StandardSimplex (p - 1)) : Realization p

Pointwise form of a refined chart.

Equations

• s.refinedPoint N rho w = (s.refinedContinuousMap N rho) (NRR.FoxNeuwirthOrderComplex.StandardSimplex.toDelta w)

noncomputable def NRR.FoxNeuwirthOrderComplex.Simplex.refinedVertex {p : ℕ} (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) (i : Fin p) : Realization p

Vertices of a refined simplex.

Equations

• s.refinedVertex N rho i = (s.refinedContinuousMap N rho) (SphereOddDegree.FiniteSimplex.vertex (Fin.cast ⋯ i))

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.refinedPoint_vertex {p : ℕ} (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) (i : Fin p) : s.refinedPoint N rho (StandardSimplex.ofDelta (SphereOddDegree.FiniteSimplex.vertex (Fin.cast ⋯ i))) = s.refinedVertex N rho i

theorem NRR.FoxNeuwirthOrderComplex.Simplex.continuous_refinedPoint {p : ℕ} (s : Simplex p (p - 1)) (N : ℕ) (rho : RefinementWord p N) : Continuous (s.refinedPoint N rho)

The refined chart is continuous in barycentric coordinates.