Almost-sign-preserving permutations

This file defines almost-sign-preserving permutations, their inversion sets, associated slipfaces, the Bruhat order, and some properties laying the groundwork for the Demazure product $\star$ and residuals $\triangleleft$ and $\triangleright$. These three operations are not yet defined in this file; that is deferred until Submodular.lean, where the bijection between $\mathrm{ASP}$ and the set of submodular slipfaces is established. This corresponds roughly to Section 2, with some bounded-difference material from Section 7, of An extended Demazure product.

def LeanPool.DemazureProduct.invSet (τ : ℤ → ℤ) : Set (ℤ × ℤ)

The inversion set $\operatorname{Inv} \tau = \{(u,v) \in \mathbb{Z}^2 : u < v \text{ and } \tau(u) > \tau(v)\}$. Definition 2.5 (defn:Inv) of An extended Demazure product.

Equations

• LeanPool.DemazureProduct.invSet τ = {(i, j) : ℤ × ℤ | i < j ∧ τ j < τ i}

def LeanPool.DemazureProduct.southeastSet (τ : ℤ → ℤ) (m n : ℤ) : Set ℤ

The southeast quadrant below value m and weakly to the right of index n.

Equations

• LeanPool.DemazureProduct.southeastSet τ m n = {k : ℤ | n ≤ k ∧ τ k < m}

def LeanPool.DemazureProduct.northwestSet (τ : ℤ → ℤ) (m n : ℤ) : Set ℤ

The northwest quadrant above value m and strictly to the left of index n.

Equations

• LeanPool.DemazureProduct.northwestSet τ m n = {k : ℤ | k < n ∧ m ≤ τ k}

@[reducible, inline]

abbrev LeanPool.DemazureProduct.flipFunc (f : ℤ → ℤ) : ℤ → ℤ

Reflect an integer function by the order-reversing involution n ↦ -1 - n.

Equations

• LeanPool.DemazureProduct.flipFunc f k = -1 - f (-1 - k)

theorem LeanPool.DemazureProduct.flip_quadrant (f : ℤ → ℤ) (a b : ℤ) : (fun (x : ℤ) => -1 - x) '' southeastSet f a b = northwestSet (flipFunc f) (-a) (-b)

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

The almost-sign-preserving condition: the set $\{ n \in \mathbb{Z} : n \tau(n) < 0 \}$ is finite.

Equivalently, only finitely many integers change sign under τ.

Equations

• LeanPool.DemazureProduct.isAsp τ = {n : ℤ | n * τ n < 0}.Finite

theorem LeanPool.DemazureProduct.se_finite_of_asp {τ : ℤ → ℤ} (h_inj : Function.Injective τ) (m n : ℤ) : isAsp τ → (southeastSet τ m n).Finite

theorem LeanPool.DemazureProduct.nw_finite_of_asp {τ : ℤ → ℤ} (h_inj : Function.Injective τ) (m n : ℤ) : isAsp τ → (northwestSet τ m n).Finite

theorem LeanPool.DemazureProduct.asp_of_finite_quadrants {τ : ℤ → ℤ} (h_inj : Function.Injective τ) {m n m' n' : ℤ} (fin_se : (southeastSet τ m n).Finite) (fin_nw : (northwestSet τ m' n').Finite) : isAsp τ

structure LeanPool.DemazureProduct.AspPerm : Type

An almost-sign-preserving permutation of ℤ, abbreviated ASP permutation.

This is the group $\mathrm{ASP}$ from An extended Demazure product, packaged in Lean as a function together with proofs of bijectivity and the ASP condition.

• func : ℤ → ℤ

  The underlying bijection of integers.

• bijective : Function.Bijective self.func

  The underlying function is bijective.

• asp : isAsp self.func

  The underlying function is almost-sign-preserving.

@[implicit_reducible]

instance LeanPool.DemazureProduct.instCoeFunAspPermForallInt : CoeFun AspPerm fun (x : AspPerm) => ℤ → ℤ

Equations

• LeanPool.DemazureProduct.instCoeFunAspPermForallInt = { coe := LeanPool.DemazureProduct.AspPerm.func }

theorem LeanPool.DemazureProduct.AspPerm.injective (τ : AspPerm) : Function.Injective τ.func

theorem LeanPool.DemazureProduct.AspPerm.surjective (τ : AspPerm) : Function.Surjective τ.func

theorem LeanPool.DemazureProduct.AspPerm.inv_iff_lt (τ : AspPerm) {i j : ℤ} (i_le_j : i ≤ j) : (i, j) ∈ invSet τ.func ↔ τ.func j < τ.func i

theorem LeanPool.DemazureProduct.AspPerm.inv_iff_le (τ : AspPerm) {i j : ℤ} (i_lt_j : i < j) : (i, j) ∈ invSet τ.func ↔ τ.func j ≤ τ.func i

theorem LeanPool.DemazureProduct.AspPerm.ext {σ τ : AspPerm} : σ = τ ↔ σ.func = τ.func

def LeanPool.DemazureProduct.AspPerm.mul (σ τ : AspPerm) : AspPerm

Composition of ASP permutations.

Equations

• σ.mul τ = { func := σ.func ∘ τ.func, bijective := ⋯, asp := ⋯ }

noncomputable def LeanPool.DemazureProduct.AspPerm.inv (τ : AspPerm) : AspPerm

The inverse ASP permutation.

Equations

• τ.inv = { func := Function.invFun τ.func, bijective := ⋯, asp := ⋯ }

def LeanPool.DemazureProduct.AspPerm.id : AspPerm

The identity ASP permutation.

Equations

• LeanPool.DemazureProduct.AspPerm.id = { func := id, bijective := LeanPool.DemazureProduct.AspPerm.id._proof_1, asp := LeanPool.DemazureProduct.AspPerm.id._proof_2 }

@[implicit_reducible]

noncomputable instance LeanPool.DemazureProduct.AspPerm.instGroup : Group AspPerm

Equations

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

@[simp]

theorem LeanPool.DemazureProduct.AspPerm.mul_apply (σ τ : AspPerm) (n : ℤ) : (σ * τ).func n = σ.func (τ.func n)

Ordinary multiplication of ASP permutations is function composition.

@[simp]

theorem LeanPool.DemazureProduct.AspPerm.inv_mul_cancel_eval (τ : AspPerm) (n : ℤ) : τ⁻¹.func (τ.func n) = n

@[simp]

theorem LeanPool.DemazureProduct.AspPerm.mul_inv_cancel_eval (τ : AspPerm) (n : ℤ) : τ.func (τ⁻¹.func n) = n

theorem LeanPool.DemazureProduct.AspPerm.se_finite (τ : AspPerm) (a b : ℤ) : (southeastSet τ.func a b).Finite

theorem LeanPool.DemazureProduct.AspPerm.nw_finite (τ : AspPerm) (a b : ℤ) : (northwestSet τ.func a b).Finite

noncomputable def LeanPool.DemazureProduct.AspPerm.seFinset (τ : AspPerm) (a b : ℤ) : Finset ℤ

The finite southeast quadrant for an ASP permutation.

Equations

• τ.seFinset a b = ⋯.toFinset

@[simp]

theorem LeanPool.DemazureProduct.AspPerm.mem_se (τ : AspPerm) (a b n : ℤ) : n ∈ τ.seFinset a b ↔ n ≥ b ∧ τ.func n < a

noncomputable def LeanPool.DemazureProduct.AspPerm.nwFinset (τ : AspPerm) (a b : ℤ) : Finset ℤ

The finite northwest quadrant for an ASP permutation.

Equations

• τ.nwFinset a b = ⋯.toFinset

@[simp]

theorem LeanPool.DemazureProduct.AspPerm.mem_nw (τ : AspPerm) (a b n : ℤ) : n ∈ τ.nwFinset a b ↔ n < b ∧ τ.func n ≥ a

theorem LeanPool.DemazureProduct.AspPerm.inv_set_inverse (τ : AspPerm) (u v : ℤ) : (u, v) ∈ invSet τ.func ↔ (τ.func v, τ.func u) ∈ invSet τ⁻¹.func

def LeanPool.DemazureProduct.AspPerm.revMap (τ : AspPerm) : ℤ × ℤ → ℤ × ℤ

Reverse an inversion box through an ASP permutation.

Equations

• τ.revMap (i, j) = (τ.func j, τ.func i)

noncomputable def LeanPool.DemazureProduct.AspPerm.χ (τ : AspPerm) : ℤ

The shift $\chi_\tau = s_\tau(0,0) - s_{\tau^{-1}}(0,0)$.

An extended Demazure product writes this as $\chi_\tau$; Lean writes it as τ.χ.

Equations

• τ.χ = LeanPool.DemazureProduct.AspPerm.s_raw✝ τ 0 0 - LeanPool.DemazureProduct.AspPerm.s'_raw✝ τ 0 0

noncomputable def LeanPool.DemazureProduct.AspPerm.s (τ : AspPerm) : SlipFace

The slipface attached to τ. An extended Demazure product writes its values as $s_\tau(a,b)$; in Lean the corresponding value is τ.s_raw a b, and τ.s packages the same data as a SlipFace.

Equations

• τ.s = { func := LeanPool.DemazureProduct.AspPerm.s_raw✝ τ, χ := τ.χ, a_step := ⋯, b_step := ⋯, nonneg := ⋯, ge_diff := ⋯, small_a := ⋯, large_a := ⋯, small_b := ⋯, large_b := ⋯ }

Basic properties of the slipface of a permutation

theorem LeanPool.DemazureProduct.AspPerm.s_eq_ncard (τ : AspPerm) (a b : ℤ) : τ.s.func a b = ↑(southeastSet τ.func a b).ncard

theorem LeanPool.DemazureProduct.AspPerm.s'_eq_ncard (τ : AspPerm) (b a : ℤ) : τ⁻¹.s.func b a = ↑(northwestSet τ.func a b).ncard

theorem LeanPool.DemazureProduct.AspPerm.s_eq_se_card (τ : AspPerm) (a b : ℤ) : τ.s.func a b = ↑(τ.seFinset a b).card

theorem LeanPool.DemazureProduct.AspPerm.s_nonneg (τ : AspPerm) (a b : ℤ) : τ.s.func a b ≥ 0

theorem LeanPool.DemazureProduct.AspPerm.s_ge (τ : AspPerm) (a b : ℤ) : τ.s.func a b ≥ a - b + τ.χ

theorem LeanPool.DemazureProduct.AspPerm.a_step (τ : AspPerm) (a b : ℤ) : τ.s.func (a + 1) b = τ.s.func a b + if τ⁻¹.func a ≥ b then 1 else 0

theorem LeanPool.DemazureProduct.AspPerm.b_step (τ : AspPerm) (a b : ℤ) : τ.s.func a (b + 1) = τ.s.func a b - if τ.func b < a then 1 else 0

theorem LeanPool.DemazureProduct.AspPerm.s_noninc (τ : AspPerm) (a : ℤ) {b b' : ℤ} (b_le_b' : b ≤ b') : τ.s.func a b ≥ τ.s.func a b' ∧ (τ.s.func a b = τ.s.func a b' ↔ ∀ (x : ℤ), b ≤ x → x < b' → τ.func x ≥ a)

theorem LeanPool.DemazureProduct.AspPerm.s_nondec (τ : AspPerm) {a a' : ℤ} (a_le_a' : a ≤ a') (b : ℤ) : τ.s.func a b ≤ τ.s.func a' b ∧ (τ.s.func a b = τ.s.func a' b ↔ ∀ (x : ℤ), a ≤ τ.func x → τ.func x < a' → x < b)

theorem LeanPool.DemazureProduct.AspPerm.duality (τ : AspPerm) (a b : ℤ) : τ.s.func a b - τ⁻¹.s.func b a = τ.χ + a - b

theorem LeanPool.DemazureProduct.AspPerm.s_eq (τ : AspPerm) (a b : ℤ) : τ.s.func a b = τ⁻¹.s.func b a + τ.χ + a - b

theorem LeanPool.DemazureProduct.AspPerm.s'_eq (τ : AspPerm) (a b : ℤ) : τ⁻¹.s.func a b = τ.s.func b a - τ.χ + a - b

theorem LeanPool.DemazureProduct.AspPerm.tend_zero_a (τ : AspPerm) (b : ℤ) : ∃ (a : ℤ), τ.s.func a b = 0

theorem LeanPool.DemazureProduct.AspPerm.tend_zero_b (τ : AspPerm) (a : ℤ) : ∃ (b : ℤ), τ.s.func a b = 0

theorem LeanPool.DemazureProduct.AspPerm.a_move_up (τ : AspPerm) (a a' b : ℤ) (a_le_a' : a ≤ a') : τ.s.func a' b = τ.s.func a b + ↑{x ∈ Finset.Ico a a' | τ⁻¹.func x ≥ b}.card

theorem LeanPool.DemazureProduct.AspPerm.b_move_up (τ : AspPerm) (a b b' : ℤ) (b_le_b' : b ≤ b') : τ.s.func a b' = τ.s.func a b - ↑{x ∈ Finset.Ico b b' | τ.func x < a}.card

theorem LeanPool.DemazureProduct.AspPerm.chi_eq_card (τ : AspPerm) : τ.χ = ↑(τ.seFinset 0 0).card - ↑(τ.nwFinset 0 0).card

The shift as a difference of southeast and northwest cardinalities.

@[simp]

theorem LeanPool.DemazureProduct.AspPerm.id_chi : id.χ = 0

theorem LeanPool.DemazureProduct.AspPerm.chi_dual (τ : AspPerm) : τ⁻¹.χ = -τ.χ

theorem LeanPool.DemazureProduct.AspPerm.chi_dual' (τ : AspPerm) : τ.χ = -τ⁻¹.χ

theorem LeanPool.DemazureProduct.AspPerm.chi_mul (α β : AspPerm) : (α * β).χ = α.χ + β.χ

Shift is additive under ordinary multiplication: $\chi_{\alpha\beta} = \chi_\alpha + \chi_\beta$. Equation (16) (eq:chiHom) of An extended Demazure product.

theorem LeanPool.DemazureProduct.AspPerm.b_step_one_iff (τ : AspPerm) (a b : ℤ) : τ.s.func a (b + 1) = τ.s.func a b - 1 ↔ τ.func b < a

theorem LeanPool.DemazureProduct.AspPerm.b_step_lt_iff (τ : AspPerm) (a b : ℤ) : τ.s.func a (b + 1) < τ.s.func a b ↔ τ.func b < a

theorem LeanPool.DemazureProduct.AspPerm.b_step_eq_iff (τ : AspPerm) (a b : ℤ) : τ.s.func a (b + 1) = τ.s.func a b ↔ a ≤ τ.func b

theorem LeanPool.DemazureProduct.AspPerm.b_step_ge_iff (τ : AspPerm) (a b : ℤ) : τ.s.func a (b + 1) ≥ τ.s.func a b ↔ a ≤ τ.func b

theorem LeanPool.DemazureProduct.AspPerm.a_step_one_iff (τ : AspPerm) (a b : ℤ) : τ.s.func (a + 1) b = τ.s.func a b + 1 ↔ τ⁻¹.func a ≥ b

theorem LeanPool.DemazureProduct.AspPerm.a_step_gt_iff (τ : AspPerm) (a b : ℤ) : τ.s.func a b < τ.s.func (a + 1) b ↔ b ≤ τ⁻¹.func a

theorem LeanPool.DemazureProduct.AspPerm.a_step_le_iff (τ : AspPerm) (a b : ℤ) : τ.s.func (a + 1) b ≤ τ.s.func a b ↔ τ⁻¹.func a < b

theorem LeanPool.DemazureProduct.AspPerm.a_step_one_iff' (τ : AspPerm) (u b : ℤ) : τ.s.func (τ.func u + 1) b = τ.s.func (τ.func u) b + 1 ↔ u ≥ b

theorem LeanPool.DemazureProduct.AspPerm.a_step_eq_iff (τ : AspPerm) (a b : ℤ) : τ.s.func (a + 1) b = τ.s.func a b ↔ τ⁻¹.func a < b

theorem LeanPool.DemazureProduct.AspPerm.a_step_eq_iff' (τ : AspPerm) (u b : ℤ) : τ.s.func (τ.func u + 1) b = τ.s.func (τ.func u) b ↔ u < b

def LeanPool.DemazureProduct.AspPerm.inset (τ : AspPerm) (v : ℤ) : Set ℤ

The set of inversion sources ending at v.

Equations

• τ.inset v = {u : ℤ | (u, v) ∈ LeanPool.DemazureProduct.invSet τ.func}

theorem LeanPool.DemazureProduct.AspPerm.inset_eq_nw (τ : AspPerm) (v : ℤ) : τ.inset v = northwestSet τ.func (τ.func v) v

theorem LeanPool.DemazureProduct.AspPerm.invset_iff_inset (τ : AspPerm) (u v : ℤ) : (u, v) ∈ invSet τ.func ↔ u ∈ τ.inset v

theorem LeanPool.DemazureProduct.AspPerm.inset_finite (τ : AspPerm) (v : ℤ) : (τ.inset v).Finite

def LeanPool.DemazureProduct.AspPerm.outset (τ : AspPerm) (u : ℤ) : Set ℤ

The set of inversion targets starting at u.

Equations

• τ.outset u = {v : ℤ | (u, v) ∈ LeanPool.DemazureProduct.invSet τ.func}

theorem LeanPool.DemazureProduct.AspPerm.outset_eq_se (τ : AspPerm) (u : ℤ) : τ.outset u = southeastSet τ.func (τ.func u) u

theorem LeanPool.DemazureProduct.AspPerm.invset_iff_outset (τ : AspPerm) (u v : ℤ) : (u, v) ∈ invSet τ.func ↔ v ∈ τ.outset u

theorem LeanPool.DemazureProduct.AspPerm.outset_finite (τ : AspPerm) (u : ℤ) : (τ.outset u).Finite

theorem LeanPool.DemazureProduct.AspPerm.reconstruction (τ : AspPerm) (n : ℤ) : τ.func n = n - τ.χ + ↑(τ.outset n).ncard - ↑(τ.inset n).ncard

Reconstruct τ n from its shift and inversion set: $\tau(n) = n - \chi_\tau$ $+ \#\{v \in \mathbb{Z} : (n,v) \in \operatorname{Inv} \tau\}$ $- \#\{u \in \mathbb{Z} : (u,n) \in \operatorname{Inv} \tau\}$.

Proposition 2.11 (prop:reconstruction) of An extended Demazure product, part 1/2.

theorem LeanPool.DemazureProduct.AspPerm.eq_of_inv_set_eq_of_chi_eq (σ τ : AspPerm) (h_inv : invSet σ.func = invSet τ.func) (h_χ : σ.χ = τ.χ) : σ = τ

Two ASP permutations are equal if they have the same inversion set and the same shift. Proposition 2.11 (prop:reconstruction) of An extended Demazure product, consequence, part 2/2.

theorem LeanPool.DemazureProduct.AspPerm.eq_id_of_inv_set_eq_empty_of_chi_eq_zero (τ : AspPerm) (h_inv : invSet τ.func = ∅) (h_χ : τ.χ = 0) : τ = id

An ASP permutation with empty inversion set and zero shift is the identity.

@[simp]

theorem LeanPool.DemazureProduct.AspPerm.inv_set_id : invSet id.func = ∅

@[simp]

theorem LeanPool.DemazureProduct.AspPerm.s_chi_eq (τ : AspPerm) : τ.s.χ = τ.χ

theorem LeanPool.DemazureProduct.AspPerm.s_dual (τ : AspPerm) : τ.s.dual = τ⁻¹.s

theorem LeanPool.DemazureProduct.AspPerm.s_dual_eq_nw_card (τ : AspPerm) (b a : ℤ) : τ⁻¹.s.func b a = ↑(τ.nwFinset a b).card

The northwest count (τ⁻¹).s b a (the slipface dual value) equals the cardinality of the northwest set. The slipface replacement for s'_eq_nw_card.

theorem LeanPool.DemazureProduct.AspPerm.bend_set_sf (β : AspPerm) (b : ℤ) : β.s.bendSet b = {l : ℤ | β⁻¹.func (l - 1) < b ∧ b ≤ β⁻¹.func l}

The bend set is a finite set on which the minimum defining the Demazure product is always obtained. It is characterized in Lemma 3.13 (lem:setL) of An extended Demazure product, part 5/5.

theorem LeanPool.DemazureProduct.AspPerm.Delta_eq (τ : AspPerm) (a b : ℤ) : τ.s.Δ a b = if τ.func b = a then 1 else 0

Formula (14) (eq:Deltasa) of An extended Demazure product, characterizing the values of a permutation via the second iterated difference of its slipface.

theorem LeanPool.DemazureProduct.AspPerm.Γ_eq (τ : AspPerm) : τ.s.Γ = {(a, b) : ℤ × ℤ | τ.func b = a}

theorem LeanPool.DemazureProduct.AspPerm.submodular (τ : AspPerm) : τ.s.submodular

The slipface of an ASP permutation is submodular. Proposition 4.3 (prop:imageASP) of An extended Demazure product, one direction.

Ramps, lamps, and wing parameters

This section defines the ramp and lamp regions associated to an ASP permutation. These are Young diagrams associated to particular values of a or b, useful in characterizing Demazure factorizations of 321-avoiding permutations.

This material is not present in An extended Demazure product.

def LeanPool.DemazureProduct.AspPerm.ramp (τ : AspPerm) (b : ℤ) : Set (ℤ × ℤ)

The b-ramp of an ASP permutation: the region, shaped like a Young diagram, of pairs (m,n) such that $s_\tau(\ell,b) \ge m$ and $s^∨_\tau(b,\ell) \ge n$ for some $\ell$.

Equations

• τ.ramp b = {(m, n) : ℤ × ℤ | ∃ (l : ℤ), τ.s.func l b ≥ m ∧ τ⁻¹.s.func b l ≥ n}

def LeanPool.DemazureProduct.AspPerm.lamp (τ : AspPerm) (a : ℤ) : Set (ℤ × ℤ)

The a-lamp of an ASP permutation, defined as the dual of a ramp.

Equations

• τ.lamp a = {(m, n) : ℤ × ℤ | ∃ (l : ℤ), τ.s.func a l ≥ m ∧ τ⁻¹.s.func l a ≥ n}

theorem LeanPool.DemazureProduct.AspPerm.ramp_closed (τ : AspPerm) (b : ℤ) {m₁ n₁ m₂ n₂ : ℤ} (hm : m₁ ≤ m₂) (hn : n₁ ≤ n₂) : (m₂, n₂) ∈ τ.ramp b → (m₁, n₁) ∈ τ.ramp b

theorem LeanPool.DemazureProduct.AspPerm.ramp_lamp_dual (τ : AspPerm) (b m n : ℤ) : (m, n) ∈ τ.ramp b ↔ (n, m) ∈ τ⁻¹.lamp b

theorem LeanPool.DemazureProduct.AspPerm.mem_ramp_iff_s_ge (τ : AspPerm) (b m n : ℤ) : (m, n) ∈ τ.ramp b ↔ τ.s.func (b + m - n - τ.χ) b ≥ m

theorem LeanPool.DemazureProduct.AspPerm.mem_lamp_iff_s_ge (τ : AspPerm) (a m n : ℤ) : (m, n) ∈ τ.lamp a ↔ τ⁻¹.s.func (a - m + n + τ.χ) a ≥ n

noncomputable def LeanPool.DemazureProduct.AspPerm.v (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) : ℤ

The rightmost index whose image is the last value with s below m in row b.

Equations

• τ.v b m_pos = τ⁻¹.func (Classical.choose ⋯)

theorem LeanPool.DemazureProduct.AspPerm.v_crit (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) (v : ℤ) : v = τ.v b m_pos ↔ τ.s.func (τ.func v) b = m - 1 ∧ b ≤ v

theorem LeanPool.DemazureProduct.AspPerm.s_τv_b (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) : τ.s.func (τ.func (τ.v b m_pos)) b = m - 1

theorem LeanPool.DemazureProduct.AspPerm.v_ge (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) : b ≤ τ.v b m_pos

theorem LeanPool.DemazureProduct.AspPerm.τv_lt (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) {a : ℤ} (s_ge_m : m ≤ τ.s.func a b) : τ.func (τ.v b m_pos) < a

noncomputable def LeanPool.DemazureProduct.AspPerm.u (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : ℤ

The rightmost index witnessing the dual lower bound n in row b.

Equations

• τ.u b n_pos = τ⁻¹.func (Classical.choose ⋯)

theorem LeanPool.DemazureProduct.AspPerm.u_crit (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) (u : ℤ) : u = τ.u b n_pos ↔ τ⁻¹.s.func b (τ.func u) = n ∧ u < b

theorem LeanPool.DemazureProduct.AspPerm.s'_b_τu (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : τ⁻¹.s.func b (τ.func (τ.u b n_pos)) = n

theorem LeanPool.DemazureProduct.AspPerm.s'_pos_of_lt (τ : AspPerm) {u b : ℤ} (u_lt_b : u < b) : τ⁻¹.s.func b (τ.func u) ≥ 1

theorem LeanPool.DemazureProduct.AspPerm.u_lt (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : τ.u b n_pos < b

theorem LeanPool.DemazureProduct.AspPerm.τu_ge (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) {a : ℤ} (s_ge_n : n ≤ τ⁻¹.s.func b a) : τ.func (τ.u b n_pos) ≥ a

theorem LeanPool.DemazureProduct.AspPerm.inv_ramp_correspondence (τ : AspPerm) (b : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (m, n) ∈ τ.ramp b ↔ (τ.u b n_pos, τ.v b m_pos) ∈ invSet τ.func

A box lies in the ramp exactly when a specific inversion belongs to invSet τ, given by the functions u and v above.

Reduced products and weak orders

This section introduces some infrastructure about inversion sets.

def LeanPool.DemazureProduct.AspPerm.ReducedProduct (α β : AspPerm) : Prop

A product $\alpha \beta$ is reduced if $\operatorname{Inv}(\alpha) \cap \operatorname{Inv}(\beta^{-1})$ is empty.

Definition 2.7 (defn:reducedProduct) of An extended Demazure product.

Equations

• α.ReducedProduct β = Disjoint (LeanPool.DemazureProduct.invSet α.func) (LeanPool.DemazureProduct.invSet β⁻¹.func)

def LeanPool.DemazureProduct.AspPerm.leWeakL (σ τ : AspPerm) : Prop

The left weak order: σ ≤L τ if and only if $\operatorname{Inv} \sigma \subseteq \operatorname{Inv} \tau$. Definition 2.6 (defn:weakOrders), part 1/2, of An extended Demazure product.

Equations

• (σ ≤L τ) = (LeanPool.DemazureProduct.invSet σ.func ⊆ LeanPool.DemazureProduct.invSet τ.func)

def LeanPool.DemazureProduct.AspPerm.«term_≤L_» : Lean.TrailingParserDescr

Infix notation for the left weak order on ASP permutations.

Equations

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

def LeanPool.DemazureProduct.AspPerm.leWeakR (σ τ : AspPerm) : Prop

The right weak order: σ ≤R τ if and only if $\operatorname{Inv}(\sigma^{-1}) \subseteq \operatorname{Inv}(\tau^{-1})$. Definition 2.6 (defn:weakOrders), part 2/2, of An extended Demazure product.

Equations

• (σ ≤R τ) = (LeanPool.DemazureProduct.invSet σ⁻¹.func ⊆ LeanPool.DemazureProduct.invSet τ⁻¹.func)

def LeanPool.DemazureProduct.AspPerm.«term_≤R_» : Lean.TrailingParserDescr

Infix notation for the right weak order on ASP permutations.

Equations

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

theorem LeanPool.DemazureProduct.AspPerm.le_weak_L_of_R {σ τ : AspPerm} (h_R : σ ≤R τ) : σ⁻¹ ≤L τ⁻¹

theorem LeanPool.DemazureProduct.AspPerm.le_weak_R_of_L {σ τ : AspPerm} (h_L : σ ≤L τ) : σ⁻¹ ≤R τ⁻¹

theorem LeanPool.DemazureProduct.AspPerm.reduced_iff_leR (α β : AspPerm) : α.ReducedProduct β ↔ α ≤R α * β

A product α β is reduced exactly when α is below α β in right weak order. Lemma 2.8 (lem:reducedWeakEquivs) of An extended Demazure product, part 1/2.

theorem LeanPool.DemazureProduct.AspPerm.reduced_iff_leL (α β : AspPerm) : α.ReducedProduct β ↔ β ≤L α * β

A product α β is reduced exactly when β is below α β in left weak order. Lemma 2.8 (lem:reducedWeakEquivs) of An extended Demazure product, part 2/2.

theorem LeanPool.DemazureProduct.AspPerm.reducedProduct_inv_swap (α β : AspPerm) : α.ReducedProduct β ↔ β⁻¹.ReducedProduct α⁻¹

Inversion reverses the factors in a reduced product.

noncomputable def LeanPool.DemazureProduct.AspPerm.sr (τ α : AspPerm) : ℤ × ℤ → ℤ × ℤ

Slide right inversions from α to boxes indexed by τ.

Equations

• τ.sr α x = (τ⁻¹.func (α.func x.1), τ⁻¹.func (α.func x.2))

theorem LeanPool.DemazureProduct.AspPerm.sr_crit (τ α : AspPerm) (u v : ℤ) : (u, v) ∈ τ.sr α '' invSet α.func ↔ (τ.func v, τ.func u) ∈ invSet α⁻¹.func

theorem LeanPool.DemazureProduct.AspPerm.sr_subset (τ α : AspPerm) (h_R : α ≤R τ) : τ.sr α '' invSet α.func ⊆ invSet τ.func

def LeanPool.DemazureProduct.AspPerm.dprodValGe (α β : AspPerm) (a b n : ℤ) : Prop

The min-plus Demazure-product value is at least n at (a, b).

Equations

• α.dprodValGe β a b n = ∀ (l : ℤ), α.s.func a l + β.s.func l b ≥ n

def LeanPool.DemazureProduct.AspPerm.leDprod (τ α β : AspPerm) : Prop

Pointwise lower-bound predicate for a candidate Demazure product.

Equations

• τ.leDprod α β = ∀ (a b : ℤ), α.dprodValGe β a b (τ.s.func a b)

def LeanPool.DemazureProduct.AspPerm.dprodValLe (α β : AspPerm) (a b n : ℤ) : Prop

The min-plus Demazure-product value is at most n at (a, b).

Equations

• α.dprodValLe β a b n = ∃ (l : ℤ), α.s.func a l + β.s.func l b ≤ n

def LeanPool.DemazureProduct.AspPerm.geDprod (τ α β : AspPerm) : Prop

Pointwise upper-bound predicate for a candidate Demazure product.

Equations

• τ.geDprod α β = ∀ (a b : ℤ), α.dprodValLe β a b (τ.s.func a b)

def LeanPool.DemazureProduct.AspPerm.eqDprod (τ α β : AspPerm) : Prop

Pointwise equality predicate for a candidate Demazure product.

Equations

• τ.eqDprod α β = (τ.leDprod α β ∧ τ.geDprod α β)

theorem LeanPool.DemazureProduct.AspPerm.chi_ge_of_dprod_ge {α β τ : AspPerm} (h_ge : τ.leDprod α β) : α.χ + β.χ ≥ τ.χ

theorem LeanPool.DemazureProduct.AspPerm.chi_le_of_dprod_le {α β τ : AspPerm} (h_le : τ.geDprod α β) : α.χ + β.χ ≤ τ.χ

theorem LeanPool.DemazureProduct.AspPerm.chi_eq_of_drop_eq {τ α β : AspPerm} (h_eq : τ.eqDprod α β) : α.χ + β.χ = τ.χ

theorem LeanPool.DemazureProduct.AspPerm.dprod_inv_eq_inv_dprod (τ α β : AspPerm) (h_eq : τ.eqDprod α β) : τ⁻¹.eqDprod β⁻¹ α⁻¹

theorem LeanPool.DemazureProduct.AspPerm.ramp_dprod_legos (α β : AspPerm) (a b M N : ℤ) (habMN : a - b + α.χ + β.χ = M - N) : α.dprodValGe β a b M ↔ ∀ m ∈ Set.Icc 1 M, ∀ n ∈ Set.Icc 1 N, (m, n) ∈ β.ramp b ∨ (M + 1 - m, N + 1 - n) ∈ α.lamp a

A characterization of Demazure products in terms of the Young diagrams called "ramps" and "lamps" above. This is the key input in classifying the Demazure factorizations of 321-avoiding permutations.

This theorem is not present in An extended Demazure product.

The essential set of a permutation

This section formalizes results from Section 7.2 of An extended Demazure product about the essential set of a permutation and permutations of bounded difference.

def LeanPool.DemazureProduct.AspPerm.ess (τ : AspPerm) : Set (ℤ × ℤ)

The essential set of an ASP permutation.

Equations

• τ.ess = {(a, b) : ℤ × ℤ | τ.func b < a ∧ a ≤ τ.func (b - 1) ∧ τ⁻¹.func a < b ∧ b ≤ τ⁻¹.func (a - 1)}

theorem LeanPool.DemazureProduct.AspPerm.ess_asp_eq_ess_sf (τ : AspPerm) : τ.ess = τ.s.ess

def LeanPool.DemazureProduct.AspPerm.isBdiff (τ : AspPerm) : Prop

The bounded-difference condition for an ASP permutation.

Equations

• τ.isBdiff = ∃ (M : ℤ), ∀ (n : ℤ), |n - τ.func n| ≤ M

def LeanPool.DemazureProduct.AspPerm.M (τ : AspPerm) : Set ℤ

The first auxiliary unboundedness set used for bounded-difference criteria.

Equations

• τ.M = {m : ℤ | ∃ (a : ℤ) (b : ℤ), τ.s.func a b > 0 ∧ m ≤ τ⁻¹.s.func b a}

def LeanPool.DemazureProduct.AspPerm.M' (τ : AspPerm) : Set ℤ

The second auxiliary unboundedness set used for bounded-difference criteria.

Equations

• τ.M' = {m : ℤ | ∃ (n : ℤ), m ≤ n - τ.func n - τ.χ}

def LeanPool.DemazureProduct.AspPerm.M'' (τ : AspPerm) : Set ℤ

The third auxiliary unboundedness set used for bounded-difference criteria.

Equations

• τ.M'' = {m : ℤ | ∃ (a : ℤ) (b : ℤ), τ.s.func a b > 0 ∧ m ≤ b - a - τ.χ + 1}

theorem LeanPool.DemazureProduct.AspPerm.M'_eq_M (τ : AspPerm) : τ.M' = τ.M

A set-theoretic reformulation of Lemma 7.8 (lem:malpha) of An extended Demazure product, part 1/2.*

theorem LeanPool.DemazureProduct.AspPerm.M''_eq_M (τ : AspPerm) : τ.M'' = τ.M

A set-theoretic reformulation of Lemma 7.8 (lem:malpha) of An extended Demazure product, part 2/2.*

theorem LeanPool.DemazureProduct.AspPerm.bdiff_iff_width (τ : AspPerm) : τ.isBdiff ↔ ∃ (N : ℤ), LeanPool.DemazureProduct.AspPerm.width_bound✝ τ N

A permutation $\tau$ has bounded difference if and only if $s_\tau(a,b)$ agrees with $\max\{0, a-b+\chi(\tau)\}$ for all $|a-b| \gg 0$. Proposition 7.7 (prop:cliffordPerms) of An extended Demazure product, part 1/2.*

theorem LeanPool.DemazureProduct.AspPerm.bdiff_iff_clifford (τ : AspPerm) : τ.isBdiff ↔ τ.s.isClifford

A permutation $\tau$ has bounded difference if and only if $s_\tau$ is a Clifford slipface. Proposition 7.7 (prop:cliffordPerms) of An extended Demazure product, part 2/2.*