Affine maps on iterated subdivisions of the Fox--Neuwirth cycle

The original S6 interface only allowed affine data on the vertices of the unrefined order complex. This module supplies the correct refined object. A refined top cell consists of an S4 top-orbit representative together with a word of barycentric-subdivision permutations. A continuous global coordinate map is sampled at the vertices of that refined simplex and extended affinely.

@[reducible, inline]

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

One top simplex of the N-fold subdivision of the prime-orbit cycle.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.TopCell hp N = (NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.TopOrbit hp × NRR.FoxNeuwirthOrderComplex.RefinementWord p N)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.instFintypeTopCell {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : Fintype (TopCell hp N)

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.instFintypeTopCell hp N = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.instDecidableEqTopCell {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : DecidableEq (TopCell hp N)

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.instDecidableEqTopCell hp N = inferInstance

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.subdivisionSign {p : ℕ} (N : ℕ) (rho : RefinementWord p N) : ZMod p

Sign of an iterated barycentric-subdivision summand.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.subdivisionSign N rho = ∏ r : Fin N, ↑↑(Equiv.Perm.sign (rho r))

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.subdivisionSignInt {p : ℕ} (N : ℕ) (rho : RefinementWord p N) : ℤ

Integer version of the subdivision sign.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.subdivisionSignInt N rho = ∏ r : Fin N, ↑(Equiv.Perm.sign (rho r))

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.ContinuousCoordinateMap (p : ℕ) : Type

Continuous coordinate maps on the global realization.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.ContinuousCoordinateMap p = C(NRR.FoxNeuwirthOrderComplex.Realization p, Fin p → ℝ)

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.chart {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : TopCell hp N) : C(↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)), Realization p)

Refined chart attached to a top-orbit representative and a subdivision word.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.chart hp N q = (NRR.FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.topRepr hp q.1).refinedContinuousMap N q.2

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.vertex {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : TopCell hp N) (i : Fin (p - 1 + 1)) : Realization p

Vertices of a refined top simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.vertexValue {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) (i : Fin (p - 1 + 1)) (j : Fin p) : ℝ

Vertex samples of a continuous coordinate map on one refined simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.vertexValue hp N F q i j = F (NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.vertex hp N q i) j

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.value {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) (w : StandardSimplex (p - 1)) : Fin p → ℝ

Affine interpolation of the sampled full coordinate vector.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.value hp N F q w j = ∑ i : Fin (p - 1 + 1), ↑w i * NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.vertexValue hp N F q i j

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.deviationVertexValue {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) (i : Fin (p - 1 + 1)) (r : Fin (p - 1)) : ℝ

Difference-coordinate vertex samples.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.augmentedMatrix {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) : Matrix (Fin (p - 1 + 1)) (Fin (p - 1 + 1)) ℝ

Augmented matrix controlling affine regularity on a refined simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.determinant {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) : ℝ

Refined-simplex determinant.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.determinant hp N F q = (NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.augmentedMatrix hp N F q).det

def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.HasPositiveInteriorZero {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) : Prop

Relative-interior positive-ray intersection on a refined top simplex.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.hasPositiveInteriorZeroDecidable {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) : Decidable (HasPositiveInteriorZero hp N F q)

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.hasPositiveInteriorZeroDecidable hp N F q = Classical.propDecidable (NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.HasPositiveInteriorZero hp N F q)

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.localIndex {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) (q : TopCell hp N) : ZMod p

Signed local positive-ray index on one refined simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.coefficient {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : TopCell hp N) : ZMod p

Coefficient of a refined top cell: original orbit-cycle coefficient times subdivision sign.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.zeroCount {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : ContinuousCoordinateMap p) : ZMod p

Refined positive orbit count.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.segment {p : ℕ} (F G : ContinuousCoordinateMap p) (t : ℝ) : ContinuousCoordinateMap p

Straight-line combination of two continuous coordinate maps.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.segment F G t = { toFun := fun (x : NRR.FoxNeuwirthOrderComplex.Realization p) => (1 - t) • F x + t • G x, continuous_toFun := ⋯ }

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.segment_zero {p : ℕ} (F G : ContinuousCoordinateMap p) : segment F G 0 = F

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.segment_one {p : ℕ} (F G : ContinuousCoordinateMap p) : segment F G 1 = G

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.ofCoordinateAffineVertexMap {p : ℕ} (F : CoordinateAffineVertexMap p) : ContinuousCoordinateMap p

A continuous map obtained from an original affine vertex map.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.ofCoordinateAffineVertexMap F = { toFun := F.globalValue, continuous_toFun := ⋯ }

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.augmentedMatrix_segment {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F G : ContinuousCoordinateMap p) (t : ℝ) (q : TopCell hp N) : augmentedMatrix hp N (segment F G t) q = (1 - t) • augmentedMatrix hp N F q + t • augmentedMatrix hp N G q

Refined augmented matrices depend affinely on straight-line combinations of global maps.