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 inv_set (τ : ℤ → ℤ) : 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

• inv_set τ = {(i, j) : ℤ × ℤ | i < j ∧ τ j < τ i}

def southeast_set (τ : ℤ → ℤ) (m n : ℤ) : Set ℤ

Equations

• southeast_set τ m n = {k : ℤ | n ≤ k ∧ τ k < m}

def northwest_set (τ : ℤ → ℤ) (m n : ℤ) : Set ℤ

Equations

• northwest_set τ m n = {k : ℤ | k < n ∧ m ≤ τ k}

@[reducible, inline]

abbrev flip_func (f : ℤ → ℤ) : ℤ → ℤ

Equations

• flip_func f k = -1 - f (-1 - k)

theorem flip_quadrant (f : ℤ → ℤ) (a b : ℤ) : (fun (x : ℤ) => -1 - x) '' southeast_set f a b = northwest_set (flip_func f) (-a) (-b)

def is_asp (τ : ℤ → ℤ) : 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

• is_asp τ = {n : ℤ | n * τ n < 0}.Finite

theorem se_finite_of_asp {τ : ℤ → ℤ} (h_inj : Function.Injective τ) (m n : ℤ) : is_asp τ → (southeast_set τ m n).Finite

theorem nw_finite_of_asp {τ : ℤ → ℤ} (h_inj : Function.Injective τ) (m n : ℤ) : is_asp τ → (northwest_set τ m n).Finite

theorem asp_of_finite_quadrants {τ : ℤ → ℤ} (h_inj : Function.Injective τ) {m n m' n' : ℤ} (fin_se : (southeast_set τ m n).Finite) (fin_nw : (northwest_set τ m' n').Finite) : is_asp τ

structure 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 : ℤ → ℤ
• bijective : Function.Bijective self.func
• asp : is_asp self.func

@[implicit_reducible]

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

Equations

• instCoeFunAspPermForallInt = { coe := AspPerm.func }

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

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

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

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

@[simp]

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

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

Equations

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

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

Equations

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

def AspPerm.id : AspPerm

Equations

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

@[implicit_reducible]

noncomputable instance AspPerm.instGroup : Group AspPerm

Equations

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

@[simp]

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

Ordinary multiplication of ASP permutations is function composition.

@[simp]

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

@[simp]

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

theorem AspPerm.se_finite (τ : AspPerm) (a b : ℤ) : (southeast_set τ.func a b).Finite

theorem AspPerm.nw_finite (τ : AspPerm) (a b : ℤ) : (northwest_set τ.func a b).Finite

noncomputable def AspPerm.se_finset (τ : AspPerm) (a b : ℤ) : Finset ℤ

Equations

• τ.se_finset a b = ⋯.toFinset

@[simp]

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

noncomputable def AspPerm.nw_finset (τ : AspPerm) (a b : ℤ) : Finset ℤ

Equations

• τ.nw_finset a b = ⋯.toFinset

@[simp]

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

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

def AspPerm.rev_map (τ : AspPerm) : ℤ × ℤ → ℤ × ℤ

Equations

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

noncomputable def 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

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

noncomputable def 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 := 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 AspPerm.s_eq_ncard (τ : AspPerm) (a b : ℤ) : τ.s.func a b = ↑(southeast_set τ.func a b).ncard

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

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

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

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

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

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

theorem 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 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 AspPerm.duality (τ : AspPerm) (a b : ℤ) : τ.s.func a b - τ⁻¹.s.func b a = τ.χ + a - b

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

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

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

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

theorem 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 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 AspPerm.chi_eq_card (τ : AspPerm) : τ.χ = ↑(τ.se_finset 0 0).card - ↑(τ.nw_finset 0 0).card

The shift as a difference of southeast and northwest cardinalities.

@[simp]

theorem AspPerm.id_chi : id.χ = 0

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

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

theorem 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 AspPerm.b_step_one_iff (τ : AspPerm) (a b : ℤ) : τ.s.func a (b + 1) = τ.s.func a b - 1 ↔ τ.func b < a

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

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

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

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

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

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

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

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

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

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

Equations

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

theorem AspPerm.inset_eq_nw (τ : AspPerm) (v : ℤ) : τ.inset v = northwest_set τ.func (τ.func v) v

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

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

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

Equations

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

theorem AspPerm.outset_eq_se (τ : AspPerm) (u : ℤ) : τ.outset u = southeast_set τ.func (τ.func u) u

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

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

theorem 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 AspPerm.eq_of_inv_set_eq_of_chi_eq (σ τ : AspPerm) (h_inv : inv_set σ.func = inv_set τ.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 AspPerm.eq_id_of_inv_set_eq_empty_of_chi_eq_zero (τ : AspPerm) (h_inv : inv_set τ.func = ∅) (h_χ : τ.χ = 0) : τ = id

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

@[simp]

theorem AspPerm.inv_set_id : inv_set id.func = ∅

@[simp]

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

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

theorem AspPerm.s_dual_eq_nw_card (τ : AspPerm) (b a : ℤ) : τ⁻¹.s.func b a = ↑(τ.nw_finset 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 AspPerm.bend_set_sf (β : AspPerm) (b : ℤ) : β.s.bend_set 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 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 AspPerm.Γ_eq (τ : AspPerm) : τ.s.Γ = {(a, b) : ℤ × ℤ | τ.func b = a}

theorem 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 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 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}

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

Equations

• ⋯ = ⋯

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

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

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

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

Equations

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

theorem 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 AspPerm.s_τv_b (τ : AspPerm) (b : ℤ) {m : ℤ} (m_pos : m > 0) : τ.s.func (τ.func (τ.v b m_pos)) b = m - 1

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

theorem 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 AspPerm.u (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : ℤ

Equations

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

theorem 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 AspPerm.s'_b_τu (τ : AspPerm) (b : ℤ) {n : ℤ} (n_pos : n > 0) : τ⁻¹.s.func b (τ.func (τ.u b n_pos)) = n

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

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

theorem 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 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) ∈ inv_set τ.func

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

Reduced products and weak orders

This section introduces some infrastructure about inversion sets.

def 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 (inv_set α.func) (inv_set β⁻¹.func)

def AspPerm.le_weak_L (σ τ : 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 τ) = (inv_set σ.func ⊆ inv_set τ.func)

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

Equations

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

def AspPerm.le_weak_R (σ τ : 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 τ) = (inv_set σ⁻¹.func ⊆ inv_set τ⁻¹.func)

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

Equations

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

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

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

theorem 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 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 AspPerm.reducedProduct_inv_swap (α β : AspPerm) : α.ReducedProduct β ↔ β⁻¹.ReducedProduct α⁻¹

Inversion reverses the factors in a reduced product.

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

Equations

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

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

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

def AspPerm.dprod_val_ge (α β : AspPerm) (a b n : ℤ) : Prop

Equations

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

def AspPerm.le_dprod (τ α β : AspPerm) : Prop

Equations

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

def AspPerm.dprod_val_le (α β : AspPerm) (a b n : ℤ) : Prop

Equations

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

def AspPerm.ge_dprod (τ α β : AspPerm) : Prop

Equations

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

def AspPerm.eq_dprod (τ α β : AspPerm) : Prop

Equations

• τ.eq_dprod α β = (τ.le_dprod α β ∧ τ.ge_dprod α β)

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

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

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

theorem AspPerm.dprod_inv_eq_inv_dprod (τ α β : AspPerm) (h_eq : τ.eq_dprod α β) : τ⁻¹.eq_dprod β⁻¹ α⁻¹

theorem AspPerm.ramp_dprod_legos (α β : AspPerm) (a b M N : ℤ) (habMN : a - b + α.χ + β.χ = M - N) : α.dprod_val_ge β 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 AspPerm.ess (τ : AspPerm) : Set (ℤ × ℤ)

Equations

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

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

def AspPerm.is_bdiff (τ : AspPerm) : Prop

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

theorem 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 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 AspPerm.bdiff_iff_width (τ : AspPerm) : τ.is_bdiff ↔ ∃ (N : ℤ), 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 AspPerm.bdiff_iff_clifford (τ : AspPerm) : τ.is_bdiff ↔ τ.s.is_clifford

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.*