Shuffles

A (p, q)-shuffle is an injective monotone map Fin (p + q + 1) → Fin (p + 1) × Fin (q + 1), i.e. a lattice path from (0, 0) to (p, q) taking unit left and right steps. This file develops the combinatorics of shuffles needed for the Eilenberg–Zilber shuffle map: inversion counts and signs, the boundary decomposition of a shuffle into insertions of left/right steps, and the sign-reversing involution swapDiagonalSteps that cancels the diagonal boundary terms.

Shuffles

@[reducible, inline]

abbrev LeanPool.EilenbergZilber.Index (k : ℕ) : Type

The finite chain object 0 ≤ 1 ≤ ··· ≤ k in PoSet, represented by Fin (k+1).

Equations

• LeanPool.EilenbergZilber.Index k = Fin (k + 1)

@[reducible, inline]

abbrev LeanPool.EilenbergZilber.Shuffle (p q : ℕ) : Type

A (p,q)-shuffle as an injective monotone map Index (p + q) ⟶ Index p × Index q in PoSet.

Equations

• LeanPool.EilenbergZilber.Shuffle p q = { φ : LeanPool.EilenbergZilber.Index (p + q) →o LeanPool.EilenbergZilber.Index p × LeanPool.EilenbergZilber.Index q // Function.Injective ⇑φ }

@[instance_reducible]

noncomputable instance LeanPool.EilenbergZilber.Shuffle.instFintype (p q : ℕ) : Fintype (Shuffle p q)

There are finitely many (p,q)-shuffles: exactly Nat.choose (p + q) p.

Equations

• LeanPool.EilenbergZilber.Shuffle.instFintype p q = Fintype.ofFinite (LeanPool.EilenbergZilber.Shuffle p q)

def LeanPool.EilenbergZilber.Shuffle.invCount {p q : ℕ} (μ : Shuffle p q) : ℕ

The number of inversions of a shuffle.

Equations

• μ.invCount = ∑ r : Fin (p + q), if (↑μ r.castSucc).1 < (↑μ r.succ).1 then ↑(↑μ r.castSucc).2 else 0

def LeanPool.EilenbergZilber.Shuffle.sign {p q : ℕ} (μ : Shuffle p q) : ℤ

The sign of a shuffle: (-1)^k where k is the number of inversions.

Equations

• μ.sign = (-1) ^ μ.invCount

def LeanPool.EilenbergZilber.Shuffle.swap {p q : ℕ} (μ : Shuffle p q) : Shuffle q p

Swap the two coordinates of a shuffle, yielding a (q,p)-shuffle.

Equations

• μ.swap = ⟨{ toFun := fun (x : LeanPool.EilenbergZilber.Index (q + p)) => (↑μ ((Fin.castOrderIso ⋯) x)).swap, monotone' := ⋯ }, ⋯⟩

@[simp]

theorem LeanPool.EilenbergZilber.Shuffle.swap_swap {p q : ℕ} (μ : Shuffle p q) : μ.swap.swap = μ

def LeanPool.EilenbergZilber.Shuffle.swapEquiv (p q : ℕ) : Shuffle p q ≃ Shuffle q p

Swapping coordinates gives an equivalence Shuffle p q ≃ Shuffle q p.

Equations

• LeanPool.EilenbergZilber.Shuffle.swapEquiv p q = { toFun := LeanPool.EilenbergZilber.Shuffle.swap, invFun := LeanPool.EilenbergZilber.Shuffle.swap, left_inv := ⋯, right_inv := ⋯ }

Lattice path structure

theorem LeanPool.EilenbergZilber.Shuffle.coordSum_eq {p q : ℕ} (u : Shuffle p q) (r : Fin (p + q + 1)) : ↑(↑u r).1 + ↑(↑u r).2 = ↑r

At every position r, the coordinate sum equals r.val.

theorem LeanPool.EilenbergZilber.Shuffle.exists_snd_step {p q : ℕ} (μ : Shuffle p q) (i : ℕ) (hi : i + 1 ≤ q) : ∃ (a : Fin (p + q)), ↑(↑μ a.castSucc).2 = i ∧ ↑(↑μ a.succ).2 = i + 1 ∧ (↑μ a.castSucc).1 = (↑μ a.succ).1

A shuffle path crosses every intermediate snd-level: for i + 1 ≤ q there is a step a that is a q-step at level i — the second coordinate goes i → i + 1 while the first coordinate is fixed. This is the degeneracy analog of the face-insertion step lemmas, and is what lets the Eilenberg–Zilber map carry a one-direction degeneracy to a diagonal one.

theorem LeanPool.EilenbergZilber.Shuffle.exists_fst_step {p q : ℕ} (μ : Shuffle p q) (i : ℕ) (hi : i + 1 ≤ p) : ∃ (a : Fin (p + q)), ↑(↑μ a.castSucc).1 = i ∧ ↑(↑μ a.succ).1 = i + 1 ∧ (↑μ a.castSucc).2 = (↑μ a.succ).2

The first-coordinate analog of exists_snd_step: for i + 1 ≤ p there is a p-step at level i — the first coordinate goes i → i + 1 while the second coordinate is fixed. Used for the outer (horizontal) Eilenberg–Zilber degeneracy kill.

theorem LeanPool.EilenbergZilber.Shuffle.apply_zero {p q : ℕ} (u : Shuffle p q) : ↑u 0 = (0, 0)

theorem LeanPool.EilenbergZilber.Shuffle.apply_last {p q : ℕ} (u : Shuffle p q) : ↑u (Fin.last (p + q)) = (Fin.last p, Fin.last q)

theorem LeanPool.EilenbergZilber.Shuffle.invCount_eq_sum_mul_diff {p q : ℕ} (u : Shuffle p q) : u.invCount = ∑ r : Fin (p + q), ↑(↑u r.castSucc).2 * (↑(↑u r.succ).1 - ↑(↑u r.castSucc).1)

theorem LeanPool.EilenbergZilber.Shuffle.swap_invCount_eq_sum_mul_diff {p q : ℕ} (u : Shuffle p q) : u.swap.invCount = ∑ r : Fin (p + q), ↑(↑u r.castSucc).1 * (↑(↑u r.succ).2 - ↑(↑u r.castSucc).2)

theorem LeanPool.EilenbergZilber.Shuffle.xy_diff_eq_sum_mixed {p q : ℕ} (u : Shuffle p q) (r : Fin (p + q)) : ↑(↑u r.succ).1 * ↑(↑u r.succ).2 - ↑(↑u r.castSucc).1 * ↑(↑u r.castSucc).2 = ↑(↑u r.castSucc).2 * (↑(↑u r.succ).1 - ↑(↑u r.castSucc).1) + ↑(↑u r.castSucc).1 * (↑(↑u r.succ).2 - ↑(↑u r.castSucc).2)

theorem LeanPool.EilenbergZilber.Shuffle.invCount_add_invCount_swap {p q : ℕ} (u : Shuffle p q) : u.invCount + u.swap.invCount = p * q

theorem LeanPool.EilenbergZilber.Shuffle.sign_eq_negOnePow_mul_swap_sign {p q : ℕ} (u : Shuffle p q) : u.sign = (-1) ^ (p * q) * u.swap.sign

Swapping a (p,q)-shuffle changes the sign by the Koszul factor (-1)^(p*q).

Shuffle (0,0)

theorem LeanPool.EilenbergZilber.Shuffle.unique_0_0 (μ : Shuffle 0 0) : ↑μ = { toFun := fun (x : Index (0 + 0)) => (0, 0), monotone' := ⋯ }

For Shuffle 0 0, the domain and codomain are both Fin 1, so every shuffle has the same underlying map: the unique monotone injection to (0, 0).

instance LeanPool.EilenbergZilber.Shuffle.subsingleton_0_0 : Subsingleton (Shuffle 0 0)

There is exactly one (0,0)-shuffle.

def LeanPool.EilenbergZilber.Shuffle.trivialShuffle (r m : ℕ) : Shuffle r m

The staircase (r,m)-shuffle k ↦ (min(k,r), k - r): it goes right r steps then up m steps (the lexicographically smallest shuffle path). Its front-r face and back-m face recover the identity, so it is the unique shuffle contributing the identity summand to the diagonal Eilenberg–Zilber/Alexander–Whitney pairing.

Equations

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

@[simp]

theorem LeanPool.EilenbergZilber.Shuffle.trivialShuffle_apply (r m : ℕ) (k : Index (r + m)) : ↑(trivialShuffle r m) k = (⟨min (↑k) r, ⋯⟩, ⟨↑k - r, ⋯⟩)

The coordinates of the staircase shuffle: fst = min(·, r), snd = · - r.

theorem LeanPool.EilenbergZilber.Shuffle.sign_trivialShuffle (r m : ℕ) : (trivialShuffle r m).sign = 1

The staircase shuffle has no inversions, hence sign 1.

Face-shuffle decomposition (Leibniz rule infrastructure)

Why "remove step" doesn't work. An earlier attempt defined removeLeftStep μ r by removing vertex r from the shuffle path whenever step r is a left step. This is wrong: the face map δ_r removes vertex r, which merges the steps on either side of r. If those steps have different types (one left, one right), the merged step is a diagonal (both coordinates increase), which cannot be a valid shuffle step.

Example: the (1,1)-shuffle (0,0) → (1,0) → (1,1) has step 0 = Left, step 1 = Right. Removing vertex 1 = (1,0) gives (0,0) → (1,1), a diagonal. This doesn't factor as ν ≫ (δⱼ × id) for any shuffle ν. The factorization only works for "LL" vertices (both adjacent steps are left) or "RR" vertices.

The insert approach. Instead of decomposing the LHS face terms, we work from the RHS and inject into the LHS. Given a (p, q+1)-shuffle ν and a face index j : Fin (p+2), we construct a (p+1, q+1)-shuffle insertLeftStep ν j by lifting ν's first coordinate via Fin.succAbove j (skipping value j) and inserting a new left step where the first coordinate crosses j.

The proof of universalSimplexCrossProduct_boundary then proceeds:

1. Show the RHS terms inject into the LHS via insertLeftStep / insertRightStep.
2. Show the remaining LHS terms (diagonal terms) cancel via a sign-reversing involution swapDiagonalSteps.

def LeanPool.EilenbergZilber.Shuffle.isLeftStep {p q : ℕ} (μ : Shuffle p q) (r : Fin (p + q)) : Prop

Whether step r of shuffle μ is a "left step" (first coordinate increments).

Equations

• μ.isLeftStep r = (↑(↑μ r.castSucc).1 < ↑(↑μ r.succ).1)

@[instance_reducible]

instance LeanPool.EilenbergZilber.Shuffle.decidableIsLeftStep {p q : ℕ} (μ : Shuffle p q) (r : Fin (p + q)) : Decidable (μ.isLeftStep r)

Equations

• μ.decidableIsLeftStep r = { decide := (↑(↑μ r.castSucc).1).succ.ble ↑(↑μ r.succ).1, reflects_decide := ⋯ }

Insertion indices

def LeanPool.EilenbergZilber.Shuffle.insertLeftIndex {p q : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) : Fin (p + q + 2)

The vertex index in the (p+1, q)-shuffle's domain where the new left step was inserted. Removing this vertex via δ recovers the original shuffle. Equals the number of vertices of ν whose first coordinate is < j.

Equations

• ν.insertLeftIndex j = ⟨{r : Fin (p + q + 1) | ↑(↑ν r).1 < ↑j}.card, ⋯⟩

def LeanPool.EilenbergZilber.Shuffle.insertRightIndex {p q : ℕ} (ν : Shuffle p q) (k : Fin (q + 2)) : Fin (p + q + 2)

The vertex index where the new right step was inserted. Equals the number of vertices of ν whose second coordinate is < k.

Equations

• ν.insertRightIndex k = ⟨{r : Fin (p + q + 1) | ↑(↑ν r).2 < ↑k}.card, ⋯⟩

Insertion helpers

theorem LeanPool.EilenbergZilber.Shuffle.insertLeftIndex_le {p q : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) : ↑(ν.insertLeftIndex j) ≤ ↑j + q

The insertion index satisfies t ≤ j + q: vertices with fst < j have index ≤ (j-1) + q by coordSum_eq, so there are at most j + q of them.

Insertion maps (RHS → LHS direction)

noncomputable def LeanPool.EilenbergZilber.Shuffle.insertLeftStepFun {p q : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) : Fin (p + 1 + q + 1) → Index (p + 1) × Index q

The underlying piecewise map for insertLeftStep: before the insertion point, embed the original vertex via succAbove j; at the insertion point, place (j, t-j); after the insertion point, embed the shifted-back vertex via succAbove j.

Equations

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

noncomputable def LeanPool.EilenbergZilber.Shuffle.insertLeftStep {p q : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) : Shuffle (p + 1) q

Insert a left step at face index j, turning a (p, q)-shuffle into a (p+1, q)-shuffle. The original path from (0,0) to (p, q) is embedded into a path from (0,0) to (p+1, q) by applying Fin.succAbove j to the first coordinate and inserting a new left step where the first coordinate crosses j.

Equations

• ν.insertLeftStep j = ⟨{ toFun := ν.insertLeftStepFun j, monotone' := ⋯ }, ⋯⟩

noncomputable def LeanPool.EilenbergZilber.Shuffle.insertRightStepFun {p q : ℕ} (ν : Shuffle p q) (k : Fin (q + 2)) : Fin (p + (q + 1) + 1) → Index p × Index (q + 1)

The underlying piecewise map for insertRightStep: before the insertion point, embed the original vertex via succAbove k on the second coordinate; at the insertion point, place (t-k, k); after the insertion point, embed the shifted-back vertex via succAbove k.

Equations

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

noncomputable def LeanPool.EilenbergZilber.Shuffle.insertRightStep {p q : ℕ} (ν : Shuffle p q) (k : Fin (q + 2)) : Shuffle p (q + 1)

Insert a right step at face index k, turning a (p, q)-shuffle into a (p, q+1)-shuffle. Applies Fin.succAbove k to the second coordinate and inserts a new right step where the second coordinate crosses k.

Equations

• ν.insertRightStep k = ⟨{ toFun := ν.insertRightStepFun k, monotone' := ⋯ }, ⋯⟩

theorem LeanPool.EilenbergZilber.Shuffle.insertLeftStep_face {p q : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) (k : Index (p + q)) : ↑(ν.insertLeftStep j) (⟨↑(ν.insertLeftIndex j), ⋯⟩.succAbove (Fin.cast ⋯ k)) = (j.succAbove (↑ν k).1, (↑ν k).2)

Inserting a left step and removing the inserted vertex recovers the original shuffle with Fin.succAbove j applied to the first coordinate. (Purely combinatorial: no SimplexCategory or topology needed.)

theorem LeanPool.EilenbergZilber.Shuffle.insertRightStep_face {p q : ℕ} (ν : Shuffle p q) (k : Fin (q + 2)) (i : Index (p + q)) : ↑(ν.insertRightStep k) (⟨↑(ν.insertRightIndex k), ⋯⟩.succAbove (Fin.cast ⋯ i)) = ((↑ν i).1, k.succAbove (↑ν i).2)

Inserting a right step and removing the inserted vertex recovers the original shuffle with Fin.succAbove k applied to the second coordinate.

theorem LeanPool.EilenbergZilber.Shuffle.insertLeftStep_injective {p q : ℕ} (j₁ j₂ : Fin (p + 2)) (ν₁ ν₂ : Shuffle p q) (hμ : ν₁.insertLeftStep j₁ = ν₂.insertLeftStep j₂) (hr : ν₁.insertLeftIndex j₁ = ν₂.insertLeftIndex j₂) : j₁ = j₂ ∧ ν₁ = ν₂

The insert-left map (j, ν) ↦ (insertLeftStep ν j, insertLeftIndex ν j) is injective: distinct (j, ν) pairs produce distinct (μ, vertex) pairs.

theorem LeanPool.EilenbergZilber.Shuffle.insertRightStep_injective {p q : ℕ} (k₁ k₂ : Fin (q + 2)) (ν₁ ν₂ : Shuffle p q) (hμ : ν₁.insertRightStep k₁ = ν₂.insertRightStep k₂) (hr : ν₁.insertRightIndex k₁ = ν₂.insertRightIndex k₂) : k₁ = k₂ ∧ ν₁ = ν₂

The insert-right map is injective.

Helper lemmas for sign_insertLeftStep

The proof reduces to an inversion-count identity: inserting a left step at position j adds exactly t - j to the inversion count, where t = insertLeftIndex ν j. We split the invCount sum at t using Fin.sum_univ_succAbove, match the non-inserted terms against invCount ν, and compute the contribution of the inserted step directly.

theorem LeanPool.EilenbergZilber.Shuffle.sign_insertLeftStep {p q : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) : (ν.insertLeftStep j).sign * (-1) ^ ↑(ν.insertLeftIndex j) = (-1) ^ ↑j * ν.sign

Sign relation for left insertion: (insertLeftStep ν j).sign * (-1)^(insertLeftIndex ν j) = (-1)^j * ν.sign.

Derived from invCount_insertLeftStep_add via exponent arithmetic: the identity invCount(μ) + j = invCount(ν) + t gives (-1)^(invCount(μ) + j) = (-1)^(invCount(ν) + t), hence sign(μ) * (-1)^j = sign(ν) * (-1)^t, and multiplying both sides by (-1)^(j+t) (using (-1)^(2k) = 1) yields the result.

theorem LeanPool.EilenbergZilber.Shuffle.sign_insertRightStep {p q : ℕ} (ν : Shuffle p q) (k : Fin (q + 2)) : (ν.insertRightStep k).sign * (-1) ^ ↑(ν.insertRightIndex k) = (-1) ^ p * ((-1) ^ ↑k * ν.sign)

Sign relation for right insertion: (insertRightStep ν k).sign * (-1)^(insertRightIndex ν k) = (-1)^p * (-1)^k * ν.sign.

Diagonal cancellation

The LHS terms not in the image of insertLeftStep or insertRightStep are "diagonal" terms: they arise from vertex removals where the steps on either side have different types (one left, one right). These cancel pairwise via a sign-reversing involution that swaps the two steps around the removed vertex.

def LeanPool.EilenbergZilber.Shuffle.isDiagonalVertex {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) : Prop

A (μ, r) pair is a diagonal term if vertex r has one adjacent left step and one adjacent right step (in either order LR or RL). Boundary vertices (r = 0 or r = last) are never diagonal.

Equations

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

@[instance_reducible]

instance LeanPool.EilenbergZilber.Shuffle.decidablePredIsDiagonalVertex {p q : ℕ} (μ : Shuffle p q) : DecidablePred μ.isDiagonalVertex

Equations

• μ.decidablePredIsDiagonalVertex r = id (if h : 0 < ↑r then ⋯.mpr (if h_1 : ↑r < p + q then ⋯.mpr inferInstance else ⋯.mpr inferInstance) else ⋯.mpr inferInstance)

Insertion–diagonal interface

The insertion maps produce exactly the non-diagonal terms of the boundary sum. Each insertion lands in the non-diagonal set, together they cover it, and their images are disjoint.

theorem LeanPool.EilenbergZilber.Shuffle.insertLeftStep_not_diagonal {p q : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) : ¬(ν.insertLeftStep j).isDiagonalVertex (Fin.cast ⋯ (ν.insertLeftIndex j))

Left insertion always produces a non-diagonal vertex: the two steps adjacent to the inserted vertex are both left steps (LL pattern).

theorem LeanPool.EilenbergZilber.Shuffle.insertRightStep_not_diagonal {p q : ℕ} (ν : Shuffle (p + 1) q) (k : Fin (q + 2)) : ¬(ν.insertRightStep k).isDiagonalVertex (Fin.cast ⋯ (ν.insertRightIndex k))

Right insertion always produces a non-diagonal vertex: the two steps adjacent to the inserted vertex are both right steps (RR pattern).

def LeanPool.EilenbergZilber.Shuffle.isLeftVertex {p q : ℕ} (μ : Shuffle p q) (r : Fin (p + q + 1)) : Prop

A vertex r is a "left vertex" if the adjacent steps are both left steps (or it is a boundary vertex adjacent to a left step).

Equations

• μ.isLeftVertex r = ((∀ (k : Fin (p + q)), k.succ = r → μ.isLeftStep k) ∧ ∀ (k : Fin (p + q)), k.castSucc = r → μ.isLeftStep k)

def LeanPool.EilenbergZilber.Shuffle.isRightVertex {p q : ℕ} (μ : Shuffle p q) (r : Fin (p + q + 1)) : Prop

A vertex r is a "right vertex" if the adjacent steps are both right steps.

Equations

• μ.isRightVertex r = ((∀ (k : Fin (p + q)), k.succ = r → ¬μ.isLeftStep k) ∧ ∀ (k : Fin (p + q)), k.castSucc = r → ¬μ.isLeftStep k)

def LeanPool.EilenbergZilber.Shuffle.finRemove {n : ℕ} (p i : Fin (n + 2)) : Fin (n + 1)

Inverse of Fin.succAbove p: maps i to j such that p.succAbove j = i, assuming i ≠ p.

Equations

• LeanPool.EilenbergZilber.Shuffle.finRemove p i = if h : i < p then ⟨↑i, ⋯⟩ else ⟨↑i - 1, ⋯⟩

def LeanPool.EilenbergZilber.Shuffle.removeLeftFun {p q : ℕ} (μ : Shuffle (p + 1) q) (r : Fin (p + q + 2)) : Index (p + q) → Index p × Index q

Removing a left step at r (assuming isLeftVertex μ r).

Equations

• μ.removeLeftFun r k = (LeanPool.EilenbergZilber.Shuffle.finRemove (↑μ (Fin.cast ⋯ r)).1 (↑μ ((Fin.cast ⋯ r).succAbove (Fin.cast ⋯ k))).1, (↑μ ((Fin.cast ⋯ r).succAbove (Fin.cast ⋯ k))).2)

def LeanPool.EilenbergZilber.Shuffle.removeRightFun {p q : ℕ} (μ : Shuffle p (q + 1)) (r : Fin (p + q + 2)) : Index (p + q) → Index p × Index q

Removing a right step at r (assuming isRightVertex μ r).

Equations

• μ.removeRightFun r k = ((↑μ ((Fin.cast ⋯ r).succAbove (Fin.cast ⋯ k))).1, LeanPool.EilenbergZilber.Shuffle.finRemove (↑μ (Fin.cast ⋯ r)).2 (↑μ ((Fin.cast ⋯ r).succAbove (Fin.cast ⋯ k))).2)

theorem LeanPool.EilenbergZilber.Shuffle.succAbove_finRemove {n : ℕ} (p i : Fin (n + 2)) (h : i ≠ p) : p.succAbove (finRemove p i) = i

theorem LeanPool.EilenbergZilber.Shuffle.finRemove_strictMono_on {n : ℕ} (p : Fin (n + 2)) : StrictMonoOn (finRemove p) {i : Fin (n + 2) | i ≠ p}

theorem LeanPool.EilenbergZilber.Shuffle.ne_fst_of_isLeftVertex {p q : ℕ} {μ : Shuffle (p + 1) q} {r : Index (p + 1 + q)} (h : μ.isLeftVertex r) (k : Index (p + 1 + q)) (hkr : k ≠ r) : (↑μ k).1 ≠ (↑μ r).1

theorem LeanPool.EilenbergZilber.Shuffle.ne_snd_of_isRightVertex {p q : ℕ} {μ : Shuffle p (q + 1)} {r : Index (p + (q + 1))} (h : μ.isRightVertex r) (k : Index (p + (q + 1))) (hkr : k ≠ r) : (↑μ k).2 ≠ (↑μ r).2

theorem LeanPool.EilenbergZilber.Shuffle.removeLeft_is_shuffle {p q : ℕ} {μ : Shuffle (p + 1) q} {r : Fin (p + q + 2)} (h : μ.isLeftVertex (Fin.cast ⋯ r)) : StrictMono (μ.removeLeftFun r)

theorem LeanPool.EilenbergZilber.Shuffle.removeRight_is_shuffle {p q : ℕ} {μ : Shuffle p (q + 1)} {r : Fin (p + q + 2)} (h : μ.isRightVertex (Fin.cast ⋯ r)) : StrictMono (μ.removeRightFun r)

def LeanPool.EilenbergZilber.Shuffle.removeLeft {p q : ℕ} (μ : Shuffle (p + 1) q) (r : Fin (p + q + 2)) (h : μ.isLeftVertex (Fin.cast ⋯ r)) : Shuffle p q

The shuffle obtained by removing a left step.

Equations

• μ.removeLeft r h = ⟨{ toFun := μ.removeLeftFun r, monotone' := ⋯ }, ⋯⟩

def LeanPool.EilenbergZilber.Shuffle.removeRight {p q : ℕ} (μ : Shuffle p (q + 1)) (r : Fin (p + q + 2)) (h : μ.isRightVertex (Fin.cast ⋯ r)) : Shuffle p q

The shuffle obtained by removing a right step.

Equations

• μ.removeRight r h = ⟨{ toFun := μ.removeRightFun r, monotone' := ⋯ }, ⋯⟩

theorem LeanPool.EilenbergZilber.Shuffle.finRemove_val_lt_iff {n : ℕ} {p i : Fin (n + 2)} (h : i ≠ p) : ↑(finRemove p i) < ↑p ↔ i < p

theorem LeanPool.EilenbergZilber.Shuffle.insertIndex_removeLeft {p q : ℕ} {μ : Shuffle (p + 1) q} {r : Fin (p + q + 2)} (h : μ.isLeftVertex (Fin.cast ⋯ r)) : (μ.removeLeft r h).insertLeftIndex (↑μ (Fin.cast ⋯ r)).1 = Fin.cast ⋯ r

theorem LeanPool.EilenbergZilber.Shuffle.insertLeft_removeLeft {p q : ℕ} {μ : Shuffle (p + 1) q} {r : Fin (p + q + 2)} (h : μ.isLeftVertex (Fin.cast ⋯ r)) : (μ.removeLeft r h).insertLeftStep (↑μ (Fin.cast ⋯ r)).1 = μ

theorem LeanPool.EilenbergZilber.Shuffle.insertIndex_removeRight {p q : ℕ} {μ : Shuffle p (q + 1)} {r : Fin (p + q + 2)} (h : μ.isRightVertex (Fin.cast ⋯ r)) : (μ.removeRight r h).insertRightIndex (↑μ (Fin.cast ⋯ r)).2 = Fin.cast ⋯ r

theorem LeanPool.EilenbergZilber.Shuffle.isRightVertex_swap {p q : ℕ} {μ : Shuffle p q} {r : Fin (p + q + 1)} : μ.isRightVertex r ↔ μ.swap.isLeftVertex (Fin.cast ⋯ r)

theorem LeanPool.EilenbergZilber.Shuffle.removeRight_eq_swap_removeLeft {p q : ℕ} (μ : Shuffle p (q + 1)) (r : Fin (p + q + 2)) (h : μ.isRightVertex (Fin.cast ⋯ r)) : μ.removeRight r h = (μ.swap.removeLeft (Fin.cast ⋯ r) ⋯).swap

theorem LeanPool.EilenbergZilber.Shuffle.not_diagonal_iff_left_or_right {p q : ℕ} {μ : Shuffle (p + 1) (q + 1)} {r : Fin (p + q + 3)} : ¬μ.isDiagonalVertex (Fin.cast ⋯ r) ↔ μ.isLeftVertex (Fin.cast ⋯ r) ∨ μ.isRightVertex (Fin.cast ⋯ r)

theorem LeanPool.EilenbergZilber.Shuffle.nondiag_mem_insertLeft_or_insertRight {p q : ℕ} (μ : Shuffle (p + 1) (q + 1)) (r : Index (p + 1 + (q + 1))) (hr : ¬μ.isDiagonalVertex r) : (∃ (j : Fin (p + 2)) (ν : Shuffle p (q + 1)), μ = ν.insertLeftStep j ∧ ↑(ν.insertLeftIndex j) = ↑r) ∨ ∃ (k : Fin (q + 2)) (ν : Shuffle (p + 1) q), μ = ν.insertRightStep k ∧ ↑(ν.insertRightIndex k) = ↑r

theorem LeanPool.EilenbergZilber.Shuffle.insertLeftStep_isLeftType {p q : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) : (ν.insertLeftStep j).isLeftStep ⟨min (↑(ν.insertLeftIndex j)) (p + 1 + q - 1), ⋯⟩

Left insertion produces a left-type vertex: the step at (or just before) the inserted vertex is a left step. Here isLeftType checks isLeftStep at index min r.val ((p+1)+(q)-1).

theorem LeanPool.EilenbergZilber.Shuffle.insertRightStep_not_isLeftType {p q : ℕ} (ν : Shuffle p q) (k : Fin (q + 2)) : ¬(ν.insertRightStep k).isLeftStep ⟨min (↑(ν.insertRightIndex k)) (p + (q + 1) - 1), ⋯⟩

Right insertion produces a non-left-type vertex: the step at (or just before) the inserted vertex is a right step, not a left step.

theorem LeanPool.EilenbergZilber.Shuffle.isDiagonalVertex_bounds {p q : ℕ} {μ : Shuffle p q} {r : Index (p + q)} (hr : μ.isDiagonalVertex r) : 0 < ↑r ∧ ↑r < p + q

Extract the two facts from isDiagonalVertex: 0 < r and r < (p+1)+(q+1).

theorem LeanPool.EilenbergZilber.Shuffle.diagonal_left_fst_pos {p q : ℕ} {μ : Shuffle p q} {r : Index (p + q)} (hr : μ.isDiagonalVertex r) (hL : μ.isLeftStep ⟨↑r - 1, ⋯⟩) : 0 < ↑(↑μ r).1

At a diagonal vertex with a left step at r-1, the shuffle step from r-1 to r increments fst, giving μ(r).1 ≥ 1.

theorem LeanPool.EilenbergZilber.Shuffle.diagonal_right_snd_pos {p q : ℕ} {μ : Shuffle p q} {r : Index (p + q)} (hr : μ.isDiagonalVertex r) (hR : ¬μ.isLeftStep ⟨↑r - 1, ⋯⟩) : 0 < ↑(↑μ r).2

At a diagonal vertex with a right step at r-1, the shuffle step from r-1 to r increments snd, giving μ(r).2 ≥ 1.

def LeanPool.EilenbergZilber.Shuffle.swapDiagonalStepsFun {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : Index (p + q) → Index p × Index q

The underlying function for swapDiagonalSteps: agrees with μ everywhere except at vertex r, where the step type is swapped.

• LR diagonal (left then right): μ(r) becomes (μ(r).1 - 1, μ(r).2 + 1)
• RL diagonal (right then left): μ(r) becomes (μ(r).1 + 1, μ(r).2 - 1)

Equations

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

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalStepsFun_monotone {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : Monotone (μ.swapDiagonalStepsFun r hr)

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalStepsFun_injective {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : Function.Injective (μ.swapDiagonalStepsFun r hr)

swapDiagonalStepsFun is injective. Follows from monotonicity + coordinate-sum preservation (same argument as for insertLeftStep).

def LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : Shuffle p q

The sign-reversing involution on diagonal terms. Given a (p+1, q+1)-shuffle μ and a diagonal vertex r, swap the steps adjacent to r (replacing an LR corner with RL or vice versa). This produces a new shuffle μ' such that:

• μ' ∘ δ_r = μ ∘ δ_r (same underlying map after vertex removal)
• μ'.sign = -μ.sign (opposite sign, from the inversion count change)

Equations

• μ.swapDiagonalSteps r hr = ⟨{ toFun := μ.swapDiagonalStepsFun r hr, monotone' := ⋯ }, ⋯⟩

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_apply_ne {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) (i : Index (p + q)) (hi : i ≠ r) : ↑(μ.swapDiagonalSteps r hr) i = ↑μ i

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_apply_r_of_left {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) (hL : μ.isLeftStep ⟨↑r - 1, ⋯⟩) : ↑(μ.swapDiagonalSteps r hr) r = (⟨↑(↑μ r).1 - 1, ⋯⟩, ⟨↑(↑μ r).2 + 1, ⋯⟩)

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_apply_r_of_right {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) (hR : ¬μ.isLeftStep ⟨↑r - 1, ⋯⟩) : ↑(μ.swapDiagonalSteps r hr) r = (⟨↑(↑μ r).1 + 1, ⋯⟩, ⟨↑(↑μ r).2 - 1, ⋯⟩)

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_flip_prev {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : (μ.swapDiagonalSteps r hr).isLeftStep ⟨↑r - 1, ⋯⟩ ↔ ¬μ.isLeftStep ⟨↑r - 1, ⋯⟩

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_flip_curr {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : (μ.swapDiagonalSteps r hr).isLeftStep ⟨↑r, ⋯⟩ ↔ ¬μ.isLeftStep ⟨↑r, ⋯⟩

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_vertex {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : (μ.swapDiagonalSteps r hr).isDiagonalVertex r

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_apply_ne_r {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) (i : Index (p + q)) (h : i ≠ r) : ↑(μ.swapDiagonalSteps r hr) i = ↑μ i

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_val_r {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) (rm1 : Fin (p + q)) (h_rm1 : ↑rm1 = ↑r - 1) : ↑(μ.swapDiagonalSteps r hr) r = if h : μ.isLeftStep rm1 then (⟨↑(↑μ r).1 - 1, ⋯⟩, ⟨↑(↑μ r).2 + 1, ⋯⟩) else (⟨↑(↑μ r).1 + 1, ⋯⟩, ⟨↑(↑μ r).2 - 1, ⋯⟩)

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_isLeftStep_toggle {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : have rm1 := ⟨↑r - 1, ⋯⟩; (μ.swapDiagonalSteps r hr).isLeftStep rm1 ↔ ¬μ.isLeftStep rm1

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_involutive {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : (μ.swapDiagonalSteps r hr).swapDiagonalSteps r ⋯ = μ

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_neg_sign {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : (μ.swapDiagonalSteps r hr).sign = -μ.sign

The swap negates the signed coefficient.

Derives from swapDiagonalSteps_invCount_sum_odd: since the invCount sum is odd, (-1)^invCount' * (-1)^invCount = -1, and multiplying both sides by (-1)^invCount (which squares to 1) gives (-1)^invCount' = -(-1)^invCount.

theorem LeanPool.EilenbergZilber.Shuffle.swapDiagonalSteps_ne {p q : ℕ} (μ : Shuffle p q) (r : Index (p + q)) (hr : μ.isDiagonalVertex r) : μ.swapDiagonalSteps r hr ≠ μ

The swap involution is never the identity: swapping two steps of different type always produces a distinct shuffle.

@[instance_reducible]

instance LeanPool.EilenbergZilber.uniqueShuffleNZero {n : ℕ} : Unique (Shuffle n 0)

Equations

• LeanPool.EilenbergZilber.uniqueShuffleNZero = { default := ⟨{ toFun := fun (i : LeanPool.EilenbergZilber.Index (n + 0)) => (i, 0), monotone' := ⋯ }, ⋯⟩, uniq := ⋯ }

@[instance_reducible]

instance LeanPool.EilenbergZilber.uniqueShuffleZeroN {n : ℕ} : Unique (Shuffle 0 n)

Equations

• LeanPool.EilenbergZilber.uniqueShuffleZeroN = { default := ⟨{ toFun := fun (i : LeanPool.EilenbergZilber.Index (0 + n)) => (0, Fin.cast ⋯ i), monotone' := ⋯ }, ⋯⟩, uniq := ⋯ }

theorem LeanPool.EilenbergZilber.Shuffle.sign_default_zero_right {n : ℕ} : default.sign = 1

The unique (n,0)-shuffle has sign 1.

theorem LeanPool.EilenbergZilber.Shuffle.sign_default_zero_left {n : ℕ} : default.sign = 1

The unique (0,n)-shuffle has sign 1.