Staircase prism charts and their barycentric refinements

For a refined (p-1)-simplex, its product with the unit interval is triangulated by the standard p staircase simplices. Each staircase simplex is then allowed an independent iterated barycentric refinement. These charts are the finite domain on which the S6 PL homotopy is sampled.

def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseTime {p : ℕ} (k : Fin p) (j : Fin (p + 1)) : Fin 2

The interval coordinate attached to a staircase vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseTime k j = if ↑j ≤ ↑k then 0 else 1

def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseSpatial (p : ℕ) (k : Fin p) (j : Fin (p + 1)) : Fin p

Spatial vertex attached to a staircase vertex. Vertices k and k+1 project to the same spatial vertex and lie at the two interval endpoints.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseSpatial p k j = if h : ↑j ≤ ↑k then ⟨↑j, ⋯⟩ else ⟨↑j - 1, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseTime_lower {p : ℕ} (k : Fin p) (j : Fin (p + 1)) (h : ↑j ≤ ↑k) : staircaseTime k j = 0

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseTime_upper {p : ℕ} (k : Fin p) (j : Fin (p + 1)) (h : ↑k < ↑j) : staircaseTime k j = 1

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.spatialWeight {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (w : StandardSimplex p) (i : Fin (p - 1 + 1)) : ℝ

Spatial barycentric coordinate induced by one staircase simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.intervalWeight {p : ℕ} (k : Fin p) (w : StandardSimplex p) : ℝ

The staircase interval coordinate.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.intervalWeight k w = ∑ j : Fin (p + 1), if NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseTime k j = 1 then ↑w j else 0

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.spatialPoint {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (w : StandardSimplex p) : StandardSimplex (p - 1)

The spatial weights form a standard (p-1)-simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.spatialPoint hp k w = ⟨NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.spatialWeight hp k w, ⋯⟩

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.intervalPoint {p : ℕ} (k : Fin p) (w : StandardSimplex p) : ↑(Set.Icc 0 1)

The interval weight lies in the unit interval.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.intervalPoint k w = ⟨NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.intervalWeight k w, ⋯⟩

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircasePoint {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (w : StandardSimplex p) : StandardSimplex (p - 1) × ↑(Set.Icc 0 1)

One staircase chart from the p-simplex to Δ^(p-1) × I.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.BasePrismCell {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : Type

A base prism cell over one spatial refined top simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.BasePrismCell hp N = (NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.TopCell hp N × Fin p)

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.PrismRefinementWord (p L : ℕ) : Type

A word indexing a further barycentric refinement of a p-dimensional prism simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.PrismRefinementWord p L = (Fin L → Equiv.Perm (Fin (p + 1)))

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.PrismCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

A fully refined prism cell.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.instFintypePrismCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (PrismCell hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.instFintypePrismCell hp N L = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.instDecidableEqPrismCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : DecidableEq (PrismCell hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.instDecidableEqPrismCell hp N L = inferInstance

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.chart {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : PrismCell hp N L) : C(↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p), Realization p × ↑(Set.Icc 0 1))

Refined prism chart into the realization cylinder.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.vertex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : PrismCell hp N L) (i : Fin (p + 1)) : Realization p × ↑(Set.Icc 0 1)

Vertices of a refined prism cell.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.vertex hp N L q i = (NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.chart hp N L q) (SphereOddDegree.FiniteSimplex.vertex i)

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseSign {p : ℕ} (k : Fin p) : ℤ

Orientation sign of a staircase simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseSign k = (-1) ^ ↑k

noncomputable def NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.prismSign {p N L : ℕ} {hp : Nat.Prime p} (q : PrismCell hp N L) : ℤ

Orientation sign of a fully refined prism simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.prismSign q = NRR.FoxNeuwirthOrderComplex.SubdivisionPrismCharts.staircaseSign q.1.2 * ∏ r : Fin L, ↑(Equiv.Perm.sign (q.2 r))