From 8e90361d2dd9e7e82bbdf867414862ebc144018d Mon Sep 17 00:00:00 2001 From: Codex Date: Sat, 25 Jul 2026 21:56:55 +0000 Subject: [PATCH 1/7] start independent M N Jacobi-Trudi API --- .../SymmetricFunctions/JacobiTrudiMN.lean | 201 ++++++++++++++++++ 1 file changed, 201 insertions(+) create mode 100644 AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean diff --git a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean new file mode 100644 index 000000000..7da640a79 --- /dev/null +++ b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean @@ -0,0 +1,201 @@ +/- +Copyright (c) Meta Platforms, Inc. and affiliates. +All rights reserved. +-/ +import AlgebraicCombinatorics.SymmetricFunctions.PieriJacobiTrudi + +/-! +# Jacobi--Trudi with independent row and alphabet sizes + +The original API in `PieriJacobiTrudi` uses one natural number both for the number +of rows of a skew partition and for the tableau alphabet. This file starts the +compatibility-preserving generalization in which: + +* `M` indexes rows and the Jacobi--Trudi matrix; +* `N` indexes tableau entries and polynomial variables. + +The old definitions remain unchanged. The `M = N` equivalences below make the +new API interoperable with them. +-/ + +open Finset BigOperators Matrix MvPolynomial + +namespace SymmetricFunctions + +variable {M N : ℕ} {R : Type*} [CommRing R] + +/-- A semistandard tableau of an `M`-row skew shape with entries in `Fin N`. -/ +structure SkewSSYTMN (N : ℕ) (s : SkewPartition M) where + /-- The entries in each row, indexed by their offset from the inner shape. -/ + entries : + (i : Fin M) → Fin (s.outer.parts i - s.inner.parts i) → Fin N + /-- Entries weakly increase along rows. -/ + rowWeak : + ∀ i : Fin M, ∀ j k : Fin (s.outer.parts i - s.inner.parts i), + j ≤ k → entries i j ≤ entries i k + /-- Entries strictly increase down adjacent rows whenever both cells exist. -/ + colStrict : + ∀ i : Fin M, ∀ hi : i.val + 1 < M, + ∀ k : Fin (s.outer.parts i - s.inner.parts i), + ∀ _hcol : + s.inner.parts i + k.val + 1 > s.inner.parts ⟨i.val + 1, hi⟩ ∧ + s.inner.parts i + k.val + 1 ≤ s.outer.parts ⟨i.val + 1, hi⟩, + let k' := s.inner.parts i + k.val - s.inner.parts ⟨i.val + 1, hi⟩ + ∀ hk' : + k' < + s.outer.parts ⟨i.val + 1, hi⟩ - + s.inner.parts ⟨i.val + 1, hi⟩, + entries i k < entries ⟨i.val + 1, hi⟩ ⟨k', hk'⟩ + +namespace SkewSSYTMN + +/-- Two generalized skew tableaux are equal when their entries are equal. -/ +@[ext] +theorem ext {s : SkewPartition M} {T U : SkewSSYTMN N s} + (h : T.entries = U.entries) : T = U := by + cases T + cases U + simp only at h + subst h + rfl + +/-- The monomial obtained by multiplying one variable for every tableau cell. -/ +noncomputable def toMonomial {s : SkewPartition M} (T : SkewSSYTMN N s) : + MvPolynomial (Fin N) R := + ∏ i : Fin M, ∏ k : Fin (s.outer.parts i - s.inner.parts i), + X (T.entries i k) + +end SkewSSYTMN + +/-- An unrestricted filling of an `M`-row skew shape by letters in `Fin N`. -/ +abbrev SkewFillingMN (N : ℕ) (s : SkewPartition M) := + (i : Fin M) → Fin (s.outer.parts i - s.inner.parts i) → Fin N + +instance skewFillingMN_fintype (N : ℕ) (s : SkewPartition M) : + Fintype (SkewFillingMN N s) := + inferInstance + +/-- Row semistandardness for a generalized skew filling. -/ +def isRowWeakMN (s : SkewPartition M) (f : SkewFillingMN N s) : Prop := + ∀ i : Fin M, ∀ j k : Fin (s.outer.parts i - s.inner.parts i), + j ≤ k → f i j ≤ f i k + +/-- Adjacent-row column strictness for a generalized skew filling. -/ +def isColStrictMN (s : SkewPartition M) (f : SkewFillingMN N s) : Prop := + ∀ i : Fin M, ∀ hi : i.val + 1 < M, + ∀ k : Fin (s.outer.parts i - s.inner.parts i), + ∀ _hcol : + s.inner.parts i + k.val + 1 > s.inner.parts ⟨i.val + 1, hi⟩ ∧ + s.inner.parts i + k.val + 1 ≤ s.outer.parts ⟨i.val + 1, hi⟩, + let k' := s.inner.parts i + k.val - s.inner.parts ⟨i.val + 1, hi⟩ + ∀ hk' : + k' < + s.outer.parts ⟨i.val + 1, hi⟩ - + s.inner.parts ⟨i.val + 1, hi⟩, + f i k < f ⟨i.val + 1, hi⟩ ⟨k', hk'⟩ + +/-- Semistandardness for a generalized skew filling. -/ +def isSSYTFillingMN (s : SkewPartition M) (f : SkewFillingMN N s) : Prop := + isRowWeakMN s f ∧ isColStrictMN s f + +instance isRowWeakMN_decidable (s : SkewPartition M) (f : SkewFillingMN N s) : + Decidable (isRowWeakMN s f) := + Fintype.decidableForallFintype + +instance isColStrictMN_decidable (s : SkewPartition M) (f : SkewFillingMN N s) : + Decidable (isColStrictMN s f) := + Fintype.decidableForallFintype + +instance isSSYTFillingMN_decidable (s : SkewPartition M) (f : SkewFillingMN N s) : + Decidable (isSSYTFillingMN s f) := + instDecidableAnd + +/-- Turn a semistandard filling into a bundled generalized tableau. -/ +def fillingToSkewSSYTMN {s : SkewPartition M} (f : SkewFillingMN N s) + (hf : isSSYTFillingMN s f) : SkewSSYTMN N s where + entries := f + rowWeak := hf.1 + colStrict := hf.2 + +/-- The finite collection of all generalized skew tableaux of a fixed shape. -/ +noncomputable def skewSSYTMNFinset (N : ℕ) (s : SkewPartition M) : + Finset (SkewSSYTMN N s) := + (Finset.univ.filter (isSSYTFillingMN s)).attach.map + ⟨fun f => fillingToSkewSSYTMN f.1 (Finset.mem_filter.mp f.2).2, + fun f g h => by + apply Subtype.ext + apply _root_.funext + intro i + apply _root_.funext + intro k + exact congrFun (congrFun (congrArg SkewSSYTMN.entries h) i) k⟩ + +/-- Every generalized skew tableau occurs in `skewSSYTMNFinset`. -/ +theorem skewSSYTMNFinset_mem (s : SkewPartition M) (T : SkewSSYTMN N s) : + T ∈ skewSSYTMNFinset N s := by + simp only [skewSSYTMNFinset, Finset.mem_map, Finset.mem_attach, true_and, + Subtype.exists] + refine ⟨T.entries, ?_, ?_⟩ + · simp only [Finset.mem_filter, Finset.mem_univ, true_and] + exact ⟨T.rowWeak, T.colStrict⟩ + · cases T + rfl + +/-- The skew Schur polynomial of an `M`-row shape in `N` variables. -/ +noncomputable def skewSchurMN (N : ℕ) (s : SkewPartition M) : + MvPolynomial (Fin N) R := + ∑ T ∈ skewSSYTMNFinset N s, T.toMonomial + +/-- Complete homogeneous functions with the negative-index convention. -/ +noncomputable def jacobiTrudiMatrixHMN (N : ℕ) (lam mu : Fin M → ℕ) : + Matrix (Fin M) (Fin M) (MvPolynomial (Fin N) R) := + fun i j => hsymmExt (N := N) (R := R) + ((lam i : ℤ) - (mu j : ℤ) - (i.val : ℤ) + (j.val : ℤ)) + +/-- At equal row and alphabet sizes, a generalized tableau is the original tableau. -/ +def skewSSYTMNSelfEquiv (s : SkewPartition N) : SkewSSYTMN N s ≃ SkewSSYT s where + toFun T := + { entries := T.entries + rowWeak := T.rowWeak + colStrict := T.colStrict } + invFun T := + { entries := T.entries + rowWeak := T.rowWeak + colStrict := T.colStrict } + left_inv T := by cases T; rfl + right_inv T := by cases T; rfl + +@[simp] +theorem skewSSYTMNSelfEquiv_entries (s : SkewPartition N) (T : SkewSSYTMN N s) : + (skewSSYTMNSelfEquiv s T).entries = T.entries := + rfl + +@[simp] +theorem skewSSYTMNSelfEquiv_toMonomial (s : SkewPartition N) (T : SkewSSYTMN N s) : + SkewSSYT.toMonomial (R := R) (skewSSYTMNSelfEquiv s T) = + T.toMonomial := + rfl + +/-- The generalized skew Schur polynomial recovers the original API when `M = N`. -/ +@[simp] +theorem skewSchurMN_self (s : SkewPartition N) : + skewSchurMN (R := R) N s = skewSchur (R := R) s := by + unfold skewSchurMN skewSchur + apply Finset.sum_bij (fun T _ => skewSSYTMNSelfEquiv s T) + · intro T _ + exact skewSSYTFinset_mem s (skewSSYTMNSelfEquiv s T) + · intro T₁ _ T₂ _ h + exact (skewSSYTMNSelfEquiv s).injective h + · intro T hT + refine ⟨(skewSSYTMNSelfEquiv s).symm T, + skewSSYTMNFinset_mem s ((skewSSYTMNSelfEquiv s).symm T), ?_⟩ + exact (skewSSYTMNSelfEquiv s).apply_symm_apply T + · intro T _ + exact (skewSSYTMNSelfEquiv_toMonomial (R := R) s T).symm + +@[simp] +theorem jacobiTrudiMatrixHMN_self (lam mu : Fin N → ℕ) : + jacobiTrudiMatrixHMN (R := R) N lam mu = jacobiTrudiMatrixH (R := R) lam mu := + rfl + +end SymmetricFunctions From 7030a2032d2f3db05044202135282bf960bd74d1 Mon Sep 17 00:00:00 2001 From: Codex Date: Sat, 25 Jul 2026 22:39:58 +0000 Subject: [PATCH 2/7] generalize Jacobi-Trudi path tableau bijection --- .../SymmetricFunctions/JacobiTrudiMN.lean | 356 ++++++++++++++++++ 1 file changed, 356 insertions(+) diff --git a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean index 7da640a79..dd2a29a51 100644 --- a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean +++ b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean @@ -141,6 +141,86 @@ theorem skewSSYTMNFinset_mem (s : SkewPartition M) (T : SkewSSYTMN N s) : · cases T rfl +/-- Adjacent column strictness implies column strictness between arbitrary rows. -/ +theorem SkewSSYTMN.colStrict_nonadjacent {s : SkewPartition M} + (T : SkewSSYTMN N s) (i j : Fin M) (hij : i < j) + (k : Fin (s.outer.parts i - s.inner.parts i)) + (k' : Fin (s.outer.parts j - s.inner.parts j)) + (hcol_eq : s.inner.parts i + k.val = s.inner.parts j + k'.val) : + T.entries i k < T.entries j k' := by + obtain ⟨d, hd_eq⟩ : ∃ d, j.val - i.val = d + 1 := + ⟨j.val - i.val - 1, by omega⟩ + induction d using Nat.strong_induction_on generalizing i j k k' with + | _ d ih => + by_cases hd : d = 0 + · have hj_eq : j.val = i.val + 1 := by omega + have hi_lt : i.val + 1 < M := by omega + have hj_fin : j = ⟨i.val + 1, hi_lt⟩ := by + apply Fin.ext + exact hj_eq + subst hj_fin + have hcol : + s.inner.parts i + k.val + 1 > + s.inner.parts ⟨i.val + 1, hi_lt⟩ ∧ + s.inner.parts i + k.val + 1 ≤ + s.outer.parts ⟨i.val + 1, hi_lt⟩ := by + constructor <;> omega + let k''_val := + s.inner.parts i + k.val - s.inner.parts ⟨i.val + 1, hi_lt⟩ + have hk''_eq : k''_val = k'.val := by omega + have hk''_lt : + k''_val < + s.outer.parts ⟨i.val + 1, hi_lt⟩ - + s.inner.parts ⟨i.val + 1, hi_lt⟩ := by + rw [hk''_eq] + exact k'.isLt + have hres := T.colStrict i hi_lt k hcol hk''_lt + convert hres using 2 + apply Fin.ext + exact hk''_eq.symm + · have hj_gt : j.val > i.val + 1 := by omega + let j' : Fin M := ⟨j.val - 1, by omega⟩ + have hij' : i < j' := by simp only [j', Fin.lt_def]; omega + have hj'j : j' < j := by simp only [j', Fin.lt_def]; omega + let k''_val := s.inner.parts i + k.val - s.inner.parts j' + have hk''_lt : + k''_val < s.outer.parts j' - s.inner.parts j' := by + simp only [k''_val] + have hinner : s.inner.parts j' ≤ s.inner.parts i := + s.inner.weaklyDecreasing i j' (le_of_lt hij') + have houter : s.outer.parts j ≤ s.outer.parts j' := + s.outer.weaklyDecreasing j' j (le_of_lt hj'j) + omega + let k'' : Fin (s.outer.parts j' - s.inner.parts j') := + ⟨k''_val, hk''_lt⟩ + have hcol_eq' : + s.inner.parts i + k.val = s.inner.parts j' + k''.val := by + simp only [k'', k''_val] + have hinner : s.inner.parts j' ≤ s.inner.parts i := + s.inner.weaklyDecreasing i j' (le_of_lt hij') + omega + have hdiff' : j'.val - i.val - 1 < d := by + simp only [j'] + omega + have hdiff'_eq : j'.val - i.val = (j'.val - i.val - 1) + 1 := by + omega + have h₁ : T.entries i k < T.entries j' k'' := + ih (j'.val - i.val - 1) hdiff' i j' hij' k k'' hcol_eq' + hdiff'_eq + have hcol_eq'' : + s.inner.parts j' + k''.val = s.inner.parts j + k'.val := by + rw [← hcol_eq', hcol_eq] + have hdiff'' : j.val - j'.val - 1 < d := by + simp only [j'] + omega + have hdiff''_eq : j.val - j'.val = (j.val - j'.val - 1) + 1 := by + simp only [j'] + omega + have h₂ : T.entries j' k'' < T.entries j k' := + ih (j.val - j'.val - 1) hdiff'' j' j hj'j k'' k' hcol_eq'' + hdiff''_eq + exact lt_trans h₁ h₂ + /-- The skew Schur polynomial of an `M`-row shape in `N` variables. -/ noncomputable def skewSchurMN (N : ℕ) (s : SkewPartition M) : MvPolynomial (Fin N) R := @@ -152,6 +232,282 @@ noncomputable def jacobiTrudiMatrixHMN (N : ℕ) (lam mu : Fin M → ℕ) : fun i j => hsymmExt (N := N) (R := R) ((lam i : ℤ) - (mu j : ℤ) - (i.val : ℤ) + (j.val : ℤ)) +/-! ## The independent-size path/tableau correspondence -/ + +/-- An `M`-tuple of tableau paths whose east-step heights lie in `Fin N`. -/ +structure NipatMN (N : ℕ) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) where + paths : (i : Fin M) → LatticePath (N := N) + ((mu i : ℤ) - i.val) ((lam i : ℤ) - i.val) + colStrictPaths : + ∀ i j : Fin M, i < j → + ∀ k : ℕ, ∀ hk : k < (paths i).eastStepHeights.length, + ∀ k' : ℕ, ∀ hk' : k' < (paths j).eastStepHeights.length, + mu i + k = mu j + k' → + (paths i).eastStepHeights[k] < (paths j).eastStepHeights[k'] + +namespace NipatMN + +/-- The product of the weights of the component paths. -/ +noncomputable def weight {lam mu : Fin M → ℕ} + {hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i} + {hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i} + {hcontained : ∀ i, mu i ≤ lam i} + (np : NipatMN N lam mu hlam hmu hcontained) : + MvPolynomial (Fin N) R := + ∏ i : Fin M, (np.paths i).weight + +@[ext] +theorem ext {lam mu : Fin M → ℕ} + {hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i} + {hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i} + {hcontained : ∀ i, mu i ≤ lam i} + {p q : NipatMN N lam mu hlam hmu hcontained} + (h : p.paths = q.paths) : p = q := by + cases p + cases q + simp only at h + subst h + rfl + +end NipatMN + +private theorem list_isChain_getElem_le_getElem_of_le_MN + {α : Type*} [Preorder α] {l : List α} (h : l.IsChain (· ≤ ·)) + {i j : ℕ} (hi : i < l.length) (hj : j < l.length) (hij : i ≤ j) : + l[i] ≤ l[j] := by + induction j with + | zero => simp_all + | succ j ih => + by_cases heq : i = j + 1 + · simp [heq] + · by_cases hij' : i ≤ j + · have hj' : j < l.length := by omega + have h₁ := ih hj' hij' + rw [List.isChain_iff_getElem] at h + exact h₁.trans (h j hj) + · omega + +/-- Build one tableau path from the entries in a row. -/ +def mkLatticePathFromEntriesMN (lam mu i : ℕ) + (entries : Fin (lam - mu) → Fin N) + (hrowWeak : + ∀ j k : Fin (lam - mu), j ≤ k → entries j ≤ entries k) : + LatticePath (N := N) ((mu : ℤ) - i) ((lam : ℤ) - i) where + eastStepHeights := List.ofFn entries + weaklyIncreasing := by + rw [List.isChain_iff_pairwise, List.pairwise_ofFn] + intro j k hjk + exact hrowWeak j k (le_of_lt hjk) + length_eq := by simp + +/-- Turn an independent-size path tuple into its skew tableau. -/ +noncomputable def nipatMNToSSYT {lam mu : Fin M → ℕ} + {hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i} + {hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i} + {hcontained : ∀ i, mu i ≤ lam i} + (np : NipatMN N lam mu hlam hmu hcontained) : + SkewSSYTMN N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩ where + entries := fun i k => (np.paths i).eastStepHeights.get ⟨k.val, by + rw [(np.paths i).length_eq] + simp only [sub_sub_sub_cancel_right] + omega⟩ + rowWeak := fun i j k hjk => by + simp only [List.get_eq_getElem] + exact list_isChain_getElem_le_getElem_of_le_MN + (np.paths i).weaklyIncreasing + (by + rw [(np.paths i).length_eq] + simp only [sub_sub_sub_cancel_right] + simpa using j.isLt) + (by + rw [(np.paths i).length_eq] + simp only [sub_sub_sub_cancel_right] + simpa using k.isLt) + hjk + colStrict := fun i hi k hcol hk' => by + simp only [List.get_eq_getElem] + change mu i + k.val + 1 > mu ⟨i.val + 1, hi⟩ ∧ + mu i + k.val + 1 ≤ lam ⟨i.val + 1, hi⟩ at hcol + change mu i + k.val - mu ⟨i.val + 1, hi⟩ < + lam ⟨i.val + 1, hi⟩ - mu ⟨i.val + 1, hi⟩ at hk' + have hij : i < (⟨i.val + 1, hi⟩ : Fin M) := by + simp only [Fin.lt_def] + omega + have hk : + k.val < (np.paths i).eastStepHeights.length := by + have hlen : (np.paths i).eastStepHeights.length = lam i - mu i := by + rw [(np.paths i).length_eq] + simp only [sub_sub_sub_cancel_right] + omega + rw [hlen] + exact k.isLt + have hkNext : + mu i + k.val - mu ⟨i.val + 1, hi⟩ < + (np.paths ⟨i.val + 1, hi⟩).eastStepHeights.length := by + have hlen : + (np.paths ⟨i.val + 1, hi⟩).eastStepHeights.length = + lam ⟨i.val + 1, hi⟩ - mu ⟨i.val + 1, hi⟩ := by + rw [(np.paths ⟨i.val + 1, hi⟩).length_eq] + simp only [sub_sub_sub_cancel_right] + omega + rw [hlen] + exact hk' + exact np.colStrictPaths i ⟨i.val + 1, hi⟩ hij k.val hk + (mu i + k.val - mu ⟨i.val + 1, hi⟩) hkNext (by omega) + +/-- Turn an independent-size skew tableau into its tuple of tableau paths. -/ +noncomputable def ssytToNipatMN {lam mu : Fin M → ℕ} + {hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i} + {hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i} + {hcontained : ∀ i, mu i ≤ lam i} + (T : SkewSSYTMN N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩) : + NipatMN N lam mu hlam hmu hcontained where + paths := fun i => + mkLatticePathFromEntriesMN (lam i) (mu i) i.val (T.entries i) + (T.rowWeak i) + colStrictPaths := fun i j hij k hk k' hk' hcol_eq => by + simp only [mkLatticePathFromEntriesMN, List.getElem_ofFn] + have hk_fin : k < lam i - mu i := by + simpa [mkLatticePathFromEntriesMN] using hk + have hk'_fin : k' < lam j - mu j := by + simpa [mkLatticePathFromEntriesMN] using hk' + exact T.colStrict_nonadjacent i j hij ⟨k, hk_fin⟩ ⟨k', hk'_fin⟩ + hcol_eq + +@[simp] +theorem ssytToNipatMN_nipatMNToSSYT {lam mu : Fin M → ℕ} + {hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i} + {hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i} + {hcontained : ∀ i, mu i ≤ lam i} + (np : NipatMN N lam mu hlam hmu hcontained) : + ssytToNipatMN (nipatMNToSSYT np) = np := by + apply NipatMN.ext + funext i + apply LatticePath.ext + simp only [ssytToNipatMN, nipatMNToSSYT, mkLatticePathFromEntriesMN] + apply List.ext_getElem + · simp only [List.length_ofFn] + rw [(np.paths i).length_eq] + simp only [sub_sub_sub_cancel_right] + omega + · intro k hk₁ hk₂ + simp only [List.getElem_ofFn, List.get_eq_getElem] + +@[simp] +theorem nipatMNToSSYT_ssytToNipatMN {lam mu : Fin M → ℕ} + {hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i} + {hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i} + {hcontained : ∀ i, mu i ≤ lam i} + (T : SkewSSYTMN N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩) : + nipatMNToSSYT (ssytToNipatMN T) = T := by + apply SkewSSYTMN.ext + funext i k + simp only [nipatMNToSSYT, ssytToNipatMN, mkLatticePathFromEntriesMN, + List.get_ofFn] + congr 1 + +/-- The weight-preserving path/tableau equivalence with independent dimensions. -/ +noncomputable def nipatMNSSYTEquiv (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + NipatMN N lam mu hlam hmu hcontained ≃ + SkewSSYTMN N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩ where + toFun := nipatMNToSSYT + invFun := ssytToNipatMN + left_inv := ssytToNipatMN_nipatMNToSSYT + right_inv := nipatMNToSSYT_ssytToNipatMN + +private theorem list_prod_map_X_eq_finset_prod_MN + (l : List (Fin N)) (n : ℕ) (h : l.length = n) : + (l.map (fun j => X (R := R) j)).prod = + ∏ k : Fin n, X (l.get ⟨k.val, by rw [h]; exact k.isLt⟩) := by + subst h + induction l with + | nil => simp + | cons hd tl ih => + simp only [List.map_cons, List.prod_cons, List.length_cons] + rw [Fin.prod_univ_succ] + simp only [Fin.val_zero, Fin.val_succ, List.get_cons_succ, List.get] + rw [mul_comm, ih, mul_comm] + +/-- The path/tableau equivalence preserves monomial weights. -/ +theorem nipatMNToSSYT_weight {lam mu : Fin M → ℕ} + {hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i} + {hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i} + {hcontained : ∀ i, mu i ≤ lam i} + (np : NipatMN N lam mu hlam hmu hcontained) : + np.weight (R := R) = (nipatMNToSSYT np).toMonomial := by + unfold NipatMN.weight SkewSSYTMN.toMonomial + congr 1 + funext i + unfold LatticePath.weight + have hlen : (np.paths i).eastStepHeights.length = lam i - mu i := by + rw [(np.paths i).length_eq] + simp only [sub_sub_sub_cancel_right] + omega + rw [list_prod_map_X_eq_finset_prod_MN _ _ hlen] + congr 1 + +noncomputable instance SkewSSYTMN.fintype (N : ℕ) (s : SkewPartition M) : + Fintype (SkewSSYTMN N s) := by + let S := {f : SkewFillingMN N s // isSSYTFillingMN s f} + let e : S ≃ SkewSSYTMN N s := + { toFun := fun f => fillingToSkewSSYTMN f.1 f.2 + invFun := fun T => ⟨T.entries, T.rowWeak, T.colStrict⟩ + left_inv := fun f => by cases f; rfl + right_inv := fun T => by cases T; rfl } + exact Fintype.ofEquiv S e + +noncomputable instance NipatMN.fintype (N : ℕ) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + Fintype (NipatMN N lam mu hlam hmu hcontained) := + Fintype.ofEquiv _ + (nipatMNSSYTEquiv (N := N) lam mu hlam hmu hcontained).symm + +/-- Summing the independent-size path weights gives the tableau definition of +the skew Schur polynomial. -/ +theorem nipatMNWeightSum_eq_skewSchurMN (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + ∑ np : NipatMN N lam mu hlam hmu hcontained, np.weight (R := R) = + skewSchurMN (R := R) N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩ := by + let e := nipatMNSSYTEquiv (N := N) lam mu hlam hmu hcontained + rw [show (∑ np : NipatMN N lam mu hlam hmu hcontained, + np.weight (R := R)) = + ∑ T : SkewSSYTMN N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩, + T.toMonomial by + calc + _ = ∑ np : NipatMN N lam mu hlam hmu hcontained, + (e np).toMonomial := by + apply Finset.sum_congr rfl + intro np _ + exact nipatMNToSSYT_weight np + _ = _ := Equiv.sum_comp e (fun T => T.toMonomial)] + unfold skewSchurMN + symm + apply Finset.sum_bij (fun T _ => T) + · intro T _ + exact Finset.mem_univ T + · intro T₁ _ T₂ _ h + exact h + · intro T _ + exact ⟨T, skewSSYTMNFinset_mem _ T, rfl⟩ + · intro T _ + rfl + /-- At equal row and alphabet sizes, a generalized tableau is the original tableau. -/ def skewSSYTMNSelfEquiv (s : SkewPartition N) : SkewSSYTMN N s ≃ SkewSSYT s where toFun T := From 202bdebf3122ca95768231473bcc2cf604df5768 Mon Sep 17 00:00:00 2001 From: Codex Date: Sat, 25 Jul 2026 22:42:08 +0000 Subject: [PATCH 3/7] generalize Jacobi-Trudi LGV determinant layer --- .../SymmetricFunctions/JacobiTrudiMN.lean | 89 +++++++++++++++++++ 1 file changed, 89 insertions(+) diff --git a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean index dd2a29a51..e023b57d0 100644 --- a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean +++ b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean @@ -508,6 +508,95 @@ theorem nipatMNWeightSum_eq_skewSchurMN (lam mu : Fin M → ℕ) · intro T _ rfl +/-! ## Independent-size LGV determinant layer -/ + +/-- The `M` source vertices for Jacobi--Trudi. -/ +def jacobiTrudiSourceVertexMN (mu : Fin M → ℕ) : + LGV.kVertex (ℤ × ℤ) M := + fun i => ((mu i : ℤ) - i.val, 1) + +/-- The `M` target vertices, at alphabet height `N`. -/ +def jacobiTrudiTargetVertexMN (N : ℕ) (lam : Fin M → ℕ) : + LGV.kVertex (ℤ × ℤ) M := + fun i => ((lam i : ℤ) - i.val, N) + +theorem jacobiTrudiSourceVertexMN_xDecreasing (mu : Fin M → ℕ) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) : + LGV.xDecreasing (jacobiTrudiSourceVertexMN mu) := by + intro i j hij + simp only [LGV.xCoord, jacobiTrudiSourceVertexMN] + have := hmu i j hij + omega + +theorem jacobiTrudiTargetVertexMN_xDecreasing (N : ℕ) (lam : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) : + LGV.xDecreasing (jacobiTrudiTargetVertexMN N lam) := by + intro i j hij + simp only [LGV.xCoord, jacobiTrudiTargetVertexMN] + have := hlam i j hij + omega + +theorem jacobiTrudiSourceVertexMN_yIncreasing (mu : Fin M → ℕ) : + LGV.yIncreasing (jacobiTrudiSourceVertexMN mu) := by + intro i j _ + simp [LGV.yCoord, jacobiTrudiSourceVertexMN] + +theorem jacobiTrudiTargetVertexMN_yIncreasing (N : ℕ) (lam : Fin M → ℕ) : + LGV.yIncreasing (jacobiTrudiTargetVertexMN N lam) := by + intro i j _ + simp [LGV.yCoord, jacobiTrudiTargetVertexMN] + +/-- The generalized Jacobi--Trudi matrix is the transpose of its LGV path +weight matrix. Positivity of `N` is exactly what the lattice-path encoding, +whose vertical interval is from height `1` to height `N`, requires. -/ +theorem jacobiTrudiMatrixHMN_eq_pathWeightMatrix_transpose + (hN : 0 < N) (lam mu : Fin M → ℕ) : + jacobiTrudiMatrixHMN (R := R) N lam mu = + (LGV.pathWeightMatrix LGV.integerLattice_pathFinite + (jacobiTrudiArcWeight (N := N) (R := R)) + (jacobiTrudiSourceVertexMN mu) + (jacobiTrudiTargetVertexMN N lam))ᵀ := by + apply Matrix.ext + intro i j + simp only [jacobiTrudiMatrixHMN, Matrix.transpose_apply, + LGV.pathWeightMatrix, Matrix.of_apply, jacobiTrudiSourceVertexMN, + jacobiTrudiTargetVertexMN] + rw [lgv_pathWeightSum_eq_hsymmExt _ _ hN] + congr 1 + ring + +/-- Determinant form of `jacobiTrudiMatrixHMN_eq_pathWeightMatrix_transpose`. -/ +theorem det_jacobiTrudiMatrixHMN_eq_det_pathWeightMatrix + (hN : 0 < N) (lam mu : Fin M → ℕ) : + (jacobiTrudiMatrixHMN (R := R) N lam mu).det = + (LGV.pathWeightMatrix LGV.integerLattice_pathFinite + (jacobiTrudiArcWeight (N := N) (R := R)) + (jacobiTrudiSourceVertexMN mu) + (jacobiTrudiTargetVertexMN N lam)).det := by + rw [jacobiTrudiMatrixHMN_eq_pathWeightMatrix_transpose hN, + Matrix.det_transpose] + +/-- LGV expresses the generalized determinant as the sum over +nonintersecting `M`-tuples of paths. -/ +theorem det_jacobiTrudiMatrixHMN_eq_lgvNipatWeightSum + (hN : 0 < N) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) : + (jacobiTrudiMatrixHMN (R := R) N lam mu).det = + LGV.nipatWeightSum LGV.integerLattice_pathFinite + (jacobiTrudiArcWeight (N := N) (R := R)) + (jacobiTrudiSourceVertexMN mu) + (jacobiTrudiTargetVertexMN N lam) (Equiv.refl (Fin M)) := by + rw [det_jacobiTrudiMatrixHMN_eq_det_pathWeightMatrix hN] + exact LGV.lgv_nonpermutable + (jacobiTrudiArcWeight (N := N) (R := R)) + (jacobiTrudiSourceVertexMN mu) + (jacobiTrudiTargetVertexMN N lam) + (jacobiTrudiSourceVertexMN_xDecreasing mu hmu) + (jacobiTrudiSourceVertexMN_yIncreasing mu) + (jacobiTrudiTargetVertexMN_xDecreasing N lam hlam) + (jacobiTrudiTargetVertexMN_yIncreasing N lam) + /-- At equal row and alphabet sizes, a generalized tableau is the original tableau. -/ def skewSSYTMNSelfEquiv (s : SkewPartition N) : SkewSSYTMN N s ≃ SkewSSYT s where toFun T := From 043322001ba635f568e22f7a364ac09deb394f74 Mon Sep 17 00:00:00 2001 From: Codex Date: Sat, 25 Jul 2026 22:43:04 +0000 Subject: [PATCH 4/7] isolate generalized Jacobi-Trudi bridge obligation --- .../SymmetricFunctions/JacobiTrudiMN.lean | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean index e023b57d0..f434394f8 100644 --- a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean +++ b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean @@ -597,6 +597,36 @@ theorem det_jacobiTrudiMatrixHMN_eq_lgvNipatWeightSum (jacobiTrudiTargetVertexMN_xDecreasing N lam hlam) (jacobiTrudiTargetVertexMN_yIncreasing N lam) +/-- The sole remaining geometric bridge needed by the independent-size proof. + +It says that LGV's vertex-disjoint path tuples and the east-step-height tuples +used in the tableau equivalence have the same total weight. Keeping this as an +explicit proposition makes the remaining refactor obligation auditable. -/ +def JacobiTrudiMNBridge (N : ℕ) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : Prop := + LGV.nipatWeightSum LGV.integerLattice_pathFinite + (jacobiTrudiArcWeight (N := N) (R := R)) + (jacobiTrudiSourceVertexMN mu) + (jacobiTrudiTargetVertexMN N lam) (Equiv.refl (Fin M)) = + ∑ np : NipatMN N lam mu hlam hmu hcontained, np.weight (R := R) + +/-- Once the geometric path-representation bridge is supplied, the full +independent-`M`/`N` Jacobi--Trudi identity follows by the two compiled layers. -/ +theorem jacobiTrudi_h_mn_of_bridge + (hN : 0 < N) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) + (hbridge : + JacobiTrudiMNBridge (R := R) N lam mu hlam hmu hcontained) : + skewSchurMN (R := R) N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩ = + (jacobiTrudiMatrixHMN (R := R) N lam mu).det := by + rw [det_jacobiTrudiMatrixHMN_eq_lgvNipatWeightSum hN lam mu hlam hmu, + hbridge, nipatMNWeightSum_eq_skewSchurMN] + /-- At equal row and alphabet sizes, a generalized tableau is the original tableau. -/ def skewSSYTMNSelfEquiv (s : SkewPartition N) : SkewSSYTMN N s ≃ SkewSSYT s where toFun T := @@ -643,4 +673,17 @@ theorem jacobiTrudiMatrixHMN_self (lam mu : Fin N → ℕ) : jacobiTrudiMatrixHMN (R := R) N lam mu = jacobiTrudiMatrixH (R := R) lam mu := rfl +/-- The new statement specializes to the already-proved theorem when the two +dimensions agree. This is also a regression theorem for the compatibility +layer; it does not use `JacobiTrudiMNBridge`. -/ +theorem jacobiTrudi_h_mn_self (lam mu : Fin N → ℕ) + (hlam : ∀ i j : Fin N, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin N, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + skewSchurMN (R := R) N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩ = + (jacobiTrudiMatrixHMN (R := R) N lam mu).det := by + rw [skewSchurMN_self, jacobiTrudiMatrixHMN_self] + exact jacobiTrudi_h (R := R) lam mu hlam hmu hcontained + end SymmetricFunctions From e4eabfb6003152d166401fbce65be31a38f7eefa Mon Sep 17 00:00:00 2001 From: Codex Date: Sat, 25 Jul 2026 23:01:28 +0000 Subject: [PATCH 5/7] generalize LGV geometric bridge to rectangular path tuples --- .../SymmetricFunctions/JacobiTrudiMN.lean | 19 +- .../SymmetricFunctions/PieriJacobiTrudi.lean | 271 ++++++++++++------ 2 files changed, 190 insertions(+), 100 deletions(-) diff --git a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean index f434394f8..111a2e10b 100644 --- a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean +++ b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean @@ -234,19 +234,12 @@ noncomputable def jacobiTrudiMatrixHMN (N : ℕ) (lam mu : Fin M → ℕ) : /-! ## The independent-size path/tableau correspondence -/ -/-- An `M`-tuple of tableau paths whose east-step heights lie in `Fin N`. -/ -structure NipatMN (N : ℕ) (lam mu : Fin M → ℕ) +/-- The rectangular path tuple from the foundational Jacobi--Trudi module. -/ +abbrev NipatMN (N : ℕ) (lam mu : Fin M → ℕ) (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) - (hcontained : ∀ i, mu i ≤ lam i) where - paths : (i : Fin M) → LatticePath (N := N) - ((mu i : ℤ) - i.val) ((lam i : ℤ) - i.val) - colStrictPaths : - ∀ i j : Fin M, i < j → - ∀ k : ℕ, ∀ hk : k < (paths i).eastStepHeights.length, - ∀ k' : ℕ, ∀ hk' : k' < (paths j).eastStepHeights.length, - mu i + k = mu j + k' → - (paths i).eastStepHeights[k] < (paths j).eastStepHeights[k'] + (hcontained : ∀ i, mu i ≤ lam i) := + RectNipat N lam mu hlam hmu hcontained namespace NipatMN @@ -257,7 +250,7 @@ noncomputable def weight {lam mu : Fin M → ℕ} {hcontained : ∀ i, mu i ≤ lam i} (np : NipatMN N lam mu hlam hmu hcontained) : MvPolynomial (Fin N) R := - ∏ i : Fin M, (np.paths i).weight + RectNipat.weight np @[ext] theorem ext {lam mu : Fin M → ℕ} @@ -445,7 +438,7 @@ theorem nipatMNToSSYT_weight {lam mu : Fin M → ℕ} {hcontained : ∀ i, mu i ≤ lam i} (np : NipatMN N lam mu hlam hmu hcontained) : np.weight (R := R) = (nipatMNToSSYT np).toMonomial := by - unfold NipatMN.weight SkewSSYTMN.toMonomial + unfold NipatMN.weight RectNipat.weight SkewSSYTMN.toMonomial congr 1 funext i unfold LatticePath.weight diff --git a/AlgebraicCombinatorics/SymmetricFunctions/PieriJacobiTrudi.lean b/AlgebraicCombinatorics/SymmetricFunctions/PieriJacobiTrudi.lean index 1c12a83f6..70c1d81a7 100644 --- a/AlgebraicCombinatorics/SymmetricFunctions/PieriJacobiTrudi.lean +++ b/AlgebraicCombinatorics/SymmetricFunctions/PieriJacobiTrudi.lean @@ -80,7 +80,7 @@ open Finset BigOperators Matrix MvPolynomial namespace SymmetricFunctions -variable {N : ℕ} {R : Type*} [CommRing R] +variable {M N : ℕ} {R : Type*} [CommRing R] /-! ## N-Partitions @@ -2886,6 +2886,53 @@ structure Nipat (lam mu : Fin N → ℕ) mu i + k = mu j + k' → (paths i).eastStepHeights[k] < (paths j).eastStepHeights[k'] +/-- A rectangular Jacobi--Trudi path tuple: `M` paths whose east-step heights +lie in the alphabet `Fin N`. This separates the determinant size from the +number of variables while retaining the path representation used below. -/ +structure RectNipat (N : ℕ) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) where + paths : (i : Fin M) → LatticePath (N := N) + ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) + colStrictPaths : ∀ i j : Fin M, i < j → + ∀ k : ℕ, ∀ hk : k < (paths i).eastStepHeights.length, + ∀ k' : ℕ, ∀ hk' : k' < (paths j).eastStepHeights.length, + mu i + k = mu j + k' → + (paths i).eastStepHeights[k] < (paths j).eastStepHeights[k'] + +/-- Weight of a rectangular path tuple. -/ +noncomputable def RectNipat.weight {lam mu : Fin M → ℕ} + {hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i} + {hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i} + {hcontained : ∀ i, mu i ≤ lam i} + (np : RectNipat N lam mu hlam hmu hcontained) : + MvPolynomial (Fin N) R := + ∏ i : Fin M, (np.paths i).weight + +/-- Rectangular path tuples are finite because each component path is finite and +the column condition cuts out a subtype of their finite product. -/ +noncomputable instance RectNipat.fintype (N : ℕ) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + Fintype (RectNipat N lam mu hlam hmu hcontained) := by + let Paths := + (i : Fin M) → LatticePath (N := N) + ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) + let Good (paths : Paths) : Prop := + ∀ i j : Fin M, i < j → + ∀ k : ℕ, ∀ hk : k < (paths i).eastStepHeights.length, + ∀ k' : ℕ, ∀ hk' : k' < (paths j).eastStepHeights.length, + mu i + k = mu j + k' → + (paths i).eastStepHeights[k] < (paths j).eastStepHeights[k'] + let e : RectNipat N lam mu hlam hmu hcontained ≃ {p : Paths // Good p} := + { toFun := fun p => ⟨p.paths, p.colStrictPaths⟩ + invFun := fun p => ⟨p.1, p.2⟩ + left_inv := fun p => by cases p; rfl + right_inv := fun p => by cases p; rfl } + exact Fintype.ofEquiv _ e.symm + /-- The weight of a nipat is the product of the weights of its component paths. -/ noncomputable def Nipat.weight {lam mu : Fin N → ℕ} {hlam : ∀ i j : Fin N, i ≤ j → lam j ≤ lam i} @@ -3258,6 +3305,15 @@ def jacobiTrudiSourceVertex (mu : Fin N → ℕ) : LGV.kVertex (ℤ × ℤ) N := def jacobiTrudiTargetVertex (lam : Fin N → ℕ) : LGV.kVertex (ℤ × ℤ) N := fun j => (jacobiTrudiTargetX lam j, N) +/-- Rectangular source tuple: `M` sources, independently of alphabet height `N`. -/ +def jacobiTrudiSourceVertexRect (mu : Fin M → ℕ) : LGV.kVertex (ℤ × ℤ) M := + fun i => ((mu i : ℤ) - (i.val : ℤ), 1) + +/-- Rectangular target tuple: `M` targets at alphabet height `N`. -/ +def jacobiTrudiTargetVertexRect (N : ℕ) (lam : Fin M → ℕ) : + LGV.kVertex (ℤ × ℤ) M := + fun i => ((lam i : ℤ) - (i.val : ℤ), N) + /-- The source vertices have x-coordinates that are weakly decreasing. -/ theorem jacobiTrudiSourceVertex_xDecreasing (mu : Fin N → ℕ) (hmu : ∀ i j : Fin N, i ≤ j → mu j ≤ mu i) : @@ -6283,17 +6339,17 @@ private lemma path_above_stays_above (p p' : LGV.SimpleDigraph.Path LGV.integerL /-- Convert an LGV PathTuple to a tuple of LatticePaths. Each path is converted using lgvPathToLatticePath. -/ -private noncomputable def pathTupleToLatticePaths (lam mu : Fin N → ℕ) - (pt : LGV.PathTuple LGV.integerLattice N - (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam)) : - (i : Fin N) → LatticePath (N := N) +private noncomputable def pathTupleToLatticePaths (N : ℕ) (lam mu : Fin M → ℕ) + (pt : LGV.PathTuple LGV.integerLattice M + (jacobiTrudiSourceVertexRect mu) (jacobiTrudiTargetVertexRect N lam)) : + (i : Fin M) → LatticePath (N := N) ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) := fun i => lgvPathToLatticePath ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) (pt.paths i) - (by unfold jacobiTrudiSourceVertex jacobiTrudiSourceX at pt; exact pt.starts i) - (by unfold jacobiTrudiTargetVertex jacobiTrudiTargetX at pt; exact pt.finishes i) + (by unfold jacobiTrudiSourceVertexRect at pt; exact pt.starts i) + (by unfold jacobiTrudiTargetVertexRect at pt; exact pt.finishes i) /-- Key lemma: Non-intersection of LGV paths implies column-strictness of the converted paths. @@ -6314,19 +6370,19 @@ private noncomputable def pathTupleToLatticePaths (lam mu : Fin N → ℕ) - The east-step at column k' in path j (where μⱼ - j + k' = x) has height y - If μᵢ + k = μⱼ + k' (same tableau column), then heights should be strictly ordered - But both have height y, contradiction -/ -private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) - (hlam : ∀ i j : Fin N, i ≤ j → lam j ≤ lam i) - (hmu : ∀ i j : Fin N, i ≤ j → mu j ≤ mu i) +private lemma isNonIntersecting_implies_colStrictPaths (N : ℕ) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) (hcontained : ∀ i, mu i ≤ lam i) - (pt : LGV.PathTuple LGV.integerLattice N - (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam)) + (pt : LGV.PathTuple LGV.integerLattice M + (jacobiTrudiSourceVertexRect mu) (jacobiTrudiTargetVertexRect N lam)) (hni : pt.isNonIntersecting) : - ∀ i j : Fin N, i < j → - ∀ k : ℕ, ∀ hk : k < ((pathTupleToLatticePaths lam mu pt) i).eastStepHeights.length, - ∀ k' : ℕ, ∀ hk' : k' < ((pathTupleToLatticePaths lam mu pt) j).eastStepHeights.length, + ∀ i j : Fin M, i < j → + ∀ k : ℕ, ∀ hk : k < ((pathTupleToLatticePaths N lam mu pt) i).eastStepHeights.length, + ∀ k' : ℕ, ∀ hk' : k' < ((pathTupleToLatticePaths N lam mu pt) j).eastStepHeights.length, mu i + k = mu j + k' → - ((pathTupleToLatticePaths lam mu pt) i).eastStepHeights[k] < - ((pathTupleToLatticePaths lam mu pt) j).eastStepHeights[k'] := by + ((pathTupleToLatticePaths N lam mu pt) i).eastStepHeights[k] < + ((pathTupleToLatticePaths N lam mu pt) j).eastStepHeights[k'] := by -- The proof uses strong induction on j - i. -- For any i < j, we show h_i[k] < h_j[k'] when mu i + k = mu j + k'. -- @@ -6360,7 +6416,7 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) constructor · -- (μ_i - i, 1) is the start of path i have hstart := pt.starts i - unfold jacobiTrudiSourceVertex jacobiTrudiSourceX at hstart + unfold jacobiTrudiSourceVertexRect at hstart rw [← hstart] exact List.head_mem (pt.paths i).nonempty · -- Path j visits (μ_i - i, 1) @@ -6386,8 +6442,8 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) -- Path j's start and end have hstart_j := pt.starts j have hfinish_j := pt.finishes j - unfold jacobiTrudiSourceVertex jacobiTrudiSourceX at hstart_j - unfold jacobiTrudiTargetVertex jacobiTrudiTargetX at hfinish_j + unfold jacobiTrudiSourceVertexRect at hstart_j + unfold jacobiTrudiTargetVertexRect at hfinish_j -- Path j starts at (μ_j - j, 1) which is strictly left of (μ_i - i, 1) have hmu_j_lt : (mu j : ℤ) - (j.val : ℤ) < (mu i : ℤ) - (i.val : ℤ) := by have hmu_ij : mu j ≤ mu i := hmu i j (Fin.le_of_lt hij) @@ -6395,8 +6451,8 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) -- Path j ends at x = λ_j - j. We need this to be ≥ μ_i - i + k. -- From hcol: mu i + k = mu j + k', and k' < lam j - mu j -- So mu i + k < lam j, hence μ_i - i + k < λ_j - j + 1 - have hlen_j : ((pathTupleToLatticePaths lam mu pt) j).eastStepHeights.length = lam j - mu j := by - have h := ((pathTupleToLatticePaths lam mu pt) j).length_eq + have hlen_j : ((pathTupleToLatticePaths N lam mu pt) j).eastStepHeights.length = lam j - mu j := by + have h := ((pathTupleToLatticePaths N lam mu pt) j).length_eq have hcont_j : mu j ≤ lam j := hcontained j simp only [sub_sub_sub_cancel_right] at h omega @@ -6417,8 +6473,8 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) -- path j stays above path i. So at x = μ_i - i + k, y_j > y_i. -- This means h_j[k'].val + 1 > h_i[k].val + 1, so h_j[k'] > h_i[k]. -- But h_not_lt says h_i[k] ≥ h_j[k'], contradiction. - have h_heights : ((pathTupleToLatticePaths lam mu pt) j).eastStepHeights[k'] > - ((pathTupleToLatticePaths lam mu pt) i).eastStepHeights[k] := by + have h_heights : ((pathTupleToLatticePaths N lam mu pt) j).eastStepHeights[k'] > + ((pathTupleToLatticePaths N lam mu pt) i).eastStepHeights[k] := by -- The proof uses path_above_stays_above (the sum-based version) and -- lgvPathEastStepYCoords_at_x to connect eastStepHeights to actual y-coordinates. -- @@ -6439,7 +6495,7 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) let p_j := pt.paths j -- Path i starts at (μ_i - i, 1) have hstart_i := pt.starts i - unfold jacobiTrudiSourceVertex jacobiTrudiSourceX at hstart_i + unfold jacobiTrudiSourceVertexRect at hstart_i -- At x = μ_i - i, path i is at y = 1 (sum = μ_i - i + 1) -- At x = μ_i - i, path j is at y > 1 (since it doesn't visit (μ_i - i, 1)) -- The sum for path j at x = μ_i - i is s_j = μ_i - i + y_j where y_j > 1 @@ -6458,8 +6514,8 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) · exact hmu_j_lt · have h1 : mu i + k < lam j := h_col_bound have h2 : k < lam i - mu i := by - have hlen_i : ((pathTupleToLatticePaths lam mu pt) i).eastStepHeights.length = lam i - mu i := by - have h := ((pathTupleToLatticePaths lam mu pt) i).length_eq + have hlen_i : ((pathTupleToLatticePaths N lam mu pt) i).eastStepHeights.length = lam i - mu i := by + have h := ((pathTupleToLatticePaths N lam mu pt) i).length_eq have hcont_i : mu i ≤ lam i := hcontained i simp only [sub_sub_sub_cancel_right] at h omega @@ -6697,7 +6753,7 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) -- For path i: the k-th east step is at x = start_x + k = μ_i - i + k = x₁ have hk_lt_ycoords_i : k < (lgvPathEastStepYCoords p_i.vertices).length := by have hlen_eq : (lgvPathEastStepYCoords p_i.vertices).length = - ((pathTupleToLatticePaths lam mu pt) i).eastStepHeights.length := by + ((pathTupleToLatticePaths N lam mu pt) i).eastStepHeights.length := by simp only [pathTupleToLatticePaths, lgvPathToLatticePath, p_i] simp only [lgvYCoordsToFinN, List.length_pmap] rw [hlen_eq]; exact hk @@ -6718,7 +6774,7 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) -- So path j's k'-th east step is at x = x₁ - 1, and AFTER the east step, path j is at x₁ have hk'_lt_ycoords_j : k' < (lgvPathEastStepYCoords p_j.vertices).length := by have hlen_eq : (lgvPathEastStepYCoords p_j.vertices).length = - ((pathTupleToLatticePaths lam mu pt) j).eastStepHeights.length := by + ((pathTupleToLatticePaths N lam mu pt) j).eastStepHeights.length := by simp only [pathTupleToLatticePaths, lgvPathToLatticePath, p_j] simp only [lgvYCoordsToFinN, List.length_pmap] rw [hlen_eq]; exact hk' @@ -6815,7 +6871,7 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) -- h_y_comparison : (lgvPathEastStepYCoords p_j.vertices)[k'] > (lgvPathEastStepYCoords p_i.vertices)[k] -- Convert to Fin comparison have hfinish_i := pt.finishes i - unfold jacobiTrudiTargetVertex jacobiTrudiTargetX at hfinish_i + unfold jacobiTrudiTargetVertexRect at hfinish_i have hbnd_i : ∀ y ∈ lgvPathEastStepYCoords p_i.vertices, 1 ≤ y ∧ y ≤ N := by intro y hy have hbnd := lgvPathEastStepYCoords_bounded p_i.vertices p_i.nonempty p_i.arcs_valid y hy @@ -6857,10 +6913,10 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) · -- Inductive case: j > i + 1 -- Use the intermediate row l = i + 1 have h_j_gt : j.val > i.val + 1 := by omega - have hl_lt_N : i.val + 1 < N := by + have hl_lt_N : i.val + 1 < M := by have := j.is_lt omega - let l : Fin N := ⟨i.val + 1, hl_lt_N⟩ + let l : Fin M := ⟨i.val + 1, hl_lt_N⟩ -- k_l = μ_i + k - μ_l is the index for row l at the same tableau column have hmu_l : mu l ≤ mu i := hmu i l (Fin.le_of_lt (by simp only [l, Fin.lt_def]; omega : i < l)) have hlam_l : lam j ≤ lam l := hlam l j (by simp only [l, Fin.le_iff_val_le_val]; omega) @@ -6869,12 +6925,12 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) show mu l + (mu i + k - mu l) = mu i + k omega -- Verify k_l is a valid index - have hk_l_lt : k_l < ((pathTupleToLatticePaths lam mu pt) l).eastStepHeights.length := by + have hk_l_lt : k_l < ((pathTupleToLatticePaths N lam mu pt) l).eastStepHeights.length := by -- k_l = mu i + k - mu l < lam l - mu l -- This follows from mu i + k = mu j + k' < lam j ≤ lam l -- First establish that length = lam l - mu l - have hlen_l : ((pathTupleToLatticePaths lam mu pt) l).eastStepHeights.length = lam l - mu l := by - have h := ((pathTupleToLatticePaths lam mu pt) l).length_eq + have hlen_l : ((pathTupleToLatticePaths N lam mu pt) l).eastStepHeights.length = lam l - mu l := by + have h := ((pathTupleToLatticePaths N lam mu pt) l).length_eq -- h : length = ((lam l : ℤ) - l.val - ((mu l : ℤ) - l.val)).toNat have hcont_l : mu l ≤ lam l := hcontained l simp only [sub_sub_sub_cancel_right] at h @@ -6882,8 +6938,8 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) rw [hlen_l] -- Now goal is k_l < lam l - mu l -- From hk' : k' < length_j = lam j - mu j - have hlen_j : ((pathTupleToLatticePaths lam mu pt) j).eastStepHeights.length = lam j - mu j := by - have h := ((pathTupleToLatticePaths lam mu pt) j).length_eq + have hlen_j : ((pathTupleToLatticePaths N lam mu pt) j).eastStepHeights.length = lam j - mu j := by + have h := ((pathTupleToLatticePaths N lam mu pt) j).length_eq have hcont_j : mu j ≤ lam j := hcontained j simp only [sub_sub_sub_cancel_right] at h omega @@ -6900,8 +6956,8 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) omega have h_d1_pos : 0 < l.val - i.val := by simp [l] have h_d1_eq : l.val - i.val = 0 + 1 := by simp [l] - have h1 : ((pathTupleToLatticePaths lam mu pt) i).eastStepHeights[k] < - ((pathTupleToLatticePaths lam mu pt) l).eastStepHeights[k_l] := by + have h1 : ((pathTupleToLatticePaths N lam mu pt) i).eastStepHeights[k] < + ((pathTupleToLatticePaths N lam mu pt) l).eastStepHeights[k_l] := by have h_d1_lt : 0 < d := by omega exact ih 0 h_d1_lt i l h_i_lt_l k hk k_l hk_l_lt hk_l_eq.symm h_d1_pos h_d1_eq -- Apply IH for (l, j) with d' = j - l - 1 < d @@ -6910,38 +6966,40 @@ private lemma isNonIntersecting_implies_colStrictPaths (lam mu : Fin N → ℕ) have h_d2_eq : j.val - l.val = (d - 1) + 1 := by simp [l]; omega have h_d2_lt : d - 1 < d := Nat.sub_lt (by omega : 0 < d) Nat.one_pos have hcol_l : mu l + k_l = mu j + k' := by rw [hk_l_eq, hcol] - have h2 : ((pathTupleToLatticePaths lam mu pt) l).eastStepHeights[k_l] < - ((pathTupleToLatticePaths lam mu pt) j).eastStepHeights[k'] := by + have h2 : ((pathTupleToLatticePaths N lam mu pt) l).eastStepHeights[k_l] < + ((pathTupleToLatticePaths N lam mu pt) j).eastStepHeights[k'] := by exact ih (d - 1) h_d2_lt l j h_l_lt_j k_l hk_l_lt k' hk' hcol_l h_d2_pos h_d2_eq -- Combine by transitivity exact Fin.lt_trans h1 h2 /-- Convert a non-intersecting PathTuple to a Nipat. -/ -private noncomputable def pathTupleToNipat (lam mu : Fin N → ℕ) - (hlam : ∀ i j : Fin N, i ≤ j → lam j ≤ lam i) - (hmu : ∀ i j : Fin N, i ≤ j → mu j ≤ mu i) +private noncomputable def pathTupleToRectNipat (N : ℕ) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) (hcontained : ∀ i, mu i ≤ lam i) - (pt : LGV.PathTuple LGV.integerLattice N - (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam)) + (pt : LGV.PathTuple LGV.integerLattice M + (jacobiTrudiSourceVertexRect mu) (jacobiTrudiTargetVertexRect N lam)) (hni : pt.isNonIntersecting) : - Nipat lam mu hlam hmu hcontained where - paths := pathTupleToLatticePaths lam mu pt - colStrictPaths := isNonIntersecting_implies_colStrictPaths lam mu hlam hmu hcontained pt hni + RectNipat N lam mu hlam hmu hcontained where + paths := pathTupleToLatticePaths N lam mu pt + colStrictPaths := + isNonIntersecting_implies_colStrictPaths N lam mu hlam hmu hcontained pt hni /-- Weight preservation: The LGV pathTupleWeight equals the Nipat weight under conversion. -/ -private lemma pathTupleToNipat_weight (lam mu : Fin N → ℕ) - (hlam : ∀ i j : Fin N, i ≤ j → lam j ≤ lam i) - (hmu : ∀ i j : Fin N, i ≤ j → mu j ≤ mu i) +private lemma pathTupleToRectNipat_weight (N : ℕ) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) (hcontained : ∀ i, mu i ≤ lam i) - (pt : LGV.PathTuple LGV.integerLattice N - (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam)) + (pt : LGV.PathTuple LGV.integerLattice M + (jacobiTrudiSourceVertexRect mu) (jacobiTrudiTargetVertexRect N lam)) (hni : pt.isNonIntersecting) : LGV.pathTupleWeight (jacobiTrudiArcWeight (N := N) (R := R)) pt.paths = - (pathTupleToNipat lam mu hlam hmu hcontained pt hni).weight (R := R) := by + (pathTupleToRectNipat N lam mu hlam hmu hcontained pt hni).weight (R := R) := by -- The weight of a PathTuple is ∏ᵢ pathWeight(pᵢ) -- The weight of a Nipat is ∏ᵢ (paths i).weight -- By lgvPathToLatticePath_weight_eq, these are equal for each path - unfold LGV.pathTupleWeight Nipat.weight pathTupleToNipat pathTupleToLatticePaths + unfold LGV.pathTupleWeight RectNipat.weight pathTupleToRectNipat + pathTupleToLatticePaths simp only apply Finset.prod_congr rfl intro i _ @@ -6949,8 +7007,8 @@ private lemma pathTupleToNipat_weight (lam mu : Fin N → ℕ) ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) (pt.paths i) - (by unfold jacobiTrudiSourceVertex jacobiTrudiSourceX at pt; exact pt.starts i) - (by unfold jacobiTrudiTargetVertex jacobiTrudiTargetX at pt; exact pt.finishes i) + (by unfold jacobiTrudiSourceVertexRect at pt; exact pt.starts i) + (by unfold jacobiTrudiTargetVertexRect at pt; exact pt.finishes i) /-- The LGV nipat weight sum equals our Nipat weight sum. @@ -6965,14 +7023,16 @@ private lemma pathTupleToNipat_weight (lam mu : Fin N → ℕ) The proof uses `pathTupleToNipat` to convert LGV nipats to our Nipat type, with weight preservation via `pathTupleToNipat_weight`. -/ -theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) - (hlam : ∀ i j : Fin N, i ≤ j → lam j ≤ lam i) - (hmu : ∀ i j : Fin N, i ≤ j → mu j ≤ mu i) +theorem lgv_nipatWeightSum_eq_rectNipatSum (N : ℕ) (lam mu : Fin M → ℕ) + (hheight : M ≠ 0 → 0 < N) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) (hcontained : ∀ i, mu i ≤ lam i) : LGV.nipatWeightSum LGV.integerLattice_pathFinite (jacobiTrudiArcWeight (N := N) (R := R)) - (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam) (Equiv.refl (Fin N)) = - ∑ np : Nipat lam mu hlam hmu hcontained, np.weight (R := R) := by + (jacobiTrudiSourceVertexRect mu) (jacobiTrudiTargetVertexRect N lam) + (Equiv.refl (Fin M)) = + ∑ np : RectNipat N lam mu hlam hmu hcontained, np.weight (R := R) := by -- The proof establishes a weight-preserving bijection between: -- 1. LGV nipats: elements of nipatFinset with isNonIntersecting -- 2. Our Nipat: tuples of LatticePaths with colStrictPaths @@ -6987,7 +7047,7 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) unfold LGV.nipatWeightSum -- Use sum_bij to establish the equality refine Finset.sum_bij - (fun pt hpt => pathTupleToNipat lam mu hlam hmu hcontained pt + (fun pt hpt => pathTupleToRectNipat N lam mu hlam hmu hcontained pt ((LGV.mem_nipatFinset_iff LGV.integerLattice_pathFinite pt).mp hpt)) ?_ ?_ ?_ ?_ -- 1. The function maps into Finset.univ @@ -6998,12 +7058,12 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) -- pathTupleToNipat extracts paths via pathTupleToLatticePaths, which uses lgvPathToLatticePath -- lgvPathToLatticePath extracts east-step heights, which uniquely determine the path -- Therefore, equal Nipats imply equal PathTuples - have hpaths : (pathTupleToNipat lam mu hlam hmu hcontained pt₁ + have hpaths : (pathTupleToRectNipat N lam mu hlam hmu hcontained pt₁ ((LGV.mem_nipatFinset_iff LGV.integerLattice_pathFinite pt₁).mp hpt₁)).paths = - (pathTupleToNipat lam mu hlam hmu hcontained pt₂ + (pathTupleToRectNipat N lam mu hlam hmu hcontained pt₂ ((LGV.mem_nipatFinset_iff LGV.integerLattice_pathFinite pt₂).mp hpt₂)).paths := - congr_arg Nipat.paths heq - simp only [pathTupleToNipat] at hpaths + congr_arg RectNipat.paths heq + simp only [pathTupleToRectNipat] at hpaths -- hpaths : pathTupleToLatticePaths ... pt₁ = pathTupleToLatticePaths ... pt₂ -- Need to show pt₁ = pt₂, i.e., pt₁.paths = pt₂.paths (as functions) ext i @@ -7018,10 +7078,10 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) (pt₁.paths i) (pt₂.paths i) - (by unfold jacobiTrudiSourceVertex jacobiTrudiSourceX at pt₁; exact pt₁.starts i) - (by unfold jacobiTrudiTargetVertex jacobiTrudiTargetX at pt₁; exact pt₁.finishes i) - (by unfold jacobiTrudiSourceVertex jacobiTrudiSourceX at pt₂; exact pt₂.starts i) - (by unfold jacobiTrudiTargetVertex jacobiTrudiTargetX at pt₂; exact pt₂.finishes i) + (by unfold jacobiTrudiSourceVertexRect at pt₁; exact pt₁.starts i) + (by unfold jacobiTrudiTargetVertexRect at pt₁; exact pt₁.finishes i) + (by unfold jacobiTrudiSourceVertexRect at pt₂; exact pt₂.starts i) + (by unfold jacobiTrudiTargetVertexRect at pt₂; exact pt₂.finishes i) hi -- 3. Surjectivity: for every np : Nipat, there exists pt ∈ nipatFinset with pathTupleToNipat pt = np · intro np _ @@ -7029,12 +7089,12 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) -- For each path np.paths i : LatticePath, we build an LGV path using buildVertices. -- -- First, we need N ≥ 1 for the buildVertices lemmas - by_cases hN : N = 0 - · -- If N = 0, there are no Fin N elements - subst hN + by_cases hM : M = 0 + · -- If M = 0, there are no path indices. + subst hM -- Construct the trivial PathTuple (no paths) let pt : LGV.PathTuple LGV.integerLattice 0 - (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam) := + (jacobiTrudiSourceVertexRect mu) (jacobiTrudiTargetVertexRect N lam) := ⟨fun i => Fin.elim0 i, fun i => Fin.elim0 i, fun i => Fin.elim0 i⟩ use pt refine ⟨?_, ?_⟩ @@ -7042,17 +7102,17 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) simp only [LGV.mem_nipatFinset_iff, LGV.PathTuple.isNonIntersecting] exact fun i => Fin.elim0 i · -- pathTupleToNipat pt = np - simp only [pathTupleToNipat] + simp only [pathTupleToRectNipat] cases np with | mk paths colStrict => congr 1 funext i exact Fin.elim0 i · -- N ≥ 1 - have hN_pos : 0 < N := Nat.pos_of_ne_zero hN + have hN_pos : 0 < N := hheight hM have hN_ge : N ≥ 1 := hN_pos -- For each i, construct the LGV path from np.paths i -- Define the path function - let pathFn : (i : Fin N) → LGV.SimpleDigraph.Path LGV.integerLattice := fun i => + let pathFn : (i : Fin M) → LGV.SimpleDigraph.Path LGV.integerLattice := fun i => let lp := np.paths i let a := (mu i : ℤ) - (i.val : ℤ) let c := (lam i : ℤ) - (i.val : ℤ) @@ -7066,16 +7126,16 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) let harcs := buildVertices_arcs_valid a c N lp.eastStepHeights hN_pos lp.length_eq h_ca ⟨vertices, hne, harcs⟩ -- Verify start conditions - have hstarts : ∀ i, (pathFn i).start = jacobiTrudiSourceVertex mu i := fun i => by + have hstarts : ∀ i, (pathFn i).start = jacobiTrudiSourceVertexRect mu i := fun i => by simp only [pathFn, LGV.SimpleDigraph.Path.start] have hne := buildVertices_nonempty ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) N (np.paths i).eastStepHeights have h := buildVertices_head ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) N (np.paths i).eastStepHeights hN_ge - simp only [jacobiTrudiSourceVertex, jacobiTrudiSourceX] + simp only [jacobiTrudiSourceVertexRect] rw [← h] -- Verify finish conditions - have hfinishes : ∀ i, (pathFn i).finish = jacobiTrudiTargetVertex lam i := fun i => by + have hfinishes : ∀ i, (pathFn i).finish = jacobiTrudiTargetVertexRect N lam i := fun i => by simp only [pathFn, LGV.SimpleDigraph.Path.finish] have h_ca : 0 ≤ ((lam i : ℤ) - (i.val : ℤ)) - ((mu i : ℤ) - (i.val : ℤ)) := by have hcont := hcontained i @@ -7085,11 +7145,11 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) have h := buildVertices_getLast ((mu i : ℤ) - (i.val : ℤ)) ((lam i : ℤ) - (i.val : ℤ)) N (np.paths i).eastStepHeights hN_pos (np.paths i).length_eq h_ca (np.paths i).weaklyIncreasing - simp only [jacobiTrudiTargetVertex, jacobiTrudiTargetX] + simp only [jacobiTrudiTargetVertexRect] rw [← h] -- Construct the PathTuple - let pt : LGV.PathTuple LGV.integerLattice N - (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam) := + let pt : LGV.PathTuple LGV.integerLattice M + (jacobiTrudiSourceVertexRect mu) (jacobiTrudiTargetVertexRect N lam) := ⟨pathFn, hstarts, hfinishes⟩ -- Show pt is non-intersecting have hni : pt.isNonIntersecting := by @@ -7952,7 +8012,7 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) · -- Show pathTupleToNipat pt = np -- Need to show the two Nipat structures are equal -- This follows from the fact that lgvPathToLatticePath ∘ buildVertices = id - simp only [pathTupleToNipat] + simp only [pathTupleToRectNipat] congr 1 funext i simp only [pathTupleToLatticePaths, pt, pathFn] @@ -7970,9 +8030,46 @@ theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) exact lgvYCoordsToFinN_map_val_add_one_eq (np.paths i).eastStepHeights heq _ -- 4. Weight preservation · intro pt hpt - exact pathTupleToNipat_weight lam mu hlam hmu hcontained pt + exact pathTupleToRectNipat_weight N lam mu hlam hmu hcontained pt ((LGV.mem_nipatFinset_iff LGV.integerLattice_pathFinite pt).mp hpt) +/-- At equal path-count and alphabet sizes, rectangular path tuples are the +original `Nipat` objects. -/ +private noncomputable def rectNipatSelfEquiv (lam mu : Fin N → ℕ) + (hlam : ∀ i j : Fin N, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin N, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + RectNipat N lam mu hlam hmu hcontained ≃ + Nipat lam mu hlam hmu hcontained where + toFun p := ⟨p.paths, p.colStrictPaths⟩ + invFun p := ⟨p.paths, p.colStrictPaths⟩ + left_inv p := by cases p; rfl + right_inv p := by cases p; rfl + +/-- Compatibility wrapper retaining the original fixed-size bridge theorem. -/ +theorem lgv_nipatWeightSum_eq_nipatSum (lam mu : Fin N → ℕ) + (hlam : ∀ i j : Fin N, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin N, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + LGV.nipatWeightSum LGV.integerLattice_pathFinite + (jacobiTrudiArcWeight (N := N) (R := R)) + (jacobiTrudiSourceVertex mu) (jacobiTrudiTargetVertex lam) + (Equiv.refl (Fin N)) = + ∑ np : Nipat lam mu hlam hmu hcontained, np.weight (R := R) := by + have hrect := + lgv_nipatWeightSum_eq_rectNipatSum (R := R) N lam mu + (fun h => Nat.pos_of_ne_zero h) hlam hmu hcontained + rw [show jacobiTrudiSourceVertex mu = jacobiTrudiSourceVertexRect mu by rfl, + show jacobiTrudiTargetVertex lam = jacobiTrudiTargetVertexRect N lam by rfl] + rw [hrect] + let e := rectNipatSelfEquiv lam mu hlam hmu hcontained + calc + ∑ p : RectNipat N lam mu hlam hmu hcontained, p.weight (R := R) = + ∑ p : RectNipat N lam mu hlam hmu hcontained, + (e p).weight (R := R) := by rfl + _ = ∑ p : Nipat lam mu hlam hmu hcontained, p.weight (R := R) := + Equiv.sum_comp e (fun p => p.weight) + /-- Key lemma: The Jacobi-Trudi matrix determinant equals the sum of nipat weights. This is the core connection between the LGV lemma and the Jacobi-Trudi formula. From 60419ada050a937bf4d18d56fd311ce8ae84019e Mon Sep 17 00:00:00 2001 From: Codex Date: Sat, 25 Jul 2026 23:03:27 +0000 Subject: [PATCH 6/7] prove independent M N Jacobi-Trudi theorem --- .../SymmetricFunctions/JacobiTrudiMN.lean | 40 +++++++++++++++---- 1 file changed, 32 insertions(+), 8 deletions(-) diff --git a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean index 111a2e10b..d12128d01 100644 --- a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean +++ b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean @@ -459,14 +459,6 @@ noncomputable instance SkewSSYTMN.fintype (N : ℕ) (s : SkewPartition M) : right_inv := fun T => by cases T; rfl } exact Fintype.ofEquiv S e -noncomputable instance NipatMN.fintype (N : ℕ) (lam mu : Fin M → ℕ) - (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) - (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) - (hcontained : ∀ i, mu i ≤ lam i) : - Fintype (NipatMN N lam mu hlam hmu hcontained) := - Fintype.ofEquiv _ - (nipatMNSSYTEquiv (N := N) lam mu hlam hmu hcontained).symm - /-- Summing the independent-size path weights gives the tableau definition of the skew Schur polynomial. -/ theorem nipatMNWeightSum_eq_skewSchurMN (lam mu : Fin M → ℕ) @@ -605,6 +597,25 @@ def JacobiTrudiMNBridge (N : ℕ) (lam mu : Fin M → ℕ) (jacobiTrudiTargetVertexMN N lam) (Equiv.refl (Fin M)) = ∑ np : NipatMN N lam mu hlam hmu hcontained, np.weight (R := R) +/-- The generalized geometric bridge, obtained from the rectangular version of +the repository's full nonintersection/east-step-height proof. -/ +theorem jacobiTrudiMNBridge + (hN : 0 < N) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + JacobiTrudiMNBridge (R := R) N lam mu hlam hmu hcontained := by + unfold JacobiTrudiMNBridge NipatMN.weight + change + LGV.nipatWeightSum LGV.integerLattice_pathFinite + (jacobiTrudiArcWeight (N := N) (R := R)) + (jacobiTrudiSourceVertexRect mu) + (jacobiTrudiTargetVertexRect N lam) (Equiv.refl (Fin M)) = + ∑ np : RectNipat N lam mu hlam hmu hcontained, + np.weight (R := R) + exact lgv_nipatWeightSum_eq_rectNipatSum (R := R) N lam mu + (fun _ => hN) hlam hmu hcontained + /-- Once the geometric path-representation bridge is supplied, the full independent-`M`/`N` Jacobi--Trudi identity follows by the two compiled layers. -/ theorem jacobiTrudi_h_mn_of_bridge @@ -620,6 +631,19 @@ theorem jacobiTrudi_h_mn_of_bridge rw [det_jacobiTrudiMatrixHMN_eq_lgvNipatWeightSum hN lam mu hlam hmu, hbridge, nipatMNWeightSum_eq_skewSchurMN] +/-- First Jacobi--Trudi with independent determinant size `M` and alphabet +size `N`. -/ +theorem jacobiTrudi_h_mn + (hN : 0 < N) (lam mu : Fin M → ℕ) + (hlam : ∀ i j : Fin M, i ≤ j → lam j ≤ lam i) + (hmu : ∀ i j : Fin M, i ≤ j → mu j ≤ mu i) + (hcontained : ∀ i, mu i ≤ lam i) : + skewSchurMN (R := R) N + ⟨⟨lam, hlam⟩, ⟨mu, hmu⟩, fun i => hcontained i⟩ = + (jacobiTrudiMatrixHMN (R := R) N lam mu).det := + jacobiTrudi_h_mn_of_bridge hN lam mu hlam hmu hcontained + (jacobiTrudiMNBridge hN lam mu hlam hmu hcontained) + /-- At equal row and alphabet sizes, a generalized tableau is the original tableau. -/ def skewSSYTMNSelfEquiv (s : SkewPartition N) : SkewSSYTMN N s ≃ SkewSSYT s where toFun T := From 1c6fe58eb682e452b0e8d387335ab2198fa7ac8c Mon Sep 17 00:00:00 2001 From: Codex Date: Sat, 25 Jul 2026 23:08:22 +0000 Subject: [PATCH 7/7] clean generalized Jacobi-Trudi proof warnings --- AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean index d12128d01..a074b00e2 100644 --- a/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean +++ b/AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean @@ -315,11 +315,11 @@ noncomputable def nipatMNToSSYT {lam mu : Fin M → ℕ} (by rw [(np.paths i).length_eq] simp only [sub_sub_sub_cancel_right] - simpa using j.isLt) + simp) (by rw [(np.paths i).length_eq] simp only [sub_sub_sub_cancel_right] - simpa using k.isLt) + simp) hjk colStrict := fun i hi k hcol hk' => by simp only [List.get_eq_getElem]