Facet extensions and shuffles

For a codimension-one Fox--Neuwirth cell, the labels form two ordered blocks. A containing top cell is exactly an order-preserving interleaving of these blocks, hence is determined by the set of positions occupied by the first block. This module constructs the inverse interleaving, proves the resulting equivalence with ShuffleIndex, and closes the genuine cellular-cycle calculation modulo a prime.

noncomputable def NRR.FoxNeuwirth.facetLabelSumEquiv {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : Fin p ≃ Fin (facetLeftSize hp a ha) ⊕ Fin (p - facetLeftSize hp a ha)

A codimension-one facet has two blocks; this equivalence records the old rank inside the left or right block.

Equations

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

theorem NRR.FoxNeuwirth.shuffle_compl_card {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) : (↑s)ᶜ.card = p - facetLeftSize hp a ha

The complement of a shuffle has the complementary cardinality.

noncomputable def NRR.FoxNeuwirth.shuffleMergeEquiv {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) : Fin (facetLeftSize hp a ha) ⊕ Fin (p - facetLeftSize hp a ha) ≃ Fin p

Increasing merge of the two ordered blocks into the positions selected by a shuffle.

Equations

• NRR.FoxNeuwirth.shuffleMergeEquiv hp a ha s = finSumEquivOfFinset ⋯ ⋯

noncomputable def NRR.FoxNeuwirth.shuffleRank {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) : Equiv.Perm (Fin p)

The top-cell rank obtained by interleaving the two ordered blocks according to s.

Equations

• NRR.FoxNeuwirth.shuffleRank hp a ha s = (NRR.FoxNeuwirth.facetLabelSumEquiv hp a ha).trans (NRR.FoxNeuwirth.shuffleMergeEquiv hp a ha s)

theorem NRR.FoxNeuwirth.shuffleRank_apply_left {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) (i : Fin p) (hi : ↑(a.rank i) < facetLeftSize hp a ha) : (shuffleRank hp a ha s) i = ((↑s).orderEmbOfFin ⋯) ⟨↑(a.rank i), hi⟩

On a first-block label, shuffleRank is the increasing enumeration of the selected positions.

theorem NRR.FoxNeuwirth.shuffleRank_apply_right {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) (i : Fin p) (hi : ¬↑(a.rank i) < facetLeftSize hp a ha) : (shuffleRank hp a ha s) i = ((↑s)ᶜ.orderEmbOfFin ⋯) ⟨↑(a.rank i) - facetLeftSize hp a ha, ⋯⟩

On a second-block label, shuffleRank is the increasing enumeration of the complementary positions.

theorem NRR.FoxNeuwirth.sameBlock_iff_same_side {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (i j : Fin p) : a.SameBlock i j ↔ (↑(a.rank i) < facetLeftSize hp a ha ↔ ↑(a.rank j) < facetLeftSize hp a ha)

In a codimension-one cell, two labels are in the same block exactly when their old ranks lie on the same side of the unique bar.

theorem NRR.FoxNeuwirth.shuffleRank_preserves_sameBlock_order {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) (i j : Fin p) (hij : a.SameBlock i j) : ↑(a.rank i) < ↑(a.rank j) ↔ ↑((shuffleRank hp a ha s) i) < ↑((shuffleRank hp a ha s) j)

The shuffle merge preserves the old order inside each of the two facet blocks.

theorem NRR.FoxNeuwirth.shuffleTopCell_isFacet {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) : a.IsFacet ↑(BarredPermutation.TopCell.ofPerm (shuffleRank hp a ha s))

The merged permutation is a top-cell extension of the original facet.

noncomputable def NRR.FoxNeuwirth.shuffleToTopExtension {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : ShuffleIndex p (facetLeftSize hp a ha) → TopExtension a

Inverse construction: merge the two ordered blocks according to the chosen shuffle.

Equations

• NRR.FoxNeuwirth.shuffleToTopExtension hp a ha s = ⟨NRR.BarredPermutation.TopCell.ofPerm (NRR.FoxNeuwirth.shuffleRank hp a ha s), ⋯⟩

theorem NRR.FoxNeuwirth.firstBlockPositions_shuffleToTopExtension {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) : firstBlockPositions hp a ha ↑(shuffleToTopExtension hp a ha s) = ↑s

The first-block positions of the constructed extension are the prescribed shuffle.

@[simp]

theorem NRR.FoxNeuwirth.topExtensionToShuffle_shuffleToTopExtension {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (s : ShuffleIndex p (facetLeftSize hp a ha)) : topExtensionToShuffle hp a ha (shuffleToTopExtension hp a ha s) = s

theorem NRR.FoxNeuwirth.topExtension_preserves_sameBlock_order {p : ℕ} (a : BarredPermutation p) (c : TopExtension a) (i j : Fin p) (hij : a.SameBlock i j) : ↑(a.rank i) < ↑(a.rank j) ↔ ↑((↑↑c).rank i) < ↑((↑↑c).rank j)

A top-cell extension is order-preserving on each facet block.

theorem NRR.FoxNeuwirth.rank_mem_firstBlockPositions_iff {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : TopExtension a) (i : Fin p) : (↑↑c).rank i ∈ firstBlockPositions hp a ha ↑c ↔ ↑(a.rank i) < facetLeftSize hp a ha

A label occupies a first-block position in an extension exactly when it belongs to the first block of the facet.

noncomputable def NRR.FoxNeuwirth.topExtensionLeftOrderEmb {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : TopExtension a) : Fin (facetLeftSize hp a ha) ↪o Fin p

The first-block restriction of a top-cell extension, indexed by old rank.

Equations

• NRR.FoxNeuwirth.topExtensionLeftOrderEmb hp a ha c = { toFun := fun (r : Fin (NRR.FoxNeuwirth.facetLeftSize hp a ha)) => (↑↑c).rank ((Equiv.symm a.rank) ⟨↑r, ⋯⟩), inj' := ⋯, map_rel_iff' := ⋯ }

theorem NRR.FoxNeuwirth.topExtensionLeftOrderEmb_mem {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : TopExtension a) (r : Fin (facetLeftSize hp a ha)) : (topExtensionLeftOrderEmb hp a ha c) r ∈ firstBlockPositions hp a ha ↑c

The first-block restriction lands in the first-block position finset.

theorem NRR.FoxNeuwirth.topExtension_left_rank_eq_orderEmb {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : TopExtension a) (i : Fin p) (hi : ↑(a.rank i) < facetLeftSize hp a ha) : (↑↑c).rank i = ((firstBlockPositions hp a ha ↑c).orderEmbOfFin ⋯) ⟨↑(a.rank i), hi⟩

The increasing enumeration of first-block positions agrees with every top-cell extension.

theorem NRR.FoxNeuwirth.card_compl_firstBlockPositions {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : TopExtension a) : (firstBlockPositions hp a ha ↑c)ᶜ.card = p - facetLeftSize hp a ha

The complement of the first-block position set has the size of the second block.

noncomputable def NRR.FoxNeuwirth.topExtensionRightOrderEmb {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : TopExtension a) : Fin (p - facetLeftSize hp a ha) ↪o Fin p

The second-block restriction of a top-cell extension, indexed by old rank within that block.

Equations

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

theorem NRR.FoxNeuwirth.topExtensionRightOrderEmb_mem {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : TopExtension a) (r : Fin (p - facetLeftSize hp a ha)) : (topExtensionRightOrderEmb hp a ha c) r ∈ (firstBlockPositions hp a ha ↑c)ᶜ

The second-block restriction lands in the complementary position finset.

theorem NRR.FoxNeuwirth.topExtension_right_rank_eq_orderEmb {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) (c : TopExtension a) (i : Fin p) (hi : ¬↑(a.rank i) < facetLeftSize hp a ha) : (↑↑c).rank i = ((firstBlockPositions hp a ha ↑c)ᶜ.orderEmbOfFin ⋯) ⟨↑(a.rank i) - facetLeftSize hp a ha, ⋯⟩

The increasing enumeration of complementary positions agrees with every top-cell extension.

theorem NRR.FoxNeuwirth.topExtensionToShuffle_injective {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : Function.Injective (topExtensionToShuffle hp a ha)

Two extensions with the same first-block position set are equal.

theorem NRR.FoxNeuwirth.topExtensionToShuffle_surjective {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : Function.Surjective (topExtensionToShuffle hp a ha)

Every shuffle is realized by its canonical order-preserving merge.

noncomputable def NRR.FoxNeuwirth.facetShuffleEquiv {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) (ha : a.dualDimension = p - 2) : TopExtension a ≃ ShuffleIndex p (facetLeftSize hp a ha)

Canonical equivalence between top-cell extensions of a facet and its shuffles.

Equations

• NRR.FoxNeuwirth.facetShuffleEquiv hp a ha = Equiv.ofBijective (NRR.FoxNeuwirth.topExtensionToShuffle hp a ha) ⋯

theorem NRR.FoxNeuwirth.facetShuffleBijection {p : ℕ} (hp : Nat.Prime p) : FacetShuffleBijection hp

The canonical extension-to-shuffle map is bijective.

theorem NRR.FoxNeuwirth.facetShuffleCardinality {p : ℕ} (hp : Nat.Prime p) : FacetShuffleCardinality p

Unconditional shuffle-cardinality formula for all prime facets.

theorem NRR.FoxNeuwirth.actualTopBoundaryCoefficient_eq_zero_prime {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) : actualTopBoundaryCoefficient a = 0

Every actual cellular boundary coefficient vanishes modulo the prime.

noncomputable def NRR.FoxNeuwirth.primeActualFiniteIncidenceCycle {p : ℕ} (hp : Nat.Prime p) : FiniteIncidenceCycle (ZMod p)

The genuine top-cell incidence sum is an unconditional finite cycle modulo a prime.

Equations

• NRR.FoxNeuwirth.primeActualFiniteIncidenceCycle hp = NRR.FoxNeuwirth.actualFiniteIncidenceCycle hp ⋯