Boundary-respecting facet targets for affine-pullback endpoint stacks

The first endpoint-stack layer has a distinguished coarse lower simplex. Every time-zero local vertex is one of its vertices, and those vertices are pairwise distinct. A partial injection from frozen facet columns to coarse-simplex vertices therefore extends to a permutation. Filling the remaining movable columns with the missing coarse-simplex values makes the selected facet a column permutation of the regular endpoint matrix.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.dimShift {p : ℕ} (hp : Nat.Prime p) : p + 1 = p - 1 + 2

Vertex-index shift between a one-step cell and its local subdivision cylinder.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.cylinderVertex_time {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (q : (RelativeSubdivisionOneStepCells.cellSystem hp N).Cell) (i : Fin (p + 1)) : ↑(RelativeSubdivisionCylinderCombinatorics.vertex (p - 1) q.2 (Fin.cast ⋯ i)).2 = ↑((RelativeSubdivisionOneStepCells.cellSystem hp N).vertex q i).time

The local cylinder time of a one-step cell vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.cylinderVertex_point {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (q : (RelativeSubdivisionOneStepCells.cellSystem hp N).Cell) (i : Fin (p + 1)) : RelativeSubdivisionOneStepCells.localPoint hp q.2 (SphereOddDegree.FiniteSimplex.vertex i) = RelativeSubdivisionCylinderCombinatorics.vertex (p - 1) q.2 (Fin.cast ⋯ i)

The local cylinder point of a one-step cell vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.exists_perm_extending_finset {α : Type u_1} (s : Finset α) (f : α → α) (hinj : Set.InjOn f ↑s) : ∃ (e : Equiv.Perm α), ∀ x ∈ s, e x = f x

A finite partial injection into a finite type extends to a permutation.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.lowerFrozenColumns {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (q : (RelativeSubdivisionOneStepCells.cellSystem hp N).Cell) (k : Fin (p + 1)) : Finset (Fin p)

Facet columns whose represented local vertices lie on the coarse lower boundary.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.lowerColumnIndex {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (q : (RelativeSubdivisionOneStepCells.cellSystem hp N).Cell) (k : Fin (p + 1)) (c : ↥(lowerFrozenColumns hp q k)) : Fin p

Coarse lower-simplex index represented by a frozen facet column.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.lowerColumnIndex_injective {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (q : (RelativeSubdivisionOneStepCells.cellSystem hp N).Cell) (k : Fin (p + 1)) : Function.Injective (lowerColumnIndex hp q k)

The frozen-column map is injective.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.lowerFacetPermutation {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (q : (RelativeSubdivisionOneStepCells.cellSystem hp N).Cell) (k : Fin (p + 1)) : Equiv.Perm (Fin p)

A permutation extending the frozen-column identification.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.lowerFacetPermutation hp q k = Classical.choose ⋯

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.lowerFacetPermutation_frozen {p : ℕ} (hp : Nat.Prime p) {N : ℕ} (q : (RelativeSubdivisionOneStepCells.cellSystem hp N).Cell) (k : Fin (p + 1)) (c : Fin p) (hc : c ∈ lowerFrozenColumns hp q k) : (lowerFacetPermutation hp q k) c = lowerColumnIndex hp q k ⟨c, hc⟩

The chosen permutation agrees with the represented lower index on every frozen column.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.oneStepLowerFacetTarget {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.StableRegularApproximation hp F) (q : (RelativeSubdivisionOneStepCells.cellSystem hp A.level).Cell) (k : Fin (p + 1)) : Fin (p + 1) → Fin p → ℝ

Boundary-respecting target whose selected facet is the regular endpoint matrix with permuted columns.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.oneStepLowerFacetTarget_succAbove {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.StableRegularApproximation hp F) (q : (RelativeSubdivisionOneStepCells.cellSystem hp A.level).Cell) (k : Fin (p + 1)) (c j : Fin p) : oneStepLowerFacetTarget hp A q k (k.succAbove c) j = RefinedAffineMap.vertexValue hp A.level A.map q.1 ((AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp) ((lowerFacetPermutation hp q k) c)) j

Values on the selected facet have the advertised permuted endpoint form.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.facetMatrix_oneStepLowerFacetTarget {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.StableRegularApproximation hp F) (q : (RelativeSubdivisionOneStepCells.cellSystem hp A.level).Cell) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetMatrix hp { value := oneStepLowerFacetTarget hp A q k } k = (RefinedAffineMap.augmentedMatrix hp A.level A.map q.1).submatrix ⇑(AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp) fun (i : Fin p) => (AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp) ((lowerFacetPermutation hp q k) i)

The selected target facet matrix is a column permutation of the endpoint regularity matrix.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.oneStepLowerFacetTarget_determinant_ne_zero {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.StableRegularApproximation hp F) (q : (RelativeSubdivisionOneStepCells.cellSystem hp A.level).Cell) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetDeterminant hp { value := oneStepLowerFacetTarget hp A q k } k ≠ 0

The selected target facet is regular.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.oneStepLowerFacetTarget_respects_lower {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.StableRegularApproximation hp F) (q : (RelativeSubdivisionOneStepCells.cellSystem hp A.level).Cell) (k i : Fin (p + 1)) (j : Fin p) : ↑((RelativeSubdivisionOneStepCells.cellSystem hp A.level).vertex q i).time = 0 → oneStepLowerFacetTarget hp A q k i j = (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (RelativeSubdivisionOneStepCells.cellSystem hp A.level) (CompatibleChartMapOneStep.assignment hp (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A.toRegularApproximation)) q).value i j

The target leaves every lower-horizontal local scalar coordinate fixed.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.LowerFacetTargets {p : ℕ} (hp : Nat.Prime p) {N₀ N₁ M L : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) : Prop

Lower-relative facet target property used by stack composition.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBEndpointFacetTargets.oneStep_lowerFacetTargets {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.StableRegularApproximation hp F) : LowerFacetTargets hp (RelativeSubdivisionOneStepCells.cellSystem hp A.level) (CompatibleChartMapOneStep.assignment hp (CompatibleRefinedChartHomotopy.baseOriginalPLMap hp A.toRegularApproximation))

One endpoint layer has lower-relative facet targets.