Pointwise boundary formula for the common-level middle prism

The older prism development proves cancellation only after weighting facets by the positive-ray index of a compatible assignment. An explicit relative collar needs the stronger pointwise chain statement: the signed incidence of every prime-orbit facet equals upper boundary coefficient minus lower boundary coefficient.

This module extracts the underlying weighted boundary theorem for an arbitrary prime-invariant facet-map weight. Applying it to the characteristic function of one prime-orbit facet gives the required pointwise incidence formula. The resulting object is a genuine FoxNeuwirthRelativeAffineCollar at the common endpoint level N + L.

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.Cells {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp (N + L) (N + L) (N + L) L

The concrete middle-prism cell system.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.mapVertexSignature {p : ℕ} (hp : Nat.Prime p) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : Fin p → EquivariantPrismVertexParameters.CylinderPoint p

Ordered geometric vertices of an arbitrary affine facet map.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.translateFacetMap (p : ℕ) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)

Prime translation of an affine facet map.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.translateFacetMap p g tau x = (g • (tau x).1, (tau x).2)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.mapVertexSignature_translateFacetMap {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : mapVertexSignature hp (translateFacetMap p g tau) = fun (i : Fin p) => g • mapVertexSignature hp tau i

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.mapVertexSignature_occurrenceFacetMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (o : (Cells hp N L).FacetOccurrence) : mapVertexSignature hp (EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap hp N L o) = (Cells hp N L).facetSignature o

The old affine occurrence map and the new explicit-cell occurrence have the same ordered geometric vertex signature.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.facetOrbitIndicator {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Characteristic weight of one ordered prime-orbit facet. It is defined on all affine facet maps so it can be used in the generic staircase and subdivision boundary identities.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.facetOrbitIndicator_translate {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : facetOrbitIndicator hp N L s (translateFacetMap p g tau) = facetOrbitIndicator hp N L s tau

The facet-orbit characteristic weight is invariant under simultaneous prime translation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.facetOrbitIndicator_occurrence {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) (o : (Cells hp N L).FacetOccurrence) : facetOrbitIndicator hp N L s (EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap hp N L o) = if (Cells hp N L).facetClass o = s then 1 else 0

On an actual occurrence, the orbit characteristic weight is exactly the Kronecker delta of its quotient facet class.

Generic weighted boundary formulas

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.lowerMapWeight {p : ℕ} (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Keep only lower-horizontal affine facet maps.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.upperMapWeight {p : ℕ} (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Keep only upper-horizontal affine facet maps.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.sideMapWeight {p : ℕ} (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ZMod p

Keep only nonhorizontal affine facet maps.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.not_lower_and_upper_map {p : ℕ} (hp : Nat.Prime p) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : ¬(EquivariantPrismNonhorizontalCancellation.MapIsLowerHorizontal tau ∧ EquivariantPrismNonhorizontalCancellation.MapIsUpperHorizontal tau)

A facet map cannot be both lower and upper horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.lower_add_upper_add_side {p : ℕ} (hp : Nat.Prime p) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : lowerMapWeight W tau + upperMapWeight W tau + sideMapWeight W tau = W tau

Every facet-map weight splits into lower, upper, and nonhorizontal parts.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.occurrencePairing {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : ZMod p

Expanded occurrence pairing for an arbitrary facet-map weight.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.lowerEndpointPairing {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : ZMod p

Lower endpoint pairing at the combined spatial level.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.upperEndpointPairing {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : ZMod p

Upper endpoint pairing at the combined spatial level.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.occurrencePairing_lower {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : occurrencePairing hp N L (lowerMapWeight W) = -lowerEndpointPairing hp N L W

Lower-horizontal part of the arbitrary weighted occurrence pairing.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.occurrencePairing_upper {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) : occurrencePairing hp N L (upperMapWeight W) = upperEndpointPairing hp N L W

Upper-horizontal part of the arbitrary weighted occurrence pairing.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.sideMapWeight_translate (p : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (hW : ∀ (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)), W (translateFacetMap p g tau) = W tau) (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) : sideMapWeight W (translateFacetMap p g tau) = sideMapWeight W tau

Prime invariance is inherited by the nonhorizontal restriction of a weight.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.arbitrarySpatialSideWeight {n : ℕ} (hp : Nat.Prime (n + 1)) (L : ℕ) (V : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → Realization (n + 1) × ↑(Set.Icc 0 1)) → ZMod (n + 1)) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (h : Fin n) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n - 1)) → Realization (n + 1)) : ZMod (n + 1)

Weight of a staircase side simplex for an arbitrary affine-facet weight. This is the weight-independent form of the construction used in nonhorizontal cancellation.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.refined_side_eq_arbitrarySpatialSideWeight {n : ℕ} (hp : Nat.Prime (n + 1)) (N L : ℕ) (V : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n) → Realization (n + 1) × ↑(Set.Icc 0 1)) → ZMod (n + 1)) (orbit : PrimeOrbitCycle.TopOrbit hp) (spatial : RefinementWord (n + 1) N) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (r : Fin (n + 1)) (h : Fin n) : have hn := ⋯; have hd := ⋯; have spatial' := fun (k : Fin N) => ((Equiv.cast ⋯).trans (spatial k)).trans (Equiv.cast ⋯); have baseSimplex := fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n - 1 + 1))) => (ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap (EquivariantPrismNonhorizontalCancellation.deltaCast ⋯ x); (V fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) => EquivariantPrismNonhorizontalCancellation.sidePrismMap n (⇑(RefinedAffineMap.chart hp N (orbit, spatial))) r h ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n L eta) x)) = arbitrarySpatialSideWeight hp L V eta h (EquivariantPrismNonhorizontalCancellation.iteratedFacetMap (n - 1) N baseSimplex spatial' (Fin.cast ⋯ r))

A side simplex of a refined chart is the arbitrary side weight of its iterated spatial facet.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.refined_side_eq_arbitrarySpatialSideWeight_succ {n : ℕ} (hp : Nat.Prime (n + 1 + 1)) (N L : ℕ) (V : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → Realization (n + 1 + 1) × ↑(Set.Icc 0 1)) → ZMod (n + 1 + 1)) (orbit : PrimeOrbitCycle.TopOrbit hp) (spatial : RefinementWord (n + 1 + 1) N) (eta : Fin L → Equiv.Perm (Fin (n + 1 + 1))) (r : Fin (n + 1 + 1)) (h : Fin (n + 1)) : (V fun (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1))) => EquivariantPrismNonhorizontalCancellation.sidePrismMap (n + 1) (⇑(RefinedAffineMap.chart hp N (orbit, spatial))) r h ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (n + 1) L eta) x)) = arbitrarySpatialSideWeight hp L V eta h (EquivariantPrismNonhorizontalCancellation.iteratedFacetMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) spatial r)

Successor-dimensional arbitrary-weight side bridge, with transports normalized.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.arbitrarySpatialSide_weighted_boundary {n : ℕ} (hp : Nat.Prime (n + 1 + 1)) (N L : ℕ) (V : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → Realization (n + 1 + 1) × ↑(Set.Icc 0 1)) → ZMod (n + 1 + 1)) (eta : Fin L → Equiv.Perm (Fin (n + 1 + 1))) (h : Fin (n + 1)) (orbit : PrimeOrbitCycle.TopOrbit hp) : ∑ spatial : RefinementWord (n + 1 + 1) N, EquivariantPrismNonhorizontalCancellation.iteratedSign (ZMod (n + 1 + 1)) N spatial * ∑ r : Fin (n + 1 + 1), SimplicialChain.faceSign r * arbitrarySpatialSideWeight hp L V eta h (EquivariantPrismNonhorizontalCancellation.iteratedFacetMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) spatial r) = ∑ j : Fin (n + 1 + 1), SimplicialChain.faceSign j * ∑ theta : Fin N → Equiv.Perm (Fin (n + 1)), EquivariantPrismNonhorizontalCancellation.iteratedSign (ZMod (n + 1 + 1)) N theta * arbitrarySpatialSideWeight hp L V eta h (EquivariantPrismNonhorizontalCancellation.iteratedBoundaryMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) j theta)

Spatial subdivision boundary identity for an arbitrary fixed side weight.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.arbitrarySpatialSide_scaled_boundary {n : ℕ} (hp : Nat.Prime (n + 1 + 1)) (N L : ℕ) (V : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (n + 1)) → Realization (n + 1 + 1) × ↑(Set.Icc 0 1)) → ZMod (n + 1 + 1)) (eta : Fin L → Equiv.Perm (Fin (n + 1 + 1))) (h : Fin (n + 1)) (orbit : PrimeOrbitCycle.TopOrbit hp) : ∑ spatial : RefinementWord (n + 1 + 1) N, ∑ r : Fin (n + 1 + 1), (PrimeOrbitCycle.orbitCycle hp).coefficient orbit * EquivariantPrismNonhorizontalCancellation.iteratedSign (ZMod (n + 1 + 1)) N spatial * (EquivariantPrismNonhorizontalCancellation.iteratedSign (ZMod (n + 1 + 1)) L eta * (SimplicialChain.faceSign r * ((-1) ^ ↑h * arbitrarySpatialSideWeight hp L V eta h (EquivariantPrismNonhorizontalCancellation.iteratedFacetMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) spatial r)))) = (PrimeOrbitCycle.orbitCycle hp).coefficient orbit * EquivariantPrismNonhorizontalCancellation.iteratedSign (ZMod (n + 1 + 1)) L eta * (-1) ^ ↑h * ∑ j : Fin (n + 1 + 1), SimplicialChain.faceSign j * ∑ theta : Fin N → Equiv.Perm (Fin (n + 1)), EquivariantPrismNonhorizontalCancellation.iteratedSign (ZMod (n + 1 + 1)) N theta * arbitrarySpatialSideWeight hp L V eta h (EquivariantPrismNonhorizontalCancellation.iteratedBoundaryMap n N (⇑(ReferenceAffineOrbitCount.topRepr hp orbit).realizationContinuousMap) j theta)

Scaled form of the arbitrary spatial side boundary identity used in the final orbit sum.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.occurrencePairing_side_eq_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (hW : ∀ (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)), W (translateFacetMap p g tau) = W tau) : occurrencePairing hp N L (sideMapWeight W) = 0

The nonhorizontal part of every prime-invariant facet-map weight pairs trivially with the refined prism boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.occurrencePairing_eq_upper_sub_lower {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (W : (↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)) → ZMod p) (hW : ∀ (g : ↥(PrimeSymmetry p)) (tau : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p × ↑(Set.Icc 0 1)), W (translateFacetMap p g tau) = W tau) : occurrencePairing hp N L W = upperEndpointPairing hp N L W - lowerEndpointPairing hp N L W

Arbitrary prime-invariant weighted boundary formula for the fully refined middle prism.

Pointwise middle-prism collar

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.lowerBoundaryCoefficient {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) : ZMod p

Lower boundary coefficient of one middle-prism facet orbit.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.upperBoundaryCoefficient {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) : ZMod p

Upper boundary coefficient of one middle-prism facet orbit.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.facetIncidence_eq_occurrencePairing {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) : (Cells hp N L).facetIncidence s = occurrencePairing hp N L (facetOrbitIndicator hp N L s)

The explicit facet incidence is the arbitrary occurrence pairing evaluated at the orbit characteristic weight.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.isLowerFacet_of_indicator_lower_ne_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) (h : facetOrbitIndicator hp N L s (EquivariantPrismNonhorizontalCancellation.lowerEndpointMap sigma) ≠ 0) : (Cells hp N L).IsLowerFacet s

If a lower endpoint map belongs to an orbit facet, that facet is lower horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.isUpperFacet_of_indicator_upper_ne_zero {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) (sigma : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1)) → Realization p) (h : facetOrbitIndicator hp N L s (EquivariantPrismNonhorizontalCancellation.upperEndpointMap sigma) ≠ 0) : (Cells hp N L).IsUpperFacet s

If an upper endpoint map belongs to an orbit facet, that facet is upper horizontal.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.lowerBoundaryCoefficient_zero_of_not_lower {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) (hs : ¬(Cells hp N L).IsLowerFacet s) : lowerBoundaryCoefficient hp N L s = 0

Lower boundary coefficients vanish away from the lower horizontal boundary.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.upperBoundaryCoefficient_zero_of_not_upper {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (s : (Cells hp N L).Facet) (hs : ¬(Cells hp N L).IsUpperFacet s) : upperBoundaryCoefficient hp N L s = 0

Upper boundary coefficients vanish away from the upper horizontal boundary.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismBoundary.collar {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp (N + L) (N + L) (N + L) L

The common-level staircase prism, with its boundary understood pointwise on prime-orbit facets.

Equations

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