Skew shapes from 321-avoiding permutations

Every shift-$0$ ASP permutation $\tau$ whose sources and sinks can be separated by a set $U \subseteq \mathbb{Z}$ (equivalently, every shift-$0$ 321-avoiding ASP permutation) is $\sigma_S$ for a skew shape $S$. Given a lattice path whose step $n$ goes east exactly when $n \in U$, the shape has one box $(i(v), j(u))$ for each inversion $(u, v)$ of $\tau$, where $(i(n), j(n))$ is the $n$th vertex of the path. Conversely, every skew shape arises this way from its own boundary path.

The first draft of this file was written by Claude Opus 5.5, following a design by Nathan Pflueger.

structure SkewShapes.LatticePath : Type

A lattice path through $\mathbb{Z} \times \mathbb{Z}$, recorded by the column $c(n)$ of its $n$th vertex. Each step goes east ($c(n+1) = c(n) + 1$) or north ($c(n+1) = c(n)$), and the $n$th vertex is $(c(n) - n, c(n))$, of content $n$.

• col : ℤ → ℤ
• col_succ (n : ℤ) : self.col (n + 1) = self.col n ∨ self.col (n + 1) = self.col n + 1

theorem SkewShapes.LatticePath.ext {x y : LatticePath} (col : x.col = y.col) : x = y

theorem SkewShapes.LatticePath.ext_iff {x y : LatticePath} : x = y ↔ x.col = y.col

def SkewShapes.LatticePath.row (p : LatticePath) (n : ℤ) : ℤ

The row $c(n) - n$ of the $n$th vertex.

Equations

• p.row n = p.col n - n

def SkewShapes.LatticePath.East (p : LatticePath) (n : ℤ) : Prop

Step $n$ of the path goes east.

Equations

• p.East n = (p.col (n + 1) = p.col n + 1)

theorem SkewShapes.LatticePath.col_succ_of_not_east {p : LatticePath} {n : ℤ} (h : ¬p.East n) : p.col (n + 1) = p.col n

theorem SkewShapes.LatticePath.col_mono {p : LatticePath} {a b : ℤ} (h : a ≤ b) : p.col a ≤ p.col b

theorem SkewShapes.LatticePath.col_le_add {p : LatticePath} {a b : ℤ} (h : a ≤ b) : p.col b ≤ p.col a + (b - a)

theorem SkewShapes.LatticePath.row_anti {p : LatticePath} {a b : ℤ} (h : a ≤ b) : p.row b ≤ p.row a

theorem SkewShapes.LatticePath.col_lt_of_east {p : LatticePath} {a b : ℤ} (hab : a < b) (ha : p.East a) : p.col a < p.col b

theorem SkewShapes.LatticePath.row_lt_of_not_east {p : LatticePath} {a b : ℤ} (hab : a < b) (ha : ¬p.East a) : p.row b < p.row a

theorem SkewShapes.LatticePath.le_of_col_le {p : LatticePath} {a b : ℤ} (hb : p.East b) (h : p.col a ≤ p.col b) : a ≤ b

theorem SkewShapes.LatticePath.le_of_row_le {p : LatticePath} {a b : ℤ} (ha : ¬p.East a) (h : p.row a ≤ p.row b) : b ≤ a

theorem SkewShapes.LatticePath.eq_of_col_eq {p : LatticePath} {a b : ℤ} (ha : p.East a) (hb : p.East b) (h : p.col a = p.col b) : a = b

theorem SkewShapes.LatticePath.eq_of_row_eq {p : LatticePath} {a b : ℤ} (ha : ¬p.East a) (hb : ¬p.East b) (h : p.row a = p.row b) : a = b

theorem SkewShapes.LatticePath.col_eq_of_east {p : LatticePath} {a b : ℤ} (hab : a ≤ b) (h : ∀ (n : ℤ), a ≤ n → n < b → p.East n) : p.col b = p.col a + (b - a)

Along a run of east steps, the column increases by one at each step.

theorem SkewShapes.LatticePath.col_eq_of_not_east {p : LatticePath} {a b : ℤ} (hab : a ≤ b) (h : ∀ (n : ℤ), a ≤ n → n < b → ¬p.East n) : p.col b = p.col a

Along a run of north steps, the column is constant.

theorem SkewShapes.LatticePath.exists_col_eq {p : LatticePath} {a b c : ℤ} (hab : a ≤ b) (h1 : p.col a ≤ c) (h2 : c ≤ p.col b) : ∃ (n : ℤ), a ≤ n ∧ n ≤ b ∧ p.col n = c ∧ (n = b ∨ p.East n)

The column takes every value between $c(a)$ and $c(b)$, at the start of an east step or at $b$.

theorem SkewShapes.LatticePath.exists_row_eq {p : LatticePath} {a b r : ℤ} (hab : a ≤ b) (h1 : p.row b ≤ r) (h2 : r ≤ p.row a) : ∃ (n : ℤ), a ≤ n ∧ n ≤ b ∧ p.row n = r ∧ (n = b ∨ ¬p.East n)

The row takes every value between $r(b)$ and $r(a)$, at the start of a north step or at $b$.

structure SkewShapes.LatticePath.Compatible (p : LatticePath) (τ : AspPerm) : Prop

A path is compatible with $\tau$ if the step at each source of an inversion goes east and the step at each sink goes north.

• east (u v : ℤ) : (u, v) ∈ inv_set τ.func → p.East u
• not_east (u v : ℤ) : (u, v) ∈ inv_set τ.func → ¬p.East v

theorem SkewShapes.LatticePath.Compatible.le_of_east {p : LatticePath} {τ : AspPerm} (hc : p.Compatible τ) {u u' : ℤ} (hu : u ≤ u') (he : p.East u') : τ.func u ≤ τ.func u'

For a compatible path, $\tau$ increases from any position to a later east step.

theorem SkewShapes.LatticePath.Compatible.le_of_not_east {p : LatticePath} {τ : AspPerm} (hc : p.Compatible τ) {v v' : ℤ} (hv : v' ≤ v) (he : ¬p.East v') : τ.func v' ≤ τ.func v

For a compatible path, $\tau$ increases from a north step to any later position.

theorem SkewShapes.LatticePath.Compatible.inv_of_nested {p : LatticePath} {τ : AspPerm} (hc : p.Compatible τ) {u₁ v₁ u v : ℤ} (h : (u₁, v₁) ∈ inv_set τ.func) (hu : u₁ ≤ u) (hv : v ≤ v₁) (huv : u < v) (hue : p.East u) (hve : ¬p.East v) : (u, v) ∈ inv_set τ.func

An east step and a later north step nested inside an inversion form an inversion.

def SkewShapes.LatticePath.box (p : LatticePath) (q : ℤ × ℤ) : ℤ × ℤ

The box $(r(v), c(u))$ attached to an inversion $(u, v)$.

Equations

• p.box q = (p.row q.2, p.col q.1)

def SkewShapes.LatticePath.shape (p : LatticePath) (τ : AspPerm) (hc : p.Compatible τ) : SkewShape

The skew shape whose boxes are $(r(v), c(u))$ for the inversions $(u, v)$ of $\tau$.

Equations

• p.shape τ hc = { boxes := p.box '' inv_set τ.func, closed := ⋯, finite_below := ⋯, finite_above := ⋯ }

def SkewShapes.LatticePath.shapeBox {p : LatticePath} {τ : AspPerm} (hc : p.Compatible τ) {u v : ℤ} (h : (u, v) ∈ inv_set τ.func) : ↥(p.shape τ hc)

The box of p.shape τ hc attached to an inversion $(u, v)$ of $\tau$.

Equations

• SkewShapes.LatticePath.shapeBox hc h = ⟨p.box (u, v), ⋯⟩

theorem SkewShapes.LatticePath.shape_u {p : LatticePath} {τ : AspPerm} (hc : p.Compatible τ) {u v : ℤ} (h : (u, v) ∈ inv_set τ.func) : (p.shape τ hc).u (shapeBox hc h) = u

The box attached to the inversion $(u, v)$ has $u$-value $u$.

theorem SkewShapes.LatticePath.shape_v {p : LatticePath} {τ : AspPerm} (hc : p.Compatible τ) {u v : ℤ} (h : (u, v) ∈ inv_set τ.func) : (p.shape τ hc).v (shapeBox hc h) = v

The box attached to the inversion $(u, v)$ has $v$-value $v$.

theorem SkewShapes.LatticePath.shape_σ {p : LatticePath} {τ : AspPerm} (hc : p.Compatible τ) (hχ : τ.χ = 0) : (p.shape τ hc).σ = τ

The permutation of p.shape τ hc is $\tau$, when $\tau$ has shift $0$.

noncomputable def SkewShapes.signedCount (U : Set ℤ) (n : ℤ) : ℤ

The number of elements of $U$ in $[0, n)$, or minus the number in $[n, 0)$ when $n < 0$.

Equations

• SkewShapes.signedCount U n = ↑{x ∈ Finset.Ico 0 n | x ∈ U}.card - ↑{x ∈ Finset.Ico n 0 | x ∈ U}.card

@[simp]

theorem SkewShapes.signedCount_zero (U : Set ℤ) : signedCount U 0 = 0

theorem SkewShapes.signedCount_succ (U : Set ℤ) (n : ℤ) : signedCount U (n + 1) = signedCount U n + if n ∈ U then 1 else 0

theorem SkewShapes.signedCount_add_compl (U : Set ℤ) (n : ℤ) : signedCount U n + signedCount Uᶜ n = n

noncomputable def SkewShapes.LatticePath.ofSet (C : ℤ) (U : Set ℤ) : LatticePath

The path with $c(0) = C$ whose east steps are exactly those in $U$: its $n$th vertex is $(i(n), j(n))$ with $j(n) = C + \#\{m \in [0, n) : m \in U\}$ and $i(n) = C - \#\{m \in [0, n) : m \notin U\}$, counted with sign when $n < 0$.

Equations

• SkewShapes.LatticePath.ofSet C U = { col := fun (n : ℤ) => C + SkewShapes.signedCount U n, col_succ := ⋯ }

theorem SkewShapes.LatticePath.ofSet_col (C : ℤ) (U : Set ℤ) (n : ℤ) : (ofSet C U).col n = C + signedCount U n

theorem SkewShapes.LatticePath.ofSet_row (C : ℤ) (U : Set ℤ) (n : ℤ) : (ofSet C U).row n = C - signedCount Uᶜ n

theorem SkewShapes.LatticePath.ofSet_east_iff (C : ℤ) (U : Set ℤ) (n : ℤ) : (ofSet C U).East n ↔ n ∈ U

theorem SkewShapes.LatticePath.eq_ofSet (p : LatticePath) : p = ofSet (p.col 0) {n : ℤ | p.East n}

Every lattice path is determined by $c(0)$ and its set of east steps.

theorem SkewShapes.LatticePath.ofSet_box (C : ℤ) (U : Set ℤ) (u v : ℤ) : (ofSet C U).box (u, v) = (C - signedCount Uᶜ v, C + signedCount U u)

theorem SkewShapes.LatticePath.ofSet_compatible {τ : AspPerm} {C : ℤ} {U : Set ℤ} (hsrc : ∀ (u v : ℤ), (u, v) ∈ inv_set τ.func → u ∈ U) (hsnk : ∀ (u v : ℤ), (u, v) ∈ inv_set τ.func → v ∉ U) : (ofSet C U).Compatible τ

The path attached to $(C, U)$ is compatible with $\tau$ when $U$ contains every source and no sink of an inversion of $\tau$.

theorem SkewShapes.LatticePath.ofSet_shape_σ {τ : AspPerm} {C : ℤ} {U : Set ℤ} (hsrc : ∀ (u v : ℤ), (u, v) ∈ inv_set τ.func → u ∈ U) (hsnk : ∀ (u v : ℤ), (u, v) ∈ inv_set τ.func → v ∉ U) (hχ : τ.χ = 0) : ((ofSet C U).shape τ ⋯).σ = τ

The skew shape attached to $(\tau, C, U)$: its boxes are $(i(v), j(u))$ for the inversions $(u, v)$ of $\tau$, where $j(n) = C + \#\{m \in [0, n) : m \in U\}$ and $i(n) = C - \#\{m \in [0, n) : m \notin U\}$ (counted with sign when $n < 0$); it has $\sigma = \tau$.

noncomputable def SkewShapes.SkewShape.efBox (S : SkewShape) (hS : S.boxes.Nonempty) (n : ℤ) : ℤ × ℤ

The extended fringe box of content $n$ of a nonempty skew shape.

Equations

• S.efBox hS n = Classical.choose ⋯

theorem SkewShapes.SkewShape.efBox_mem {S : SkewShape} (hS : S.boxes.Nonempty) (n : ℤ) : S.efBox hS n ∈ S.ext_fringe

theorem SkewShapes.SkewShape.Δ_efBox {S : SkewShape} (hS : S.boxes.Nonempty) (n : ℤ) : Δ (S.efBox hS n) = n

theorem SkewShapes.SkewShape.efBox_eq {S : SkewShape} (hS : S.boxes.Nonempty) {x : ℤ × ℤ} (hx : x ∈ S.ext_fringe) : S.efBox hS (Δ x) = x

noncomputable def SkewShapes.fringePath (S : SkewShape) (hS : S.boxes.Nonempty) : LatticePath

The southeast boundary of a nonempty skew shape, as a lattice path: its $n$th vertex is the extended fringe box of content $n$.

Equations

• SkewShapes.fringePath S hS = { col := fun (n : ℤ) => (S.efBox hS n).2, col_succ := ⋯ }

theorem SkewShapes.fringePath_compatible {S : SkewShape} (hS : S.boxes.Nonempty) : (fringePath S hS).Compatible S.σ

The boundary path of $S$ is compatible with $\sigma_S$.

theorem SkewShapes.fringePath_box_pair {S : SkewShape} (hS : S.boxes.Nonempty) (x : ↥S) : (fringePath S hS).box (S.u x, S.v x) = ↑x

The box attached to the pair of $x$ along the boundary path of $S$ is $x$ itself.

theorem SkewShapes.exists_compatible_shape_eq (S : SkewShape) : ∃ (p : LatticePath) (hc : p.Compatible S.σ), p.shape S.σ hc = S

Every skew shape arises from its permutation by the construction above, using its boundary path.

theorem SkewShapes.exists_ofSet_shape_eq (S : SkewShape) : ∃ (C : ℤ) (U : Set ℤ) (hc : (LatticePath.ofSet C U).Compatible S.σ), (LatticePath.ofSet C U).shape S.σ hc = S

Every skew shape $S$ is the shape attached to $(\sigma_S, C, U)$ for some $C$ and some $U$ containing every source and no sink of an inversion of $\sigma_S$.