Refinement words carried by a prescribed boundary face

A barycentric refinement word on a p - 1 dimensional endpoint simplex must be lifted to the ambient p dimensional prism simplex. At refinement level zero the endpoint is an original staircase facet. After one or more barycentric refinements, each endpoint summand appears as the last facet of an ambient barycentric simplex. This module supplies the corresponding ambient permutations and proves the affine compatibility identity used by both the stable endpoint interpolant and the explicit middle collar.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.extendSpatialPermutation {p : ℕ} (pi : Equiv.Perm (Fin p)) : Equiv.Perm (Fin (p + 1))

Extend a spatial permutation by fixing the interval vertex.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.extendSpatialRefinementWord {p : ℕ} (L : ℕ) (eta : RefinementWord p L) : SubdivisionPrismCharts.PrismRefinementWord p L

Extend every permutation in a spatial refinement word while fixing the interval vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.extendSpatialPermutation_eq_lastFaceEquiv (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) : extendSpatialPermutation pi = (SphereOddDegree.AffineBarycentricSubdivision.lastFaceEquiv n) (Fin.last (n + 1), pi)

The block extension is the last-face permutation associated with the final boundary face.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.affineCompMap_extendSpatialRefinementWord_lastFace (n L : ℕ) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : (SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (n + 1) L (extendSpatialRefinementWord L eta)) (EquivariantPrismNonhorizontalCancellation.cofacePoint n (Fin.last (n + 1)) x) = EquivariantPrismNonhorizontalCancellation.cofacePoint n (Fin.last (n + 1)) ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n L eta) x)

Iterated block extension carries the final facet of the refined ambient simplex to the corresponding iterated refinement of the final boundary face.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftFacePermutation (n : ℕ) (j : Fin (n + 2)) (pi : Equiv.Perm (Fin (n + 1))) : Equiv.Perm (Fin (n + 2))

Lift a refinement permutation of one boundary face to an ambient permutation whose final facet is that boundary face.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftFacePermutation_eq_lastFaceEquiv (n : ℕ) (j : Fin (n + 2)) (pi : Equiv.Perm (Fin (n + 1))) : liftFacePermutation n j pi = (SphereOddDegree.AffineBarycentricSubdivision.lastFaceEquiv n) (j, pi)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftFaceRefinementWord (n L : ℕ) (j : Fin (n + 2)) (eta : Fin L → Equiv.Perm (Fin (n + 1))) : Fin L → Equiv.Perm (Fin (n + 2))

Lift the first permutation to the prescribed original face; subsequent permutations preserve the canonical last face of the already-refined simplex.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftFaceRefinementWord n 0 j eta_2 = fun (r : Fin 0) => r.elim0

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointOmitted (n L : ℕ) : Fin (n + 2) → Fin (n + 2)

The facet omitted by the canonical endpoint occurrence. Without further subdivision it is the original face j; after at least one subdivision it is the final facet of a barycentric simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointOmitted n 0 x✝ = x✝
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointOmitted n n_1.succ x✝ = Fin.last (n + 1)

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.affineCompMap_liftFaceRefinementWord (n L : ℕ) (j : Fin (n + 2)) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : (SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (n + 1) L (liftFaceRefinementWord n L j eta)) (EquivariantPrismNonhorizontalCancellation.cofacePoint n (endpointOmitted n L j) x) = EquivariantPrismNonhorizontalCancellation.cofacePoint n j ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n L eta) x)

Iterated lifted refinement realizes the requested refined original boundary face.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftBoundaryPermutation {p : ℕ} (j : Fin (p + 1)) (pi : Equiv.Perm (Fin p)) : Equiv.Perm (Fin (p + 1))

Last-face lifting for a boundary face of Fin (p + 1), without exposing predecessor casts in subsequent definitions.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftBoundaryPermutation j_2 pi_2 = Equiv.refl (Fin 1)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftBoundaryRefinementWord {p : ℕ} (L : ℕ) (j : Fin (p + 1)) (eta : RefinementWord p L) : SubdivisionPrismCharts.PrismRefinementWord p L

Lift an endpoint refinement word to the ambient prism simplex.

Equations

• One or more equations did not get rendered due to their size.
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftBoundaryRefinementWord 0 j eta_2 = fun (r : Fin 0) => r.elim0

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointOmittedPrime {p : ℕ} (L : ℕ) (j : Fin (p + 1)) : Fin (p + 1)

Facet omitted by a canonical endpoint occurrence.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointOmittedPrime 0 j = j
• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointOmittedPrime n.succ j = Fin.last p

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftBoundaryPermutation_eq_liftFacePermutation (n : ℕ) (j : Fin (n + 2)) (pi : Equiv.Perm (Fin (n + 1))) : liftBoundaryPermutation j pi = liftFacePermutation n j pi

The generic lift agrees with the standard last-face decomposition in successor dimensions.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.liftBoundaryRefinementWord_eq_liftFaceRefinementWord (n L : ℕ) (j : Fin (n + 2)) (eta : Fin L → Equiv.Perm (Fin (n + 1))) : liftBoundaryRefinementWord L j eta = liftFaceRefinementWord n L j eta

In successor dimensions, the generic boundary word is the canonical face-refinement word.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointOmittedPrime_eq_endpointOmitted (n L : ℕ) (j : Fin (n + 2)) : endpointOmittedPrime L j = endpointOmitted n L j

In successor dimensions, the two canonical omitted-index descriptions agree.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.affineCompMap_liftBoundaryRefinementWord (n L : ℕ) (j : Fin (n + 2)) (eta : Fin L → Equiv.Perm (Fin (n + 1))) (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta n)) : (SphereOddDegree.AffineBarycentricSubdivision.affineCompMap (n + 1) L (liftBoundaryRefinementWord L j eta)) (EquivariantPrismNonhorizontalCancellation.cofacePoint n (endpointOmittedPrime L j) x) = EquivariantPrismNonhorizontalCancellation.cofacePoint n j ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n L eta) x)

A lifted endpoint refinement realizes the requested refined boundary face.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.splitRefinementWord {p : ℕ} (N L : ℕ) (rho : RefinementWord p (N + L)) : RefinementWord p N × RefinementWord p L

Split a refinement word of length N + L into its prefix and tail.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.appendRefinementWord {p : ℕ} (N L : ℕ) (rho : RefinementWord p N) (eta : RefinementWord p L) : RefinementWord p (N + L)

Concatenate two refinement words.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.appendRefinementWord N L rho eta i = Fin.addCases rho eta i

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.affineCompMap_append (n N L : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) (eta : Fin L → Equiv.Perm (Fin (n + 1))) : SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n (N + L) (appendRefinementWord N L rho eta) = (SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n N rho).comp (SphereOddDegree.AffineBarycentricSubdivision.affineCompMap n L eta)

Affine refinement along a concatenated word is tail refinement followed by prefix refinement.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.split_appendRefinementWord {p : ℕ} (N L : ℕ) (rho : RefinementWord p N) (eta : RefinementWord p L) : splitRefinementWord N L (appendRefinementWord N L rho eta) = (rho, eta)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.append_splitRefinementWord {p : ℕ} (N L : ℕ) (rho : RefinementWord p (N + L)) : appendRefinementWord N L (splitRefinementWord N L rho).1 (splitRefinementWord N L rho).2 = rho

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointTopCell {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : RefinedAffineMap.TopCell hp (N + L)

Reindex a horizontal endpoint simplex as a top cell at the combined refinement level.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.refinementIndexPerm_eq_endpointRefinementPerm {p : ℕ} (hp : Nat.Prime p) (sigma : Equiv.Perm (Fin p)) : Simplex.refinementIndexPerm sigma = EquivariantPrismHorizontalEndpointIdentification.endpointRefinementWord hp 1 (fun (x : Fin 1) => sigma) 0

For a prime cardinality, the chart's simplex-index transport is the endpoint transport.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointSpatialMap_eq_chart {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L) : EquivariantPrismHorizontalEndpointIdentification.endpointSpatialMap hp N L q eta = ⇑(RefinedAffineMap.chart hp (N + L) (endpointTopCell hp N L q eta))

The endpoint spatial map is the ordinary chart at the combined refinement level.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointFaceRefinement.endpointTopCell_surjective {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : RefinedAffineMap.TopCell hp (N + L)) : ∃ (q₀ : RefinedAffineMap.TopCell hp N) (eta : RefinementWord p L), endpointTopCell hp N L q₀ eta = q

Every combined-level top cell has a split endpoint representation.