Canonical endpoint occurrences of the common-level middle prism

This module contains only the geometry of the lower and upper endpoint facets. It is deliberately independent of the stable endpoint interpolation and global Stokes modules, so both can use the same endpoint cells without an import cycle.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerStaircaseIndex {p : ℕ} (hp : Nat.Prime p) : Fin p

Final staircase simplex. Its final facet is the lower horizontal copy.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerStaircaseIndex hp = ⟨p - 1, ⋯⟩

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerStaircaseIndex_val {p : ℕ} (hp : Nat.Prime p) : ↑(lowerStaircaseIndex hp) = p - 1

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerStaircaseFacet_indices {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (j : Fin (p + 1)) (h : ∀ (i : Fin p), SubdivisionPrismCharts.staircaseTime k (j.succAbove i) = 0) : k = lowerStaircaseIndex hp ∧ j = Fin.last p

In an unrefined staircase simplex, a facet is entirely at time zero only when it is the final facet of the final staircase simplex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.upperStaircaseFacet_indices {p : ℕ} (hp : Nat.Prime p) (k : Fin p) (j : Fin (p + 1)) (h : ∀ (i : Fin p), SubdivisionPrismCharts.staircaseTime k (j.succAbove i) = 1) : k = ⟨0, ⋯⟩ ∧ j = 0

In an unrefined staircase simplex, a facet is entirely at time one only when it is the initial facet of the initial staircase simplex.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerPrismCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : SubdivisionPrismCharts.PrismCell hp N L

Refined prism cell whose endpoint face is the lower boundary simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.upperPrismCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : SubdivisionPrismCharts.PrismCell hp N L

Refined prism cell whose endpoint face is the upper boundary simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerOccurrence {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : (RelativeCollarMiddlePrism.cellSystem hp N L).FacetOccurrence

Canonical lower horizontal facet occurrence.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.upperOccurrence {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : (RelativeCollarMiddlePrism.cellSystem hp N L).FacetOccurrence

Canonical upper horizontal facet occurrence.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerOccurrence_isLower {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : (RelativeCollarMiddlePrism.cellSystem hp N L).IsLowerFacetOccurrence (lowerOccurrence hp N L q eta)

The lower occurrence is horizontal at time zero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.upperOccurrence_isUpper {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : (RelativeCollarMiddlePrism.cellSystem hp N L).IsUpperFacetOccurrence (upperOccurrence hp N L q eta)

The upper occurrence is horizontal at time one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerOccurrenceFacetMap_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap hp N L (lowerOccurrence hp N L q eta) = EquivariantPrismNonhorizontalCancellation.lowerEndpointMap (EquivariantPrismHorizontalEndpointIdentification.endpointSpatialMap hp N L q eta)

The actual lower occurrence map is the refined spatial endpoint map at time zero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.upperOccurrenceFacetMap_eq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : EquivariantPrismNonhorizontalCancellation.occurrenceFacetMap hp N L (upperOccurrence hp N L q eta) = EquivariantPrismNonhorizontalCancellation.upperEndpointMap (EquivariantPrismHorizontalEndpointIdentification.endpointSpatialMap hp N L q eta)

The actual upper occurrence map is the refined spatial endpoint map at time one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.lowerOccurrence_facetSignature {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) (i : Fin p) : (RelativeCollarMiddlePrism.cellSystem hp N L).facetSignature (lowerOccurrence hp N L q eta) i = ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp (N + L) (EndpointFaceRefinement.endpointTopCell hp N L q eta) (Fin.cast ⋯ i))

Vertex-signature form of the lower endpoint identity.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarMiddlePrismEndpointsCore.upperOccurrence_facetSignature {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) (i : Fin p) : (RelativeCollarMiddlePrism.cellSystem hp N L).facetSignature (upperOccurrence hp N L q eta) i = ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp (N + L) (EndpointFaceRefinement.endpointTopCell hp N L q eta) (Fin.cast ⋯ i))

Vertex-signature form of the upper endpoint identity.