Endpoint-identified one-step subdivision collar

The pointwise boundary identity from RelativeSubdivisionOneStepBoundary is packaged here as a FoxNeuwirthRelativeAffineCollar. The canonical lower and upper quotient facets constructed in RelativeSubdivisionOneStepEndpoints identify its horizontal boundary with the level-N and level-N+1 refined Fox--Neuwirth chains.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCollar.lowerBoundaryCoefficient_zero_of_not_lower {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (hs : ¬(RelativeSubdivisionOneStepCells.cellSystem hp N).IsLowerFacet s) : RelativeSubdivisionOneStepBoundary.lowerBoundaryCoefficient hp N s = 0

Lower boundary coefficients vanish on non-lower quotient facets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCollar.upperBoundaryCoefficient_zero_of_not_upper {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet) (hs : ¬(RelativeSubdivisionOneStepCells.cellSystem hp N).IsUpperFacet s) : RelativeSubdivisionOneStepBoundary.upperBoundaryCoefficient hp N s = 0

Upper boundary coefficients vanish on non-upper quotient facets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCollar.lowerBoundaryPairing_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : ∑ s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet, RelativeSubdivisionOneStepBoundary.lowerBoundaryCoefficient hp N s * W s = ∑ q : RefinedAffineMap.TopCell hp N, RefinedAffineMap.coefficient hp N q * W (RelativeSubdivisionOneStepEndpoints.lowerFacet hp N q)

Pairing the lower pointwise boundary coefficients against any weight recovers exactly the level-N refined orbit chain.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCollar.upperBoundaryPairing_eq {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (W : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet → ZMod p) : ∑ s : (RelativeSubdivisionOneStepCells.cellSystem hp N).Facet, RelativeSubdivisionOneStepBoundary.upperBoundaryCoefficient hp N s * W s = ∑ q : RefinedAffineMap.TopCell hp (N + 1), RefinedAffineMap.coefficient hp (N + 1) q * W (RelativeSubdivisionOneStepEndpoints.upperFacet hp N q)

Pairing the upper pointwise boundary coefficients against any weight recovers exactly the level-N+1 refined orbit chain.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCollar.relativeCollar {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp N (N + 1) (N + 1) 0

The genuine one-step affine collar from refinement level N to level N+1.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCollar.endpointIdentifiedCollar {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N (N + 1) (N + 1) 0

The one-step collar has exactly the independently refined Fox--Neuwirth endpoint chains.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeSubdivisionOneStepCollar.relativeAffineCollarExists_succ {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ExplicitAffineRelativeCollar.RelativeAffineCollarExists hp N (N + 1) (N + 1) 0

Existence form of the one-step relative subdivision collar.