Transpositions

This file characterizes the behavior of involutions $\sigma_S$ under the operations $\star$ and $\triangleleft$. Its main purpose is to prove Theorem 8.7 from An extended Demazure product, as well as the last sentences of Theorem A and the theorem labeled thm:resL, which describe the special case of $\sigma_S$ for $S = \{n\}$ a singleton.

def LeanPool.DemazureProduct.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

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

noncomputable def LeanPool.DemazureProduct.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

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

noncomputable def LeanPool.DemazureProduct.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

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

@[simp]

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

theorem LeanPool.DemazureProduct.Transpositions.sf_star_sigma (S : Set ℤ) (hS : NoConsecutive S) (s : SlipFace) (a b : ℤ) : (s ⋆ (sigma S hS).s).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 indicator $\delta(P)$ in An extended Demazure product. Lemma 3.17 (lem:starTrans) of An extended Demazure product, part 3/6.

theorem LeanPool.DemazureProduct.Transpositions.asp_star_sigma_sf (S : Set ℤ) (hS : NoConsecutive S) (α : AspPerm) (a b : ℤ) : (α.s ⋆ (sigma S hS).s).func a b = α.s.func 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.17 (lem:starTrans) of An extended Demazure product, part 4/6.

theorem LeanPool.DemazureProduct.Transpositions.sf_lres_sigma (S : Set ℤ) (hS : NoConsecutive S) (s : SlipFace) (a b : ℤ) : (s ◃ (sigma S hS).s).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 indicator $\delta(P)$ in An extended Demazure product. Lemma 3.17 (lem:starTrans) of An extended Demazure product, part 5/6.

theorem LeanPool.DemazureProduct.Transpositions.asp_residual_sigma_sf (S : Set ℤ) (hS : NoConsecutive S) (α : AspPerm) (a b : ℤ) : (α.s ◃ (sigma S hS).s).func a b = α.s.func 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_residual_sigma. Lemma 3.17 (lem:starTrans) of An extended Demazure product, part 6/6.

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

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

Equations

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

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

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

Equations

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

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

Theorem 8.7 (thm:alphaStarSigma) of An extended Demazure product, part 1/4.

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

Theorem 8.7 (thm:alphaStarSigma) of An extended Demazure product, part 2/4.

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

The simple-transposition case of the Demazure product: if $\sigma \in \mathrm{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 of An extended Demazure product, supplied by Theorem 8.7 (thm:alphaStarSigma) of An extended Demazure product, part 3/4.

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

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

This is the last sentence of Theorem 1.1 (thm:resL) of An extended Demazure product, supplied by Theorem 8.7 (thm:alphaStarSigma) of An extended Demazure product, part 4/4.