321-avoiding permutations

This file gives a characterization of the two-term Demazure factorizations of 321-avoiding permutations (not necessarily of finite length), which are all automatically in $\mathrm{ASP}$.

This material is not present in An extended Demazure product.

def LeanPool.DemazureProduct.is321a (τ : ℤ → ℤ) : Prop

The 321-avoidance condition used in this file: every triple i < j < k has either τ i < τ j or τ j < τ k.

Equations

• LeanPool.DemazureProduct.is321a τ = ∀ (i j k : ℤ), i < j → j < k → τ i < τ j ∨ τ j < τ k

structure LeanPool.DemazureProduct.ASP321a.set_321a_prop (I : Set (ℤ × ℤ)) : Prop

The abstract version of 321-avoidance for an ASP set: ASP-set axioms together with triangle-freeness.

• asp : AspSet_prop I
• tfree (u v w : ℤ) : (u, v) ∉ I ∨ (v, w) ∉ I

structure LeanPool.DemazureProduct.ASP321a.tfasextends LeanPool.DemazureProduct.AspSet : Type

A triangle-free ASP set.

• I : Set (ℤ × ℤ)
• prop : AspSet_prop self.I
• prop_321a : set_321a_prop self.I

Every 321-avoiding permutation of the integers is almost-sign-preserving.

theorem LeanPool.DemazureProduct.ASP321a.is_asp_of_is_321a (τ : ℤ → ℤ) (h_bij : Function.Bijective τ) (h_321a : is321a τ) : isAsp τ

theorem LeanPool.DemazureProduct.ASP321a.is_321a_iff_set_321a_prop (τ : ℤ → ℤ) (hperm : Function.Bijective τ) : is321a τ ↔ set_321a_prop (invSet τ)

A bijection of ℤ is 321-avoiding exactly when its inversion set is a triangle-free ASP set.

def LeanPool.DemazureProduct.ASP321a.tfasOfPerm {τ : AspPerm} (h_321a : is321a τ.func) : tfas

The triangle-free abstract ASP set associated to a 321-avoiding ASP permutation.

Equations

• LeanPool.DemazureProduct.ASP321a.tfasOfPerm h_321a = { toAspSet := LeanPool.DemazureProduct.AspSet.ofAspPerm τ, prop_321a := ⋯ }

noncomputable def LeanPool.DemazureProduct.ASP321a.perm321aEquivTfas : ↑{τ : AspPerm | is321a τ.func} ≃ tfas × ℤ

321-avoiding ASP permutations are equivalent to triangle-free ASP sets together with a shift parameter.

Equations

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

theorem LeanPool.DemazureProduct.ASP321a.inv_321a_char (I : Set (ℤ × ℤ)) : set_321a_prop I ↔ ∃ (τ : ℤ → ℤ), is321a τ ∧ Function.Bijective τ ∧ invSet τ = I

Characterize the sets of boxes that arise as inversion sets of 321-avoiding ASP permutations.

def LeanPool.DemazureProduct.ASP321a.isSrc (τ : AspPerm) (u : ℤ) : Prop

An index is a source if it is the first coordinate of an inversion.

Equations

• LeanPool.DemazureProduct.ASP321a.isSrc τ u = ∃ (v : ℤ), (u, v) ∈ LeanPool.DemazureProduct.invSet τ.func

theorem LeanPool.DemazureProduct.ASP321a.src_of_inv {τ : AspPerm} {u v : ℤ} (uv_inv : (u, v) ∈ invSet τ.func) : isSrc τ u

def LeanPool.DemazureProduct.ASP321a.isSnk (τ : AspPerm) (v : ℤ) : Prop

An index is a sink if it is the second coordinate of an inversion.

Equations

• LeanPool.DemazureProduct.ASP321a.isSnk τ v = ∃ (u : ℤ), (u, v) ∈ LeanPool.DemazureProduct.invSet τ.func

theorem LeanPool.DemazureProduct.ASP321a.snk_of_inv {τ : AspPerm} {u v : ℤ} (uv_inv : (u, v) ∈ invSet τ.func) : isSnk τ v

Source and sink geometry for a fixed 321-avoiding permutation

Fix a 321-avoiding ASP permutation τ. This section develops the source/sink geometry and the duality identities for s and s' that drive the later factorization arguments.

theorem LeanPool.DemazureProduct.ASP321a.inv_is_321a {τ : AspPerm} (h_321a : is321a τ.func) : is321a τ⁻¹.func

theorem LeanPool.DemazureProduct.ASP321a.not_src_and_snk {τ : AspPerm} (h_321a : is321a τ.func) (n : ℤ) : ¬isSrc τ n ∨ ¬isSnk τ n

theorem LeanPool.DemazureProduct.ASP321a.snk_lt {τ : AspPerm} (h_321a : is321a τ.func) {v x : ℤ} (v_snk : isSnk τ v) (v_lt_x : v < x) : τ.func v < τ.func x

theorem LeanPool.DemazureProduct.ASP321a.snk_le {τ : AspPerm} (h_321a : is321a τ.func) {v x : ℤ} (v_snk : isSnk τ v) (v_le_x : v ≤ x) : τ.func v ≤ τ.func x

theorem LeanPool.DemazureProduct.ASP321a.src_gt {τ : AspPerm} (h_321a : is321a τ.func) {u x : ℤ} (u_src : isSrc τ u) (x_lt_u : x < u) : τ.func x < τ.func u

theorem LeanPool.DemazureProduct.ASP321a.src_ge {τ : AspPerm} (h_321a : is321a τ.func) {u x : ℤ} (u_src : isSrc τ u) (x_le_u : x ≤ u) : τ.func x ≤ τ.func u

structure LeanPool.DemazureProduct.ASP321a.between_inv_prop {τ : AspPerm} (u x v : ℤ) : Prop

The inversion-pattern data forced for an index between an inversion pair.

• src_or_snk : isSrc τ x ∨ isSnk τ x

  The middle index is either a source or a sink.

• src_iff_right_inv : isSrc τ x ↔ (x, v) ∈ invSet τ.func

  Source status is equivalent to the right inversion.

• src_iff_left_ninv : isSrc τ x ↔ (u, x) ∉ invSet τ.func

  Source status is equivalent to absence of the left inversion.

• snk_iff_left_inv : isSnk τ x ↔ (u, x) ∈ invSet τ.func

  Sink status is equivalent to the left inversion.

• snk_iff_right_ninv : isSnk τ x ↔ (x, v) ∉ invSet τ.func

  Sink status is equivalent to absence of the right inversion.

theorem LeanPool.DemazureProduct.ASP321a.between_inv {τ : AspPerm} (h_321a : is321a τ.func) {u x v : ℤ} (uv_inv : (u, v) ∈ invSet τ.func) (u_le_x : u ≤ x) (x_le_v : x ≤ v) : between_inv_prop u x v

theorem LeanPool.DemazureProduct.ASP321a.inv_of_quadrants {τ : AspPerm} {a b u v : ℤ} (hu : u ∈ northwestSet τ.func a b) (hv : v ∈ southeastSet τ.func a b) : (u, v) ∈ invSet τ.func

theorem LeanPool.DemazureProduct.ASP321a.split_s {τ : AspPerm} (h_321a : is321a τ.func) {u v a b : ℤ} (u_lt_b : u < b) (b_le_v : b ≤ v) (τv_lt_a : τ.func v < a) (τu_ge_a : τ.func u ≥ a) : τ.s.func a v + τ.s.func (τ.func v) b = τ.s.func a b

theorem LeanPool.DemazureProduct.ASP321a.uv_duality {τ : AspPerm} (h_321a : is321a τ.func) {u a b : ℤ} (u_lt_b : u < b) (τu_ge_a : τ.func u ≥ a) {m m' : ℤ} (m_pos : m > 0) (m'_pos : m' > 0) (m_sum : m + m' = τ.s.func a b + 1) : τ.func (τ.v b m_pos) = τ⁻¹.u a m'_pos

theorem LeanPool.DemazureProduct.ASP321a.uv_duality_ge {τ : AspPerm} (h_321a : is321a τ.func) {a b m m' : ℤ} (m_pos : m > 0) (m'_pos : m' > 0) (m_sum : m + m' = τ.s.func a b + 1) : isSnk τ (τ.v b m_pos) → isSnk τ (τ⁻¹.func (τ⁻¹.u a m'_pos)) → τ.func (τ.v b m_pos) ≥ τ⁻¹.u a m'_pos ∧ τ.v b m_pos ≥ τ⁻¹.func (τ⁻¹.u a m'_pos)

theorem LeanPool.DemazureProduct.ASP321a.uv_duality_lt {τ : AspPerm} (h_321a : is321a τ.func) (a b : ℤ) {m m' : ℤ} (m_pos : m > 0) (m'_pos : m' > 0) (h_sum : m + m' ≥ τ.s.func a b + 2) : have v := τ.v b m_pos; have w := τ⁻¹.u a m'_pos; isSnk τ v → isSnk τ (τ⁻¹.func w) → τ⁻¹.func w < v

theorem LeanPool.DemazureProduct.ASP321a.split_s' {τ : AspPerm} (h_321a : is321a τ.func) {u v a b : ℤ} (u_lt_b : u < b) (b_le_v : b ≤ v) (τv_lt_a : τ.func v < a) (τu_ge_a : τ.func u ≥ a) : τ⁻¹.s.func b (τ.func u) + τ⁻¹.s.func u a = τ⁻¹.s.func b a

Passing to left weak order subpermutations

Here β ≤L τ is fixed. The lemmas compare the inversion geometry of β and τ, especially the way ramps, sources, sinks, and shifted inversion sets are inherited along left weak order.

theorem LeanPool.DemazureProduct.ASP321a.src_of_src {τ β : AspPerm} (h_L : β ≤L τ) {n : ℤ} (h_src : isSrc β n) : isSrc τ n

theorem LeanPool.DemazureProduct.ASP321a.snk_of_snk {τ β : AspPerm} (h_L : β ≤L τ) {n : ℤ} (h_snk : isSnk β n) : isSnk τ n

theorem LeanPool.DemazureProduct.ASP321a.is_321a_of_lel {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) : is321a β.func

structure LeanPool.DemazureProduct.ASP321a.between_inv_lel_prop (β τ : AspPerm) (u x v : ℤ) : Prop

Compatibility of between_inv_prop under a left weak-order comparison.

• propτ : between_inv_prop u x v

  The pattern for the larger permutation.

• propβ : between_inv_prop u x v

  The pattern for the smaller permutation.

• inv_iff_left : (u, x) ∈ invSet β.func ↔ (u, x) ∈ invSet τ.func

  Left inversion membership agrees in both permutations.

• inv_iff_right : (x, v) ∈ invSet β.func ↔ (x, v) ∈ invSet τ.func

  Right inversion membership agrees in both permutations.

• src_iff : isSrc β x ↔ isSrc τ x
• snk_iff : isSnk β x ↔ isSnk τ x

theorem LeanPool.DemazureProduct.ASP321a.between_inv_lel {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u x v : ℤ} (uv_inv : (u, v) ∈ invSet β.func) (u_le_x : u ≤ x) (x_le_v : x ≤ v) : between_inv_lel_prop β τ u x v

def LeanPool.DemazureProduct.ASP321a.intervalSub (i₁ i₂ : ℤ × ℤ) : Prop

The interval-subordination relation on inversion boxes.

Equations

• (i₁ ≼ i₂) = (i₂.1 ≤ i₁.1 ∧ i₁.2 ≤ i₂.2)

def LeanPool.DemazureProduct.ASP321a.«term_≼_» : Lean.TrailingParserDescr

Infix notation for interval-subordination of inversion boxes.

Equations

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

theorem LeanPool.DemazureProduct.ASP321a.inv_of_lel_iff {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u v u' v' : ℤ} (uv_inv : (u, v) ∈ invSet β.func) (nested : (u', v') ≼ (u, v)) : (u', v') ∈ invSet β.func ↔ (u', v') ∈ invSet τ.func

theorem LeanPool.DemazureProduct.ASP321a.sr_inv_of_ler_iff {τ : AspPerm} (h_321a : is321a τ.func) {α : AspPerm} (h_R : α ≤R τ) {u v u' v' : ℤ} (uv_inv : (u, v) ∈ τ.sr α '' invSet α.func) (nested : (u, v) ≼ (u', v')) : (u', v') ∈ τ.sr α '' invSet α.func ↔ (u', v') ∈ invSet τ.func

theorem LeanPool.DemazureProduct.ASP321a.set_321a_prop_of_func (avset : tfas) (χ : ℤ) : set_321a_prop (invSet (avset.recon χ))

theorem LeanPool.DemazureProduct.ASP321a.eq_s_of_lel {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u b v : ℤ} (uv_inv : (u, v) ∈ invSet β.func) (u_lt_b : u < b) : β.s.func (β.func v) b = τ.s.func (τ.func v) b

theorem LeanPool.DemazureProduct.ASP321a.eq_s'_of_lel {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u b v : ℤ} (uv_inv : (u, v) ∈ invSet β.func) (b_le_v : b ≤ v) : β⁻¹.s.func b (β.func u) = τ⁻¹.s.func b (τ.func u)

theorem LeanPool.DemazureProduct.ASP321a.uv_eq_of_lel {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) (b : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (τ.u b n_pos, τ.v b m_pos) ∈ invSet β.func → τ.u b n_pos = β.u b n_pos ∧ τ.v b m_pos = β.v b m_pos

theorem LeanPool.DemazureProduct.ASP321a.uv_eq_of_lel' {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) (b : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (β.u b n_pos, β.v b m_pos) ∈ invSet β.func → β.u b n_pos = τ.u b n_pos ∧ β.v b m_pos = τ.v b m_pos

theorem LeanPool.DemazureProduct.ASP321a.lel_ramp {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) (b : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (τ.u b n_pos, τ.v b m_pos) ∈ invSet β.func ↔ (m, n) ∈ β.ramp b

theorem LeanPool.DemazureProduct.ASP321a.lel_lamp {τ : AspPerm} (h_321a : is321a τ.func) {α : AspPerm} (h_R : α ≤R τ) (a : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (τ⁻¹.u a m_pos, τ⁻¹.v a n_pos) ∈ invSet α⁻¹.func ↔ (m, n) ∈ α.lamp a

theorem LeanPool.DemazureProduct.ASP321a.inv_of_lel_iff_ramp {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u b v : ℤ} (u_lt_b : u < b) (b_le_v : b ≤ v) : have m := τ.s.func (τ.func v) b + 1; have n := τ⁻¹.s.func b (τ.func u); (u, v) ∈ invSet β.func ↔ (m, n) ∈ β.ramp b

Two-factor Demazure factorization for 321-avoiding ASP permutations

This section proves the inversion-set criterion for a factorization τ = α ⋆ β in the 321-avoiding setting, first as upper and lower bounds and then as a full characterization.

theorem LeanPool.DemazureProduct.ASP321a.inversion_in_union {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) (a b u v : ℤ) (dprod : α.dprodValGe β a b (τ.s.func a b)) : u < b → b ≤ v → τ.func u ≥ a → τ.func v < a → (u, v) ∈ τ.sr α '' invSet α.func ∪ invSet β.func

theorem LeanPool.DemazureProduct.ASP321a.union_sufficient {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) (a b : ℤ) (h_union : invSet τ.func ⊆ τ.sr α '' invSet α.func ∪ invSet β.func) : α.dprodValGe β a b (τ.s.func a b)

theorem LeanPool.DemazureProduct.ASP321a.excess_of_not_isolated {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) {u v₁ v₂ : ℤ} (v₁_lt_v₂ : v₁ < v₂) (uv₁_inv : (u, v₁) ∈ τ.sr α '' invSet α.func) (uv₂_inv : (u, v₂) ∈ invSet β.func) : have a := τ.func v₁ + 1; have b := v₁ + 1; α.dprodValGe β a b (τ.s.func a b + 1)

theorem LeanPool.DemazureProduct.ASP321a.not_isolated_of_domino {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (a b m m' n n' : ℤ) (m_pos : m ≥ 1) (m'_pos : m' ≥ 1) (n_pos : n ≥ 1) (n'_pos : n' ≥ 1) (msum : m + m' = τ.s.func a b + 2) (nsum : n + n' = τ⁻¹.s.func b a + 1) (hα : (m', n') ∈ α.lamp a) (hβ : (m, n) ∈ β.ramp b) : ∃ (I : ℤ × ℤ) (J : ℤ × ℤ), {I, J} ⊆ τ.sr α '' invSet α.func ∩ invSet β.func ∧ I ≼ J ∧ I ≠ J

theorem LeanPool.DemazureProduct.ASP321a.not_isolated_of_excess {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) {a b : ℤ} (h_s : α.dprodValGe β a b (τ.s.func a b + 1)) : ∃ (I : ℤ × ℤ) (J : ℤ × ℤ), {I, J} ⊆ τ.sr α '' invSet α.func ∩ invSet β.func ∧ I ≼ J ∧ I ≠ J

theorem LeanPool.DemazureProduct.ASP321a.dprod_ge_iff_union {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) : τ ≤ α ⋆ β ↔ invSet τ.func ⊆ τ.sr α '' invSet α.func ∪ invSet β.func

In the 321-avoiding setting, the inequality τ ≤ α ⋆ β is equivalent to the inversion set of τ lying in the union of the shifted inversion set of α and the inversion set of β.

def LeanPool.DemazureProduct.ASP321a.isolated (S : Set (ℤ × ℤ)) : Prop

A set of boxes is isolated if it contains no two distinct comparable elements.

Equations

• LeanPool.DemazureProduct.ASP321a.isolated S = ∀ I ∈ S, ∀ J ∈ S, I ≼ J → I = J

theorem LeanPool.DemazureProduct.ASP321a.dprod_le_iff_isolated {τ : AspPerm} (h_321a : is321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) : α ⋆ β ≤ τ ↔ isolated (τ.sr α '' invSet α.func ∩ invSet β.func)

In the 321-avoiding setting, the inequality α ⋆ β ≤ τ is equivalent to isolatedness of the overlap between the shifted inversion set of α and the inversion set of β.

theorem LeanPool.DemazureProduct.ASP321a.dprod_eq_iff {τ : AspPerm} (h_321a : is321a τ.func) {β α : AspPerm} : τ = α ⋆ β ↔ α.χ + β.χ = τ.χ ∧ invSet τ.func = τ.sr α '' invSet α.func ∪ invSet β.func ∧ isolated (τ.sr α '' invSet α.func ∩ invSet β.func)

Characterize the Demazure factorization τ = α ⋆ β by equality of shifts, a union formula for inversion sets, and isolatedness of the overlap.