Finite top-cell atlas

The concrete Fox–Neuwirth model is a finite disjoint union of standard (p - 1)-simplices. This file records the closed and open cell components, their compactness, and the explicit simplex charts. The later mod-p cycle construction replaces this disjoint atlas by the invariant glued chain.

def NRR.FoxNeuwirthTopCellModelPoint.cellCarrier {p : ℕ} (c : FoxNeuwirthTopCell p) : Set (FoxNeuwirthTopCellModelPoint p)

Closed component indexed by a one-block barred permutation.

Equations

• NRR.FoxNeuwirthTopCellModelPoint.cellCarrier c = {z : NRR.FoxNeuwirthTopCellModelPoint p | z.1 = c}

def NRR.FoxNeuwirthTopCellModelPoint.cellInterior {p : ℕ} (c : FoxNeuwirthTopCell p) : Set (FoxNeuwirthTopCellModelPoint p)

Relative interior of a top-cell component.

Equations

• NRR.FoxNeuwirthTopCellModelPoint.cellInterior c = {z : NRR.FoxNeuwirthTopCellModelPoint p | z.1 = c ∧ ∀ (i : Fin p), 0 < ↑z.2 i}

def NRR.FoxNeuwirthTopCellModelPoint.cellParam {p : ℕ} (c : FoxNeuwirthTopCell p) : FoxNeuwirthWeights p → FoxNeuwirthTopCellModelPoint p

Standard simplex chart for one component.

Equations

• NRR.FoxNeuwirthTopCellModelPoint.cellParam c w = (c, w)

@[simp]

theorem NRR.FoxNeuwirthTopCellModelPoint.cellParam_apply {p : ℕ} (c : FoxNeuwirthTopCell p) (w : FoxNeuwirthWeights p) : cellParam c w = (c, w)

theorem NRR.FoxNeuwirthTopCellModelPoint.continuous_cellParam {p : ℕ} (c : FoxNeuwirthTopCell p) : Continuous (cellParam c)

theorem NRR.FoxNeuwirthTopCellModelPoint.injective_cellParam {p : ℕ} (c : FoxNeuwirthTopCell p) : Function.Injective (cellParam c)

theorem NRR.FoxNeuwirthTopCellModelPoint.range_cellParam {p : ℕ} (c : FoxNeuwirthTopCell p) : Set.range (cellParam c) = cellCarrier c

theorem NRR.FoxNeuwirthTopCellModelPoint.isClosed_cellCarrier {p : ℕ} (c : FoxNeuwirthTopCell p) : IsClosed (cellCarrier c)

theorem NRR.FoxNeuwirthTopCellModelPoint.isOpen_cellCarrier {p : ℕ} (c : FoxNeuwirthTopCell p) : IsOpen (cellCarrier c)

theorem NRR.FoxNeuwirthTopCellModelPoint.isCompact_cellCarrier {p : ℕ} (c : FoxNeuwirthTopCell p) : IsCompact (cellCarrier c)

theorem NRR.FoxNeuwirthTopCellModelPoint.cellCarrier_pairwise_disjoint {p : ℕ} {c d : FoxNeuwirthTopCell p} (hcd : c ≠ d) : Disjoint (cellCarrier c) (cellCarrier d)

theorem NRR.FoxNeuwirthTopCellModelPoint.cellCarrier_cover {p : ℕ} : ⋃ (c : FoxNeuwirthTopCell p), cellCarrier c = Set.univ

def NRR.FoxNeuwirthTopCellModelPoint.cellDimension (p : ℕ) (_c : FoxNeuwirthTopCell p) : ℕ

The declared dimension of every maximal component.

Equations

• NRR.FoxNeuwirthTopCellModelPoint.cellDimension p _c = p - 1

theorem NRR.FoxNeuwirthTopCellModelPoint.cellDimension_eq (p : ℕ) (c : FoxNeuwirthTopCell p) : cellDimension p c = p - 1

def NRR.FoxNeuwirthTopCellModelPoint.cellHomeomorph {p : ℕ} (c : FoxNeuwirthTopCell p) : FoxNeuwirthWeights p ≃ₜ ↑(cellCarrier c)

Each component is homeomorphic to the standard simplex.

Equations

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