Order complex of the Fox--Neuwirth face relation

This module defines the order complex of the finite barred-permutation face relation. Instead of trying to glue a family of closed top-cell simplices by a separate regular-CW construction, it passes to the order complex of the finite barred-permutation face relation.

A d-simplex is a strict chain of d + 1 barred permutations. Strictness is measured by a proper face relation that includes a strict increase of dual dimension. Consequently the vertices of a simplex are distinct, relabelling preserves simplices, and every strictly increasing map of finite ordinals gives a face restriction. These are the combinatorial data needed for a later global barycentric realization, where shared subchains are literally shared faces.

The file also defines the global barycentric carrier as nonnegative weights of total mass one with chain support. Compactness, simplex charts, the prime action on that carrier, and its collision-free map into configuration space are the associated geometric constructions.

def NRR.FoxNeuwirthOrderComplex.ProperFace {p : ℕ} (a b : BarredPermutation p) : Prop

Dimension-increasing proper face relation used by the order complex.

Equations

• NRR.FoxNeuwirthOrderComplex.ProperFace a b = (a.IsFace b ∧ a.dualDimension < b.dualDimension)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.properFaceDecidable {p : ℕ} (a b : BarredPermutation p) : Decidable (ProperFace a b)

Equations

• NRR.FoxNeuwirthOrderComplex.properFaceDecidable a b = Classical.dec (NRR.FoxNeuwirthOrderComplex.ProperFace a b)

theorem NRR.FoxNeuwirthOrderComplex.ProperFace.ne {p : ℕ} {a b : BarredPermutation p} (h : ProperFace a b) : a ≠ b

A proper face is never equal to the cell containing it.

theorem NRR.FoxNeuwirthOrderComplex.properFace_trans {p : ℕ} {a b c : BarredPermutation p} (hab : ProperFace a b) (hbc : ProperFace b c) : ProperFace a c

Proper faces compose.

theorem NRR.FoxNeuwirthOrderComplex.properFace_relabel_iff {p : ℕ} (sigma : Equiv.Perm (Fin p)) (a b : BarredPermutation p) : ProperFace (BarredPermutation.relabel sigma a) (BarredPermutation.relabel sigma b) ↔ ProperFace a b

Relabelling preserves and reflects proper faces.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.Simplex (p d : ℕ) : Type

A d-simplex in the order complex is a strict chain of d + 1 cells.

Equations

• NRR.FoxNeuwirthOrderComplex.Simplex p d = { vertex : Fin (d + 1) → NRR.BarredPermutation p // ∀ ⦃i j : Fin (d + 1)⦄, i < j → NRR.FoxNeuwirthOrderComplex.ProperFace (vertex i) (vertex j) }

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.Simplex.instFintype {p d : ℕ} : Fintype (Simplex p d)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.Simplex.instDecidableEq {p d : ℕ} : DecidableEq (Simplex p d)

Equations

• NRR.FoxNeuwirthOrderComplex.Simplex.instDecidableEq = Classical.decEq (NRR.FoxNeuwirthOrderComplex.Simplex p d)

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.Simplex.instCoeFunForallFinHAddNatOfNatBarredPermutation {p d : ℕ} : CoeFun (Simplex p d) fun (x : Simplex p d) => Fin (d + 1) → BarredPermutation p

Equations

• NRR.FoxNeuwirthOrderComplex.Simplex.instCoeFunForallFinHAddNatOfNatBarredPermutation = { coe := Subtype.val }

theorem NRR.FoxNeuwirthOrderComplex.Simplex.ext {p d : ℕ} {s t : Simplex p d} (h : ∀ (i : Fin (d + 1)), ↑s i = ↑t i) : s = t

theorem NRR.FoxNeuwirthOrderComplex.Simplex.ext_iff {p d : ℕ} {s t : Simplex p d} : s = t ↔ ∀ (i : Fin (d + 1)), ↑s i = ↑t i

theorem NRR.FoxNeuwirthOrderComplex.Simplex.properFace {p d : ℕ} (s : Simplex p d) {i j : Fin (d + 1)} (hij : i < j) : ProperFace (↑s i) (↑s j)

The defining chain relation, exposed as a theorem.

theorem NRR.FoxNeuwirthOrderComplex.Simplex.vertex_injective {p d : ℕ} (s : Simplex p d) : Function.Injective ↑s

Vertices in a strict chain are pairwise distinct.

def NRR.FoxNeuwirthOrderComplex.Simplex.ofCell {p : ℕ} (c : BarredPermutation p) : Simplex p 0

Every barred permutation gives a vertex of the order complex.

Equations

• NRR.FoxNeuwirthOrderComplex.Simplex.ofCell c = ⟨fun (x : Fin (0 + 1)) => c, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.ofCell_apply {p : ℕ} (c : BarredPermutation p) (i : Fin 1) : ↑(ofCell c) i = c

def NRR.FoxNeuwirthOrderComplex.Simplex.relabel {p d : ℕ} (sigma : Equiv.Perm (Fin p)) (s : Simplex p d) : Simplex p d

Relabel every vertex in a simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.Simplex.relabel sigma s = ⟨fun (i : Fin (d + 1)) => NRR.BarredPermutation.relabel sigma (↑s i), ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.relabel_apply {p d : ℕ} (sigma : Equiv.Perm (Fin p)) (s : Simplex p d) (i : Fin (d + 1)) : ↑(relabel sigma s) i = BarredPermutation.relabel sigma (↑s i)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.relabel_one {p d : ℕ} (s : Simplex p d) : relabel 1 s = s

theorem NRR.FoxNeuwirthOrderComplex.Simplex.relabel_mul {p d : ℕ} (sigma tau : Equiv.Perm (Fin p)) (s : Simplex p d) : relabel (sigma * tau) s = relabel sigma (relabel tau s)

Relabelling is a left action with the convention already used on configurations.

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.Simplex.primeSymmetryAction {d : ℕ} (p : ℕ) : MulAction (↥(PrimeSymmetry p)) (Simplex p d)

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.prime_smul_apply {d : ℕ} (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p d) (i : Fin (d + 1)) : ↑(g • s) i = g • ↑s i

def NRR.FoxNeuwirthOrderComplex.Simplex.support {p d : ℕ} (s : Simplex p d) : Finset (BarredPermutation p)

Finite vertex support of an order-complex simplex.

Equations

• s.support = Finset.image (↑s) Finset.univ

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.mem_support_iff {p d : ℕ} (s : Simplex p d) (c : BarredPermutation p) : c ∈ s.support ↔ ∃ (i : Fin (d + 1)), ↑s i = c

theorem NRR.FoxNeuwirthOrderComplex.Simplex.support_nonempty {p d : ℕ} (s : Simplex p d) : s.support.Nonempty

Every order-complex simplex has nonempty support.

def NRR.FoxNeuwirthOrderComplex.ChainSupported {p : ℕ} (weight : BarredPermutation p → ℝ) : Prop

A barycentric weight has chain support when every two distinct nonzero coordinates are comparable by the proper-face relation.

Equations

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

def NRR.FoxNeuwirthOrderComplex.Realization (p : ℕ) : Type

Global barycentric carrier of the order complex.

Using coordinates indexed by all barred permutations identifies shared faces automatically: a point belongs to a simplex precisely when its nonzero coordinate support is contained in the corresponding strict chain.

Equations

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

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.Realization.instCoeFunForallBarredPermutationReal {p : ℕ} : CoeFun (Realization p) fun (x : Realization p) => BarredPermutation p → ℝ

Equations

• NRR.FoxNeuwirthOrderComplex.Realization.instCoeFunForallBarredPermutationReal = { coe := Subtype.val }

theorem NRR.FoxNeuwirthOrderComplex.Realization.ext {p : ℕ} {x y : Realization p} (h : ∀ (c : BarredPermutation p), ↑x c = ↑y c) : x = y

theorem NRR.FoxNeuwirthOrderComplex.Realization.ext_iff {p : ℕ} {x y : Realization p} : x = y ↔ ∀ (c : BarredPermutation p), ↑x c = ↑y c

theorem NRR.FoxNeuwirthOrderComplex.Realization.nonneg {p : ℕ} (x : Realization p) (c : BarredPermutation p) : 0 ≤ ↑x c

Every barycentric coordinate is nonnegative.

theorem NRR.FoxNeuwirthOrderComplex.Realization.sum_eq_one {p : ℕ} (x : Realization p) : ∑ c : BarredPermutation p, ↑x c = 1

Barycentric coordinates sum to one.

theorem NRR.FoxNeuwirthOrderComplex.Realization.chainSupported {p : ℕ} (x : Realization p) : ChainSupported ↑x

The nonzero coordinates form a chain.

noncomputable def NRR.FoxNeuwirthOrderComplex.Realization.support {p : ℕ} (x : Realization p) : Finset (BarredPermutation p)

Finite nonzero coordinate support of a realization point.

Equations

• x.support = {c : NRR.BarredPermutation p | ↑x c ≠ 0}

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Realization.mem_support_iff {p : ℕ} (x : Realization p) (c : BarredPermutation p) : c ∈ x.support ↔ ↑x c ≠ 0

def NRR.FoxNeuwirthOrderComplex.Realization.vertexWeight {p : ℕ} (c : BarredPermutation p) : BarredPermutation p → ℝ

Coordinate vector of a vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.Realization.vertexWeight c d = if d = c then 1 else 0

def NRR.FoxNeuwirthOrderComplex.Realization.vertex {p : ℕ} (c : BarredPermutation p) : Realization p

Every barred permutation is a vertex of the global realization.

Equations

• NRR.FoxNeuwirthOrderComplex.Realization.vertex c = ⟨NRR.FoxNeuwirthOrderComplex.Realization.vertexWeight c, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Realization.vertex_apply {p : ℕ} (c d : BarredPermutation p) : ↑(vertex c) d = if d = c then 1 else 0

theorem NRR.FoxNeuwirthOrderComplex.Realization.vertex_self {p : ℕ} (c : BarredPermutation p) : ↑(vertex c) c = 1

theorem NRR.FoxNeuwirthOrderComplex.Realization.vertex_apply_of_ne {p : ℕ} {c d : BarredPermutation p} (h : d ≠ c) : ↑(vertex c) d = 0

theorem NRR.FoxNeuwirthOrderComplex.Realization.support_vertex {p : ℕ} (c : BarredPermutation p) : (vertex c).support = {c}

The support of a vertex is the singleton containing that cell.

structure NRR.FoxNeuwirthOrderComplex.FaceMap (m d : ℕ) : Type

A strictly increasing finite-ordinal map selects a face of an order-complex simplex.

• toFun : Fin (m + 1) → Fin (d + 1)

  The strictly increasing map of finite vertex indices selecting the face.

• strictMono : StrictMono self.toFun

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.FaceMap.instCoeFunForallFinHAddNatOfNat {d m : ℕ} : CoeFun (FaceMap m d) fun (x : FaceMap m d) => Fin (m + 1) → Fin (d + 1)

Equations

• NRR.FoxNeuwirthOrderComplex.FaceMap.instCoeFunForallFinHAddNatOfNat = { coe := NRR.FoxNeuwirthOrderComplex.FaceMap.toFun }

def NRR.FoxNeuwirthOrderComplex.FaceMap.id (d : ℕ) : FaceMap d d

Identity face map.

Equations

• NRR.FoxNeuwirthOrderComplex.FaceMap.id d = { toFun := fun (i : Fin (d + 1)) => i, strictMono := ⋯ }

def NRR.FoxNeuwirthOrderComplex.FaceMap.comp {d m l : ℕ} (f : FaceMap m d) (g : FaceMap l m) : FaceMap l d

Composition of face maps.

Equations

• f.comp g = { toFun := fun (i : Fin (l + 1)) => f.toFun (g.toFun i), strictMono := ⋯ }

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.FaceMap.id_apply {d : ℕ} (i : Fin (d + 1)) : (id d).toFun i = i

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.FaceMap.comp_apply {d m l : ℕ} (f : FaceMap m d) (g : FaceMap l m) (i : Fin (l + 1)) : (f.comp g).toFun i = f.toFun (g.toFun i)

def NRR.FoxNeuwirthOrderComplex.Simplex.restrict {p d m : ℕ} (s : Simplex p d) (f : FaceMap m d) : Simplex p m

Restrict a simplex along an increasing vertex map. This is the abstract face operation.

Equations

• s.restrict f = ⟨fun (i : Fin (m + 1)) => ↑s (f.toFun i), ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.restrict_apply {p d m : ℕ} (s : Simplex p d) (f : FaceMap m d) (i : Fin (m + 1)) : ↑(s.restrict f) i = ↑s (f.toFun i)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.restrict_id {p d : ℕ} (s : Simplex p d) : s.restrict (FaceMap.id d) = s

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.Simplex.restrict_comp {p d m l : ℕ} (s : Simplex p d) (f : FaceMap m d) (g : FaceMap l m) : (s.restrict f).restrict g = s.restrict (f.comp g)

theorem NRR.FoxNeuwirthOrderComplex.Simplex.relabel_restrict {p d m : ℕ} (sigma : Equiv.Perm (Fin p)) (s : Simplex p d) (f : FaceMap m d) : relabel sigma (s.restrict f) = (relabel sigma s).restrict f

Relabelling commutes with taking abstract faces.

theorem NRR.FoxNeuwirthOrderComplex.Simplex.support_restrict_subset {p d m : ℕ} (s : Simplex p d) (f : FaceMap m d) : (s.restrict f).support ⊆ s.support

The support of an abstract face is contained in the support of the ambient simplex.

theorem NRR.FoxNeuwirthOrderComplex.simplex_finite (p d : ℕ) : Finite (Simplex p d)

The order complex has a finite simplex type in every fixed dimension.

theorem NRR.FoxNeuwirthOrderComplex.zeroSimplex_nonempty (p : ℕ) : Nonempty (Simplex p 0)

The order complex is nonempty in dimension zero: every cell supplies a zero-simplex.