Weak orders on skew shapes and two-term factorizations

This file defines the left and right weak orders $S' \le_L S$ and $S' \le_R S$ on skew shapes and shows that they correspond, via $S' \mapsto \sigma_{S'}$, to the left and right weak orders on shift-$0$ ASP permutations below $\sigma_S$. It then classifies the Demazure factorizations $\sigma_S = \alpha \star \beta$ into two shift-$0$ factors: they correspond to pairs of shapes $A \le_R S$ and $B \le_L S$ with $A \cup B = S$ such that no two boxes of $A \cap B$ share a row or a column.

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

def SkewShapes.lelSet (P : Set (ℤ × ℤ)) (T : SkewShape) : Prop

A set $P$ of boxes of $T$ that is closed to the southeast within $T$: whenever $x \le y$ are boxes of $T$ with $x \in P$, also $y \in P$.

Equations

• SkewShapes.lelSet P T = (P ⊆ T.boxes ∧ ∀ x ∈ T, ∀ y ∈ T, x ≤ y → x ∈ P → y ∈ P)

def SkewShapes.lerSet (P : Set (ℤ × ℤ)) (T : SkewShape) : Prop

A set $P$ of boxes of $T$ that is closed to the northwest within $T$: whenever $x \le y$ are boxes of $T$ with $y \in P$, also $x \in P$.

Equations

• SkewShapes.lerSet P T = (P ⊆ T.boxes ∧ ∀ x ∈ T, ∀ y ∈ T, x ≤ y → y ∈ P → x ∈ P)

def SkewShapes.lel (S T : SkewShape) : Prop

The left weak order on skew shapes: $S \le_L T$ when $S \subseteq T$ and $S$ is closed to the southeast within $T$. It corresponds to the left weak order on $\sigma$.

Equations

• (S ≤L T) = SkewShapes.lelSet S.boxes T

def SkewShapes.«term_≤L_» : Lean.TrailingParserDescr

Equations

• SkewShapes.«term_≤L_» = Lean.ParserDescr.trailingNode `SkewShapes.«term_≤L_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤L ") (Lean.ParserDescr.cat `term 51))

def SkewShapes.ler (S T : SkewShape) : Prop

The right weak order on skew shapes: $S \le_R T$ when $S \subseteq T$ and $S$ is closed to the northwest within $T$. It corresponds to the right weak order on $\sigma$.

Equations

• (S ≤R T) = SkewShapes.lerSet S.boxes T

def SkewShapes.«term_≤R_» : Lean.TrailingParserDescr

Equations

• SkewShapes.«term_≤R_» = Lean.ParserDescr.trailingNode `SkewShapes.«term_≤R_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤R ") (Lean.ParserDescr.cat `term 51))

def SkewShapes.lel.box {S S' : SkewShape} (h : S' ≤L S) (x : ↥S') : ↥S

A box of $S' \le_L S$, regarded as a box of $S$.

Equations

• h.box x = ⟨↑x, ⋯⟩

@[simp]

theorem SkewShapes.lel.box_val {S S' : SkewShape} (h : S' ≤L S) (x : ↥S') : ↑(h.box x) = ↑x

theorem SkewShapes.lel.U_eq {S S' : SkewShape} (h : S' ≤L S) (x : ↥S') : S'.U x = S.U (h.box x)

Passing to $S' \le_L S$ does not change $U$.

theorem SkewShapes.lel.V_eq {S S' : SkewShape} (h : S' ≤L S) (x : ↥S') : S'.V x = S.V (h.box x)

Passing to $S' \le_L S$ does not change $V$.

theorem SkewShapes.lel.u_eq {S S' : SkewShape} (h : S' ≤L S) (x : ↥S') : S'.u x = S.u (h.box x)

theorem SkewShapes.lel.v_eq {S S' : SkewShape} (h : S' ≤L S) (x : ↥S') : S'.v x = S.v (h.box x)

theorem SkewShapes.lel.mem_iff {S S' : SkewShape} (h : S' ≤L S) (x : ↥S) : ↑x ∈ S' ↔ (S.u x, S.v x) ∈ S'.I

A box $x$ of $S$ lies in $S' \le_L S$ exactly when its pair $(u(x), v(x))$ lies in $I(S')$.

theorem SkewShapes.lel.I_subset {S S' : SkewShape} (h : S' ≤L S) : S'.I ⊆ S.I

theorem SkewShapes.lel.σ_lel {S S' : SkewShape} (h : S' ≤L S) : S'.σ ≤L S.σ

theorem SkewShapes.lel.eq_of_σ_eq {S S' S'' : SkewShape} (h' : S' ≤L S) (h'' : S'' ≤L S) (hσ : S'.σ = S''.σ) : S' = S''

Two shapes below $S$ in left weak order with the same $\sigma$ are equal.

theorem SkewShapes.restrict_lel {S : SkewShape} {P : ↥S → Prop} {hP : ∀ (x y : ↥S), ↑x ≤ ↑y → P x → P y} : S.restrict P hP ≤L S

theorem SkewShapes.exists_lel_of_lel {S : SkewShape} {τ : AspPerm} (hχ : τ.χ = 0) (hle : τ ≤L S.σ) : ∃ (S' : SkewShape), S' ≤L S ∧ S'.σ = τ

Every shift-$0$ permutation below $\sigma_S$ in left weak order is $\sigma_{S'}$ for some $S' \le_L S$.

noncomputable def SkewShapes.lelEquiv (S : SkewShape) : { S' : SkewShape // S' ≤L S } ≃ { τ : AspPerm // τ.χ = 0 ∧ τ ≤L S.σ }

The skew shapes below $S$ in left weak order correspond bijectively, via $S' \mapsto \sigma_{S'}$, to the shift-$0$ ASP permutations below $\sigma_S$ in left weak order.

Equations

• SkewShapes.lelEquiv S = Equiv.ofBijective (fun (S' : { S' : SkewShapes.SkewShape // S' ≤L S }) => ⟨(↑S').σ, ⋯⟩) ⋯

@[simp]

theorem SkewShapes.lelEquiv_apply {S : SkewShape} (S' : { S' : SkewShape // S' ≤L S }) : ↑((lelEquiv S) S') = (↑S').σ

theorem SkewShapes.lelEquiv_symm_σ {S S' : SkewShape} (h : S' ≤L S) (h' : S'.σ.χ = 0 ∧ S'.σ ≤L S.σ) : ↑((lelEquiv S).symm ⟨S'.σ, h'⟩) = S'

The right weak order, by reflection

theorem SkewShapes.ler.flip_lel {S S' : SkewShape} (h : S' ≤R S) : S'.flip ≤L S.flip

theorem SkewShapes.lel.flip_ler {S S' : SkewShape} (h : S' ≤L S) : S'.flip ≤R S.flip

theorem SkewShapes.lelSet_self (S : SkewShape) : lelSet S.boxes S

theorem SkewShapes.lelSet_empty (S : SkewShape) : lelSet ∅ S

theorem SkewShapes.lerSet_empty (S : SkewShape) : lerSet ∅ S

theorem SkewShapes.lelSet.of_subset {S : SkewShape} {P : Set (ℤ × ℤ)} {T : SkewShape} (h : lelSet P T) (hT : S.boxes ⊆ T.boxes) (hP : P ⊆ S.boxes) : lelSet P S

theorem SkewShapes.lelSet.trans {S S' : SkewShape} {P : Set (ℤ × ℤ)} (h : lelSet P S') (hS' : S' ≤L S) : lelSet P S

def SkewShapes.ofLelSet (T : SkewShape) (P : Set (ℤ × ℤ)) (h : lelSet P T) : SkewShape

A set of boxes closed to the southeast within a skew shape is itself a skew shape.

Equations

• SkewShapes.ofLelSet T P h = { boxes := P, closed := ⋯, finite_below := ⋯, finite_above := ⋯ }

theorem SkewShapes.ofLelSet_lel {T : SkewShape} {P : Set (ℤ × ℤ)} (h : lelSet P T) : ofLelSet T P h ≤L T

theorem SkewShapes.ler.σ_ler {S S' : SkewShape} (h : S' ≤R S) : S'.σ ≤R S.σ

theorem SkewShapes.lel.inv_set_σ {S S' : SkewShape} (h : S' ≤L S) : inv_set S'.σ.func = S.pair '' {x : ↥S | ↑x ∈ S'}

For $S' \le_L S$, the inversions of $\sigma_{S'}$ are the pairs of the boxes of $S'$.

theorem SkewShapes.ler.sr_image {S S' : SkewShape} (h : S' ≤R S) : S.σ.sr S'.σ '' inv_set S'.σ.func = S.pair '' {x : ↥S | ↑x ∈ S'}

For $S' \le_R S$, the inversions of $\sigma_{S'}$, slid into $\sigma_S$, are the pairs of the boxes of $S'$.

def SkewShapes.lerEquivFlip (S : SkewShape) : { S' : SkewShape // S' ≤R S } ≃ { S'' : SkewShape // S'' ≤L S.flip }

Reflection matches the shapes below $S$ in right weak order with the shapes below the reflection of $S$ in left weak order.

Equations

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

noncomputable def SkewShapes.lerEquiv (S : SkewShape) : { S' : SkewShape // S' ≤R S } ≃ { τ : AspPerm // τ.χ = 0 ∧ τ ≤R S.σ }

The skew shapes below $S$ in right weak order correspond bijectively, via $S' \mapsto \sigma_{S'}$, to the shift-$0$ ASP permutations below $\sigma_S$ in right weak order.

Equations

• SkewShapes.lerEquiv S = (SkewShapes.lerEquivFlip S).trans ((SkewShapes.lelEquiv S.flip).trans (Equiv.subtypeEquiv (Equiv.inv AspPerm) ⋯))

@[simp]

theorem SkewShapes.lerEquiv_apply {S : SkewShape} (S' : { S' : SkewShape // S' ≤R S }) : ↑((lerEquiv S) S') = (↑S').σ

theorem SkewShapes.lerEquiv_symm_σ {S S' : SkewShape} (h : S' ≤R S) (h' : S'.σ.χ = 0 ∧ S'.σ ≤R S.σ) : ↑((lerEquiv S).symm ⟨S'.σ, h'⟩) = S'

theorem SkewShapes.ler.eq_of_σ_eq {S S' S'' : SkewShape} (h' : S' ≤R S) (h'' : S'' ≤R S) (hσ : S'.σ = S''.σ) : S' = S''

Two shapes below $S$ in right weak order with the same $\sigma$ are equal.

def SkewShapes.nonattacking (C : Set (ℤ × ℤ)) : Prop

A set of boxes is nonattacking if no two of its boxes share a row or a column.

Equations

• SkewShapes.nonattacking C = ∀ x ∈ C, ∀ y ∈ C, x.1 = y.1 ∨ x.2 = y.2 → x = y

theorem SkewShapes.nonattacking.mono {C D : Set (ℤ × ℤ)} (h : nonattacking C) (hD : D ⊆ C) : nonattacking D

theorem SkewShapes.nonattacking_empty : nonattacking ∅

theorem SkewShapes.le_or_le_of_row_or_col {x y : ℤ × ℤ} (h : x.1 = y.1 ∨ x.2 = y.2) : x ≤ y ∨ y ≤ x

Two boxes in the same row or the same column are comparable.

theorem SkewShapes.eq_of_le_of_mem_inter {S : SkewShape} {P Q : Set (ℤ × ℤ)} (hP : lerSet P S) (hQ : lelSet Q S) (hna : nonattacking (P ∩ Q)) {x y : ℤ × ℤ} (hx : x ∈ P ∩ Q) (hy : y ∈ P ∩ Q) (hxy : x ≤ y) : x = y

If $P$ is closed to the northwest and $Q$ to the southeast within $S$, and $P \cap Q$ is nonattacking, then $P \cap Q$ is an antichain.

theorem SkewShapes.dprod_iff {S A B : SkewShape} (hA : A ≤R S) (hB : B ≤L S) : A.σ ⋆ B.σ = S.σ ↔ A.boxes ∪ B.boxes = S.boxes ∧ nonattacking (A.boxes ∩ B.boxes)

For $A \le_R S$ and $B \le_L S$, we have $\sigma_A \star \sigma_B = \sigma_S$ exactly when $A \cup B = S$ and no two boxes of $A \cap B$ share a row or a column.

structure SkewShapes.ShapeFactorization (S : SkewShape) : Type

A factorization of a skew shape $S$: shapes $A \le_R S$ and $B \le_L S$ with $A \cup B = S$ and no two boxes of $A \cap B$ in the same row or column.

• A : SkewShape
• B : SkewShape
• hA : self.A ≤R S
• hB : self.B ≤L S
• union_eq : self.A.boxes ∪ self.B.boxes = S.boxes
• inter_nonattacking : nonattacking (self.A.boxes ∩ self.B.boxes)

theorem SkewShapes.ShapeFactorization.ext_iff {S : SkewShape} {x y : ShapeFactorization S} : x = y ↔ x.A = y.A ∧ x.B = y.B

theorem SkewShapes.ShapeFactorization.ext {S : SkewShape} {x y : ShapeFactorization S} (A : x.A = y.A) (B : x.B = y.B) : x = y

@[reducible, inline]

abbrev SkewShapes.DemazureFactorization (S : SkewShape) : Type

Demazure factorizations $\sigma_S = \alpha \star \beta$ into two shift-$0$ factors.

Equations

• SkewShapes.DemazureFactorization S = { p : AspPerm × AspPerm // p.1.χ = 0 ∧ p.2.χ = 0 ∧ p.1 ⋆ p.2 = S.σ }

noncomputable def SkewShapes.ShapeFactorization.ofDprod {S : SkewShape} (p : DemazureFactorization S) : ShapeFactorization S

The factorization of $S$ attached to a Demazure factorization of $\sigma_S$: its pieces are the shapes whose permutations are the two factors.

Equations

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

theorem SkewShapes.ShapeFactorization.ofDprod_A_σ {S : SkewShape} (p : DemazureFactorization S) : (ofDprod p).A.σ = (↑p).1

theorem SkewShapes.ShapeFactorization.ofDprod_B_σ {S : SkewShape} (p : DemazureFactorization S) : (ofDprod p).B.σ = (↑p).2

noncomputable def SkewShapes.shapeFactorizationEquiv (S : SkewShape) : ShapeFactorization S ≃ DemazureFactorization S

Factorizations of the skew shape $S$ correspond bijectively, via $(A, B) \mapsto (\sigma_A, \sigma_B)$, to Demazure factorizations of $\sigma_S$ into two shift-$0$ factors.

Equations

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

@[simp]

theorem SkewShapes.shapeFactorizationEquiv_apply {S : SkewShape} (F : ShapeFactorization S) : ↑((shapeFactorizationEquiv S) F) = (F.A.σ, F.B.σ)