Products of non-overlapping adjacent transpositions.

This file follows Definition 3.11 and Theorem 6.8 of the paper: for a set $S$ with no consecutive integers, the permutation $\sigma_S$ swaps every pair $n, n + 1$ with $n \in S$ and fixes all other integers.

def Transpositions.NoConsecutive (S : Set ℤ) : Prop

A set of integers contains no consecutive pair. This asymmetric formulation is enough on ℤ: applying it to n - 1 rules out n - 1, n.

Equations

• Transpositions.NoConsecutive S = ∀ n ∈ S, n + 1 ∉ S

theorem Transpositions.noConsecutive_singleton (n : ℤ) : NoConsecutive {n}

A singleton has no consecutive pair.

noncomputable def Transpositions.sigmaFun (S : Set ℤ) (n : ℤ) : ℤ

The underlying function of $\sigma_S$: swap $n$ with $n + 1$ for every $n \in S$, and fix all other integers.

Equations

• Transpositions.sigmaFun S n = if n ∈ S then n + 1 else if n - 1 ∈ S then n - 1 else n

theorem Transpositions.sigmaFun_of_mem {S : Set ℤ} {n : ℤ} (hn : n ∈ S) : sigmaFun S n = n + 1

theorem Transpositions.sigmaFun_of_pred_mem {S : Set ℤ} (hS : NoConsecutive S) {n : ℤ} (hn : n - 1 ∈ S) : sigmaFun S n = n - 1

theorem Transpositions.sigmaFun_of_not_mem {S : Set ℤ} {n : ℤ} (hn : n ∉ S) (hpred : n - 1 ∉ S) : sigmaFun S n = n

theorem Transpositions.not_succ_mem_of_noConsecutive {S : Set ℤ} (hS : NoConsecutive S) {n : ℤ} (hn : n ∈ S) : n + 1 ∉ S

theorem Transpositions.not_pred_mem_of_noConsecutive {S : Set ℤ} (hS : NoConsecutive S) {n : ℤ} (hn : n ∈ S) : n - 1 ∉ S

theorem Transpositions.sigmaFun_involutive {S : Set ℤ} (hS : NoConsecutive S) : Function.Involutive (sigmaFun S)

theorem Transpositions.sigmaFun_injective {S : Set ℤ} (hS : NoConsecutive S) : Function.Injective (sigmaFun S)

theorem Transpositions.sigmaFun_surjective {S : Set ℤ} (hS : NoConsecutive S) : Function.Surjective (sigmaFun S)

theorem Transpositions.sigmaFun_asp (S : Set ℤ) : is_asp (sigmaFun S)

noncomputable def Transpositions.sigma (S : Set ℤ) (hS : NoConsecutive S) : AspPerm

The ASP permutation $\sigma_S$, exchanging each adjacent pair $n, n + 1$ for $n \in S$.

Equations

• Transpositions.sigma S hS = { func := Transpositions.sigmaFun S, bijective := ⋯, asp := ⋯ }

@[simp]

theorem Transpositions.sigma_apply (S : Set ℤ) (hS : NoConsecutive S) (n : ℤ) : (sigma S hS).func n = sigmaFun S n

theorem Transpositions.sigma_apply_of_mem {S : Set ℤ} {hS : NoConsecutive S} {n : ℤ} (hn : n ∈ S) : (sigma S hS).func n = n + 1

theorem Transpositions.sigma_apply_of_pred_mem {S : Set ℤ} {hS : NoConsecutive S} {n : ℤ} (hn : n - 1 ∈ S) : (sigma S hS).func n = n - 1

theorem Transpositions.sigma_apply_of_not_mem {S : Set ℤ} {hS : NoConsecutive S} {n : ℤ} (hn : n ∉ S) (hpred : n - 1 ∉ S) : (sigma S hS).func n = n

theorem Transpositions.sigma_involutive {S : Set ℤ} (hS : NoConsecutive S) : Function.Involutive (sigma S hS).func

@[simp]

theorem Transpositions.sigma_inv {S : Set ℤ} (hS : NoConsecutive S) : (sigma S hS)⁻¹ = sigma S hS

@[simp]

theorem Transpositions.sigma_chi (S : Set ℤ) (hS : NoConsecutive S) : (sigma S hS).χ = 0

theorem Transpositions.sigma_slipface (S : Set ℤ) (hS : NoConsecutive S) (a b : ℤ) : (sigma S hS).sf.func a b = max 0 (a - b) + Utils.oneIf (a = b ∧ a - 1 ∈ S)

The slipface of $\sigma_S$ is the identity slipface, incremented by 1 on diagonal entries corresponding to the inversions.

theorem Transpositions.bend_set_sigma_of_not_pred_mem (S : Set ℤ) (hS : NoConsecutive S) {b : ℤ} (hb : b - 1 ∉ S) : (sigma S hS).sf.bend_set b = {b}

The bend set for $\sigma_S$ is the singleton $\{b\}$ when $b - 1 \notin S$. This is one case of the computation of L in the proof of Lemma 3.13 (lem:starTrans).

theorem Transpositions.bend_set_sigma_of_pred_mem (S : Set ℤ) (hS : NoConsecutive S) {b : ℤ} (hb : b - 1 ∈ S) : (sigma S hS).sf.bend_set b = {l : ℤ | l = b - 1 ∨ l = b + 1}

The bend set for $\sigma_S$ is $\{b - 1, b + 1\}$ when $b - 1 \in S$. This is one case of the computation of L in the proof of Lemma 3.13 (lem:starTrans).

@[simp]

theorem Transpositions.sigma_sf_dual (S : Set ℤ) (hS : NoConsecutive S) : (sigma S hS).sf.dual = (sigma S hS).sf

theorem Transpositions.sf_star_sigma (S : Set ℤ) (hS : NoConsecutive S) (s : SlipFace) (a b : ℤ) : (s ⋆ (sigma S hS).sf).func a b = s.func a b + Utils.oneIf (b - 1 ∈ S ∧ s.func a (b - 1) > s.func a b ∧ s.func a b = s.func a (b + 1))

The slipface $s \star \sigma_S$ is given by adding 1 to a certain pattern of entries of $s$. The expression Utils.oneIf P is the paper's indicator $\delta(P)$. Lemma 3.13 (lem:starTrans), part 1/2.

theorem Transpositions.asp_star_sigma_sf (S : Set ℤ) (hS : NoConsecutive S) (α : AspPerm) (a b : ℤ) : (α.sf ⋆ (sigma S hS).sf).func a b = α.s a b + Utils.oneIf (b - 1 ∈ S ∧ α.func (b - 1) < a ∧ a ≤ α.func b)

A formula for $s_\alpha \star \sigma_S$, specializing the more general sf_star_sigma. Lemma 3.13 (lem:starTrans), part 1/2.

theorem Transpositions.sf_contract_sigma (S : Set ℤ) (hS : NoConsecutive S) (s : SlipFace) (a b : ℤ) : (s ◃ (sigma S hS).sf).func a b = s.func a b - Utils.oneIf (b - 1 ∈ S ∧ s.func a (b - 1) = s.func a b ∧ s.func a b > s.func a (b + 1))

A formula for $s \triangleleft \sigma_S$.

The expression Utils.oneIf P is the paper's indicator $\delta(P)$. Lemma 3.13 (lem:starTrans), part 2/2.

theorem Transpositions.asp_contract_sigma_sf (S : Set ℤ) (hS : NoConsecutive S) (α : AspPerm) (a b : ℤ) : (α.sf ◃ (sigma S hS).sf).func a b = α.s a b - Utils.oneIf (b - 1 ∈ S ∧ α.func b < a ∧ a ≤ α.func (b - 1))

A formula for $s_\alpha \triangleleft \sigma_S$. This is the ASP specialization of sf_contract_sigma. Lemma 3.13 (lem:starTrans), part 2/2.

def Transpositions.risingSet (α : AspPerm) (S : Set ℤ) : Set ℤ

The subset of $S$ where right multiplication by $\sigma_S$ should increase the permutation in Bruhat order.

Equations

• Transpositions.risingSet α S = {n : ℤ | n ∈ S ∧ α.func n < α.func (n + 1)}

def Transpositions.fallingSet (α : AspPerm) (S : Set ℤ) : Set ℤ

The subset of $S$ where right multiplication by $\sigma_S$ should decrease the permutation in Bruhat order.

Equations

• Transpositions.fallingSet α S = {n : ℤ | n ∈ S ∧ α.func (n + 1) < α.func n}

theorem Transpositions.noConsecutive_subset {S T : Set ℤ} (hS : NoConsecutive S) (hT : T ⊆ S) : NoConsecutive T

theorem Transpositions.noConsecutive_risingSet (α : AspPerm) {S : Set ℤ} (hS : NoConsecutive S) : NoConsecutive (risingSet α S)

theorem Transpositions.noConsecutive_fallingSet (α : AspPerm) {S : Set ℤ} (hS : NoConsecutive S) : NoConsecutive (fallingSet α S)

theorem Transpositions.risingSet_union_fallingSet (α : AspPerm) (S : Set ℤ) : risingSet α S ∪ fallingSet α S = S

The rising and falling parts partition $S$.

theorem Transpositions.fallingSet_union_risingSet (α : AspPerm) (S : Set ℤ) : fallingSet α S ∪ risingSet α S = S

The falling and rising parts partition $S$.

theorem Transpositions.disjoint_risingSet_fallingSet (α : AspPerm) (S : Set ℤ) : Disjoint (risingSet α S) (fallingSet α S)

The rising and falling parts of $S$ are disjoint.

theorem Transpositions.sigma_inv_set_iff (S : Set ℤ) (hS : NoConsecutive S) (u v : ℤ) : (u, v) ∈ inv_set (sigma S hS).func ↔ u ∈ S ∧ v = u + 1

The inversion set of $\sigma_S$ is exactly the adjacent pairs $(n,n+1)$ with $n \in S$.

theorem Transpositions.starSigma (α : AspPerm) (S : Set ℤ) (hS : NoConsecutive S) : α ⋆ sigma S hS = α * sigma (risingSet α S) ⋯

*Theorem 6.8 (thm:alphaStarSigma), part 1/2.

theorem Transpositions.contractSigma (α : AspPerm) (S : Set ℤ) (hS : NoConsecutive S) : α ◃ sigma S hS = α * sigma (fallingSet α S) ⋯

*Theorem 6.8 (thm:alphaStarSigma), part 2/2.

theorem Transpositions.star_of_single_adjacent_inversion (α σ : AspPerm) (n : ℤ) (hχ : σ.χ = 0) (hInv : inv_set σ.func = {(n, n + 1)}) : α ⋆ σ = if α.func n < α.func (n + 1) then α * σ else α

The simple-transposition case of the Demazure product: if $\sigma \in \asp$ has shift zero and its only inversion is $(n,n+1)$, then right Demazure multiplication by $\sigma$ follows the usual rule.

This is the last sentence of Theorem A, supplied by Theorem 8.7 (thm:alphaStarSigma).

theorem Transpositions.contract_of_single_adjacent_inversion (α σ : AspPerm) (n : ℤ) (hχ : σ.χ = 0) (hInv : inv_set σ.func = {(n, n + 1)}) : α ◃ σ = if α.func (n + 1) < α.func n then α * σ else α

The simple-transposition case of left contraction: if $\sigma \in \asp$ has shift zero and its only inversion is $(n,n+1)$, then right contraction by $\sigma$ follows the usual rule.

This is the last sentence of Theorem 1.1 (thm:tll), supplied by Theorem 8.7 (thm:alphaStarSigma).