Endpoint facets of the one-step relative subdivision cylinder

This module identifies the two external horizontal boundaries of the explicit recursive cylinder constructed in RelativeSubdivisionOneStepCells.

The lower boundary is the coarse level-N Fox--Neuwirth simplex. The upper boundary is the first barycentric subdivision, indexed by level-N + 1 top cells. The definitions are made at the quotient-facet level, while the geometric theorems are stated for arbitrary representatives of the canonical occurrences. The signed boundary formula is supplied in the following module.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.splitTopCellEquiv {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : RefinedAffineMap.TopCell hp (N + 1) ≃ RefinedAffineMap.TopCell hp N × Equiv.Perm (Fin p)

Split a level-N + 1 top cell into its level-N prefix and final subdivision permutation.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.subdivisionSign_snoc {p : ℕ} (N : ℕ) (rho : RefinementWord p N) (pi : Equiv.Perm (Fin p)) : RefinedAffineMap.subdivisionSign (N + 1) (Fin.snoc rho pi) = RefinedAffineMap.subdivisionSign N rho * ↑↑(Equiv.Perm.sign pi)

The subdivision sign factors when one final permutation is appended.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.coefficient_snoc {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (pi : Equiv.Perm (Fin p)) : RefinedAffineMap.coefficient hp (N + 1) (q.1, Fin.snoc q.2 pi) = RefinedAffineMap.coefficient hp N q * ↑↑(Equiv.Perm.sign pi)

Refined Fox--Neuwirth coefficients factor under one final subdivision step.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.lowerOccurrence {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence

Canonical lower horizontal occurrence over a level-N top cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperOccurrenceBase {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (pi : Equiv.Perm (Fin p)) : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence

Canonical upper horizontal occurrence over a level-N cell and one final subdivision permutation.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperOccurrence {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp (N + 1)) : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence

Canonical upper horizontal occurrence indexed by a level-N + 1 top cell.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.lowerFacet {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet

Canonical lower quotient facet.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperFacet {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp (N + 1)) : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet

Canonical upper quotient facet.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.lowerOccurrence_isLower {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsLowerFacetOccurrence (lowerOccurrence hp N q)

The canonical lower occurrence lies entirely in the time-zero boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperOccurrenceBase_isUpper {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (pi : Equiv.Perm (Fin p)) : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsUpperFacetOccurrence (upperOccurrenceBase hp N q pi)

The canonical upper occurrence lies entirely in the time-one boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperOccurrence_isUpper {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp (N + 1)) : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsUpperFacetOccurrence (upperOccurrence hp N q)

The canonical upper occurrence indexed by a refined top cell is horizontal at time one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.lowerFacet_isLower {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsLowerFacet (lowerFacet hp N q)

Every canonical lower quotient facet is lower-horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperFacet_isUpper {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp (N + 1)) : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsUpperFacet (upperFacet hp N q)

Every canonical upper quotient facet is upper-horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.lowerOccurrence_facetSignature {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (i : Fin p) : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetSignature (lowerOccurrence hp N q) i = ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp N q (Fin.cast ⋯ i))

Vertex signature of the coarse lower endpoint.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.refinedChart_snoc_vertex {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (pi : Equiv.Perm (Fin p)) (i : Fin p) : (RefinedAffineMap.chart hp N q) (SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter (p - 1) (Simplex.refinementIndexPerm pi) (Fin.cast ⋯ i)) = RefinedAffineMap.vertex hp (N + 1) (q.1, Fin.snoc q.2 pi) (Fin.cast ⋯ i)

Appending one permutation to a refinement word is the recursive affineCompMap step.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperOccurrenceBase_facetSignature {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (pi : Equiv.Perm (Fin p)) (i : Fin p) : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetSignature (upperOccurrenceBase hp N q pi) i = ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp (N + 1) (q.1, Fin.snoc q.2 pi) (Fin.cast ⋯ i))

Vertex signature of the refined upper endpoint before reindexing by level-N + 1 top cells.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperOccurrence_facetSignature {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp (N + 1)) (i : Fin p) : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetSignature (upperOccurrence hp N q) i = ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp (N + 1) q (Fin.cast ⋯ i))

Vertex signature of the canonical upper endpoint indexed by a level-N + 1 top cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.lowerOccurrence_exhaustive {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (o : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence) (ho : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsLowerFacetOccurrence o) : ∃ (q : RefinedAffineMap.TopCell hp N), (RelativeSubdivisionOneStepCells.cellSystem hp N).facetClass o = lowerFacet hp N q

Every lower-horizontal occurrence is the canonical lower occurrence of its level-N spatial cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperOccurrence_exhaustive {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (o : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence) (ho : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsUpperFacetOccurrence o) : ∃ (q : RefinedAffineMap.TopCell hp (N + 1)), (RelativeSubdivisionOneStepCells.cellSystem hp N).facetClass o = upperFacet hp N q

Every upper-horizontal occurrence is the canonical upper occurrence of a unique final subdivision permutation over its level-N spatial prefix.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.lowerFacet_exhaustive {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (hs : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsLowerFacet s) : ∃ (q : RefinedAffineMap.TopCell hp N), lowerFacet hp N q = s

Every lower-horizontal quotient facet is represented by a canonical lower endpoint cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperFacet_exhaustive {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (hs : (RelativeSubdivisionOneStepCells.cellSystem hp N).IsUpperFacet s) : ∃ (q : RefinedAffineMap.TopCell hp (N + 1)), upperFacet hp N q = s

Every upper-horizontal quotient facet is represented by a canonical upper endpoint cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.lowerFacetOccurrenceVertex_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp N) (o : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence) (ho : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetClass o = lowerFacet hp N q) : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (RelativeSubdivisionOneStepCells.cellSystem hp N).facetSignature o i = g • ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp N q (Fin.cast ⋯ i))

Any representative of a canonical lower quotient facet has the prescribed endpoint geometry, up to one simultaneous prime relabelling.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepEndpoints.upperFacetOccurrenceVertex_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (q : RefinedAffineMap.TopCell hp (N + 1)) (o : (RelativeSubdivisionOneStepCells.cellSystem hp N).FacetOccurrence) (ho : (RelativeSubdivisionOneStepCells.cellSystem hp N).facetClass o = upperFacet hp N q) : ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (RelativeSubdivisionOneStepCells.cellSystem hp N).facetSignature o i = g • ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp (N + 1) q (Fin.cast ⋯ i))

Any representative of a canonical upper quotient facet has the prescribed endpoint geometry, up to one simultaneous prime relabelling.