Hasse Walks in Young's Lattice

This file formalizes Lemma 8.1 from Stanley's Algebraic Combinatorics, which characterizes when a word w = D^{s_k} U^{r_k} ⋯ D^{s_1} U^{r_1} admits a Hasse walk from ∅ to a partition λ ⊢ n in Young's lattice.

inductive HasseWalks.HStep : Type

A step in a Hasse walk: Up (adding a cell) or Down (removing a cell).

• U : HStep
• D : HStep

@[implicit_reducible]

instance HasseWalks.instDecidableEqHStep : DecidableEq HStep

def HasseWalks.instReprHStep.repr : HStep → ℕ → Std.Format

@[implicit_reducible]

instance HasseWalks.instReprHStep : Repr HStep

def HasseWalks.HStep.toInt : HStep → ℤ

The integer value of a step: U ↦ +1, D ↦ -1.

def HasseWalks.expandBlock (p : ℕ × ℕ) : List HStep

Expand a block (r, s) into the step list U^r ++ D^s.

def HasseWalks.expandBlocks (w : List (ℕ × ℕ)) : List HStep

Expand a word (list of blocks) into a flat list of steps.

def HasseWalks.displacement (w : List (ℕ × ℕ)) : ℤ

Total displacement of a word: ∑(r_i - s_i).

def HasseWalks.partialDisplacement (w : List (ℕ × ℕ)) (j : ℕ) : ℤ

Partial displacement after the first j blocks.

def HasseWalks.IsValidWord (w : List (ℕ × ℕ)) (n : ℕ) : Prop

A word w is valid for n if ∑(r_i - s_i) = n and all partial sums ≥ 0.

structure HasseWalks.HasseWalk (steps : List HStep) (start target : YoungDiagram) : Type

A Hasse walk of given step-type in Young's lattice.

• diagram : Fin (steps.length + 1) → YoungDiagram
• start_eq : self.diagram ⟨0, ⋯⟩ = start
• target_eq : self.diagram ⟨steps.length, ⋯⟩ = target
• step_up (i : Fin steps.length) : steps[i] = HStep.U → self.diagram ⟨↑i, ⋯⟩ ⋖ self.diagram ⟨↑i + 1, ⋯⟩
• step_down (i : Fin steps.length) : steps[i] = HStep.D → self.diagram ⟨↑i + 1, ⋯⟩ ⋖ self.diagram ⟨↑i, ⋯⟩

Covering changes cardinality by 1

theorem HasseWalks.isLowerSet_insert_minimal {μ ν : YoungDiagram} (m : ℕ × ℕ) (hm_ν : m ∈ ν.cells) (hm_nμ : m ∉ μ.cells) (h_below : ∀ c ∈ ν.cells, c.1 ≤ m.1 → c.2 ≤ m.2 → c ≠ m → c ∈ μ.cells) : IsLowerSet ↑(Finset.cons m μ.cells hm_nμ)

theorem HasseWalks.card_covBy_succ {μ ν : YoungDiagram} (h : μ ⋖ ν) : ν.card = μ.card + 1

Covering in Young's lattice changes cardinality by exactly 1.

Expansion lemmas

theorem HasseWalks.expandBlock_toInt_sum (p : ℕ × ℕ) : (List.map HStep.toInt (expandBlock p)).sum = ↑p.1 - ↑p.2

theorem HasseWalks.expandBlocks_toInt_sum (w : List (ℕ × ℕ)) : (List.map HStep.toInt (expandBlocks w)).sum = displacement w

theorem HasseWalks.expandBlocks_append (w₁ w₂ : List (ℕ × ℕ)) : expandBlocks (w₁ ++ w₂) = expandBlocks w₁ ++ expandBlocks w₂

Walk card tracking

theorem HasseWalks.walk_card_step {steps : List HStep} {start target : YoungDiagram} (walk : HasseWalk steps start target) (i : Fin steps.length) : ↑(walk.diagram ⟨↑i + 1, ⋯⟩).card = ↑(walk.diagram ⟨↑i, ⋯⟩).card + steps[i].toInt

theorem HasseWalks.walk_card_eq {steps : List HStep} {start target : YoungDiagram} (walk : HasseWalk steps start target) (k : ℕ) (hk : k ≤ steps.length) : ↑(walk.diagram ⟨k, ⋯⟩).card = ↑start.card + (List.map HStep.toInt (List.take k steps)).sum

Main theorem: Lemma 8.1

theorem HasseWalks.walk_exists_necessity (w : List (ℕ × ℕ)) (lam : YoungDiagram) (n : ℕ) (hn : lam.card = n) (walk : HasseWalk (expandBlocks w) ⊥ lam) : IsValidWord w n

Lemma 8.1 (necessity).

Helpers for sufficiency

theorem HasseWalks.card_zero_eq_bot {μ : YoungDiagram} (h : μ.card = 0) : μ = ⊥

theorem HasseWalks.exists_covBy_below {ν : YoungDiagram} (hν : 0 < ν.card) : ∃ (μ : YoungDiagram), μ ⋖ ν

theorem HasseWalks.exists_covBy_above (μ : YoungDiagram) : ∃ (ν : YoungDiagram), μ ⋖ ν

theorem HasseWalks.nonempty_walk_extend {s : List HStep} {a : HStep} {mid target : YoungDiagram} (hw : Nonempty (HasseWalk s ⊥ mid)) (hU : a = HStep.U → mid ⋖ target) (hD : a = HStep.D → target ⋖ mid) : Nonempty (HasseWalk (s ++ [a]) ⊥ target)

theorem HasseWalks.walk_from_bot_exists (s : List HStep) (target : YoungDiagram) (hcard : ↑target.card = (List.map HStep.toInt s).sum) (hpartial : ∀ k ≤ s.length, 0 ≤ (List.map HStep.toInt (List.take k s)).sum) : Nonempty (HasseWalk s ⊥ target)

For any step list with non-negative partial sums from 0, and any target of the right size, there exists a Hasse walk from ⊥ to target.

theorem HasseWalks.expandBlocks_partial_nonneg_aux (w : List (ℕ × ℕ)) (base : ℤ) (hbase : 0 ≤ base) (hpartial : ∀ (j : ℕ), 1 ≤ j → j ≤ w.length → 0 ≤ base + partialDisplacement w j) (k : ℕ) (hk : k ≤ (expandBlocks w).length) : 0 ≤ base + (List.map HStep.toInt (List.take k (expandBlocks w))).sum

theorem HasseWalks.walk_exists_sufficiency (w : List (ℕ × ℕ)) (lam : YoungDiagram) (n : ℕ) (hn : lam.card = n) (hvalid : IsValidWord w n) : Nonempty (HasseWalk (expandBlocks w) ⊥ lam)

Lemma 8.1 (sufficiency).

theorem HasseWalks.valid_word_iff_walk_exists (w : List (ℕ × ℕ)) (lam : YoungDiagram) (n : ℕ) (hn : lam.card = n) : Nonempty (HasseWalk (expandBlocks w) ⊥ lam) ↔ IsValidWord w n

Lemma 8.1 (Stanley). Walk exists iff word is valid.