Grassmannian ASP permutations from Young diagrams

This file begins the permutation-side half of the once-marked/transmission dictionary. A Young diagram lambda determines the finite Ferrers inversion set

{(m,n) : n >= 0, -lambda_n <= m < 0}.

We prove directly that this is an AspSet, then use the reconstruction theorem from Demazure.InvSet with shift zero. Consequently the advertised inversion set and shift are kernel-checked facts, not fields supplied by a generator.

The exact slipface/corner-envelope theorem is completed in GrassmannianEnvelope, using the concrete row and column formulas established below.

def Utilities.grassmannianRowLen (lambda : YoungDiagram) (n : ℤ) : ℕ

The length of the integer-indexed row of a Young diagram, extended by zero on negative indices.

Equations

• Utilities.grassmannianRowLen lambda n = if 0 ≤ n then lambda.rowLen n.toNat else 0

@[simp]

theorem Utilities.grassmannianRowLen_of_nonneg (lambda : YoungDiagram) {n : ℤ} (hn : 0 ≤ n) : grassmannianRowLen lambda n = lambda.rowLen n.toNat

@[simp]

theorem Utilities.grassmannianRowLen_of_neg (lambda : YoungDiagram) {n : ℤ} (hn : n < 0) : grassmannianRowLen lambda n = 0

theorem Utilities.grassmannianRowLen_anti (lambda : YoungDiagram) {m n : ℤ} (hm : 0 ≤ m) (hmn : m ≤ n) : grassmannianRowLen lambda n ≤ grassmannianRowLen lambda m

Integer-indexed row lengths are weakly decreasing on nonnegative indices.

theorem Utilities.rowLen_eq_zero_of_rowLens_length_le (lambda : YoungDiagram) {n : ℕ} (hn : lambda.rowLens.length ≤ n) : lambda.rowLen n = 0

Rows beyond the positive row list have length zero.

def Utilities.grassmannianInvSet (lambda : YoungDiagram) : Set (ℤ × ℤ)

The finite Ferrers inversion diagram of the Grassmannian permutation.

Equations

• Utilities.grassmannianInvSet lambda = {p : ℤ × ℤ | 0 ≤ p.2 ∧ -↑(Utilities.grassmannianRowLen lambda p.2) ≤ p.1 ∧ p.1 < 0}

@[simp]

theorem Utilities.mem_grassmannianInvSet (lambda : YoungDiagram) (m n : ℤ) : (m, n) ∈ grassmannianInvSet lambda ↔ 0 ≤ n ∧ -↑(grassmannianRowLen lambda n) ≤ m ∧ m < 0

theorem Utilities.grassmannianInvSet_prop (lambda : YoungDiagram) : AspSet_prop (grassmannianInvSet lambda)

The Ferrers diagram satisfies the inversion-set axioms.

def Utilities.grassmannianAspSet (lambda : YoungDiagram) : AspSet

The abstract ASP inversion set associated to a Young diagram.

Equations

• Utilities.grassmannianAspSet lambda = { I := Utilities.grassmannianInvSet lambda, prop := ⋯ }

noncomputable def Utilities.grassmannianPermOfYoungDiagram (lambda : YoungDiagram) : AspPerm

The shift-zero Grassmannian ASP permutation associated to a Young diagram.

Equations

• Utilities.grassmannianPermOfYoungDiagram lambda = (Utilities.grassmannianAspSet lambda).toAspPerm 0

@[simp]

theorem Utilities.grassmannianPerm_chi (lambda : YoungDiagram) : (grassmannianPermOfYoungDiagram lambda).χ = 0

theorem Utilities.inv_set_grassmannianPerm (lambda : YoungDiagram) : invSet (grassmannianPermOfYoungDiagram lambda).func = grassmannianInvSet lambda

The reconstructed permutation has exactly the Ferrers inversion set.

theorem Utilities.grassmannianAspSet_outset_eq_empty (lambda : YoungDiagram) {n : ℤ} (hn : 0 ≤ n) : (grassmannianAspSet lambda).outset n = ∅

No nonnegative index is the first coordinate of a Grassmannian inversion.

theorem Utilities.grassmannianAspSet_inset_eq_Ico (lambda : YoungDiagram) {n : ℤ} (hn : 0 ≤ n) : (grassmannianAspSet lambda).inset n = Finset.Ico (-↑(lambda.rowLen n.toNat)) 0

The inset at a nonnegative row is the corresponding integer interval.

theorem Utilities.grassmannianAspSet_outset_eq_Ico (lambda : YoungDiagram) {m : ℤ} (hm : m < 0) : (grassmannianAspSet lambda).outset m = Finset.Ico 0 ↑(lambda.colLen (-m - 1).toNat)

At a negative input, the outset is indexed by one column of the Young diagram.

theorem Utilities.grassmannianPerm_apply_of_nonneg (lambda : YoungDiagram) {n : ℤ} (hn : 0 ≤ n) : (grassmannianPermOfYoungDiagram lambda).func n = n - ↑(lambda.rowLen n.toNat)

On nonnegative indices the reconstructed permutation has the usual Grassmannian formula n - lambda_n.

theorem Utilities.grassmannianPerm_apply_of_neg (lambda : YoungDiagram) {m : ℤ} (hm : m < 0) : (grassmannianPermOfYoungDiagram lambda).func m = m + ↑(lambda.colLen (-m - 1).toNat)

On negative indices the complementary increasing enumeration is described by column lengths of the Young diagram.

theorem Utilities.grassmannianPerm_strictMono_nonnegative (lambda : YoungDiagram) {m n : ℤ} (hm : 0 ≤ m) (hmn : m < n) : (grassmannianPermOfYoungDiagram lambda).func m < (grassmannianPermOfYoungDiagram lambda).func n

The Grassmannian permutation is strictly increasing on its nonnegative input ray.

theorem Utilities.grassmannianPerm_se_finset_eq_Icc_max (lambda : YoungDiagram) {a b : ℤ} (hb : 0 ≤ b) (hNonempty : ((grassmannianPermOfYoungDiagram lambda).seFinset a b).Nonempty) : (grassmannianPermOfYoungDiagram lambda).seFinset a b = Finset.Icc b (((grassmannianPermOfYoungDiagram lambda).seFinset a b).max' hNonempty)

On a nonnegative input ray, a nonempty southeast set is the entire integer interval from its lower endpoint through its maximum.

theorem Utilities.grassmannianPerm_se_card_last_mem (lambda : YoungDiagram) {a b : ℤ} (hb : 0 ≤ b) (hNonempty : ((grassmannianPermOfYoungDiagram lambda).seFinset a b).Nonempty) : b + ↑((grassmannianPermOfYoungDiagram lambda).seFinset a b).card - 1 ∈ (grassmannianPermOfYoungDiagram lambda).seFinset a b

The last element of a nonempty nonnegative southeast set is determined by its cardinality.

theorem Utilities.grassmannianPerm_se_finset_at_row (lambda : YoungDiagram) (i : ℕ) : (grassmannianPermOfYoungDiagram lambda).seFinset (↑i + 1 - ↑(lambda.rowLen i)) 0 = Finset.Ico 0 (↑i + 1)

At the row threshold of i, the southeast set is exactly the first i+1 nonnegative integers.

theorem Utilities.grassmannianPerm_s_at_row (lambda : YoungDiagram) (i : ℕ) : (grassmannianPermOfYoungDiagram lambda).s.func (↑i + 1 - ↑(lambda.rowLen i)) 0 = ↑i + 1

The row threshold has the exact essential slipface value i+1.

def Utilities.grassmannianCellEmbedding (cell : ℕ × ℕ) : ℤ × ℤ

A Young-diagram cell, placed in the negative/nonnegative Ferrers quadrant used for the Grassmannian inversion set.

Equations

• Utilities.grassmannianCellEmbedding cell = (-↑cell.2 - 1, ↑cell.1)

theorem Utilities.grassmannianCellEmbedding_injective : Function.Injective grassmannianCellEmbedding

theorem Utilities.grassmannianInvSet_eq_image_cells (lambda : YoungDiagram) : grassmannianInvSet lambda = grassmannianCellEmbedding '' ↑lambda.cells

The Ferrers inversion set is literally the image of the cells of the Young diagram.

theorem Utilities.grassmannianInvSet_finite (lambda : YoungDiagram) : (grassmannianInvSet lambda).Finite

The inversion set is finite, with no appeal to the ASP reconstruction.

theorem Utilities.ncard_inv_set_grassmannianPerm (lambda : YoungDiagram) : (invSet (grassmannianPermOfYoungDiagram lambda).func).ncard = lambda.card

The inversion number of the Grassmannian permutation is the number of boxes of its Young diagram.

theorem Utilities.grassmannianPerm_onceMarkedCorner_threshold (lambda : YoungDiagram) (c : Corner) : c ∈ onceMarkedCorners lambda → c.2.2 = (grassmannianPermOfYoungDiagram lambda).s.func (c.1 + 1) 0 - 1

Every row stored by onceMarkedCorners records the true slipface value of the reconstructed Grassmannian permutation.

theorem Utilities.grassmannianPerm_cornersDominate_of_nonnegative_b (lambda : YoungDiagram) (a b : ℤ) (hb : 0 ≤ b) : (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) b - 1 < 0 ∨ (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) b - 1 ≤ (grassmannianPermOfYoungDiagram lambda).χ + a - b ∨ ∃ c ∈ onceMarkedCorners lambda, (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) b - 1 ≤ cornerBound c a b

The once-marked rows dominate every transmission test whose second coordinate is nonnegative. This is the direct initial-segment half of the Grassmannian corner-envelope theorem.

theorem Utilities.grassmannianPartitionProfile_of_cornersDominate (lambda : YoungDiagram) (hDom : CornersDominate (grassmannianPermOfYoungDiagram lambda) (onceMarkedCorners lambda)) : GrassmannianPartitionProfile (grassmannianPermOfYoungDiagram lambda) lambda

Once corner domination is established, all the remaining fields of the Grassmannian partition profile follow from the explicit constructor. This isolates the exact envelope theorem still required for the full dictionary.