Submodular slipfaces

This file establishes that a slipface comes from $\mathrm{ASP}$ if and only if it is submodular, and uses this to define the operations $\star$, $\triangleleft$, and $\triangleright$ on $\mathrm{ASP}$. It corresponds roughly to Section 4 of An extended Demazure product.

Submodular slipfaces and recovery of ASP permutations

This section shows that submodular slipfaces are exactly those arising from ASP permutations.

noncomputable def Submodular.asp {s : SlipFace} (hsub : s.submodular) : AspPerm

The ASP permutation associated to a submodular slipface. It can be reconstructed from the set $\Gamma$ in the manner described in Section 4 of An extended Demazure product.

Equations

• Submodular.asp hsub = { func := fun (b : ℤ) => Exists.choose ⋯, bijective := ⋯, asp := ⋯ }

theorem Submodular.submodular_iff_asp (s : SlipFace) : s.submodular ↔ ∃ (α : AspPerm), α.s = s

A slipface is submodular if and only if it is of the form $s_\alpha$ for some ASP permutation α.

Proposition 4.3 (prop:imageASP) of An extended Demazure product., full statement.

Closure of submodularity under product

This section proves that the slipface product of submodular slipfaces is submodular.

theorem Submodular.sediment (v w : Valley) {A : ℤ} (low : ∀ l ≤ A, w.f l = v.f l + 1) (high : ∀ l > A, w.f l = v.f l) : ((v.M ≤ A → w.min = v.min + 1) ∧ (v.M > A → w.min = v.min)) ∧ v.M ≤ w.M

Compare the minima and rightmost minimizers of two valleys that differ by 1 below a cutoff and agree above it. Lemma 4.7 (lem:fg) of An extended Demazure product.

theorem Submodular.AspValley_step_a (α β : AspPerm) (a b : ℤ) : have v := Submodular.AspValley✝ α β a b; have w := Submodular.AspValley✝ α β (a + 1) b; (w.min = v.min + if v.M ≤ α⁻¹.func a then 1 else 0) ∧ v.M ≤ w.M

Incrementing the first coordinate changes the valley minimum by 1 exactly when the rightmost minimizer lies at or to the left of α⁻¹ a, and the rightmost minimizer can only move to the right. Lemma 4.8 (lem:Kstara+1) of An extended Demazure product, in slightly different phrasing.

theorem Submodular.AspValley_step_b (α β : AspPerm) (a b : ℤ) : have v := Submodular.AspValley✝ α β a b; have w := Submodular.AspValley✝ α β a (b + 1); (w.min = v.min - 1 + if v.M ≤ β.func b then 1 else 0) ∧ v.M ≤ w.M

Incrementing the second coordinate changes the valley minimum according to the position of the rightmost minimizer relative to β b, and the rightmost minimizer can only move to the right. Lemma 4.9 (lem:Kstarb+1) of An extended Demazure product, in slightly different phrasing.

theorem Submodular.AspValley_noninc (α β : AspPerm) (a b c : ℤ) (b_le_c : b ≤ c) : have v := Submodular.AspValley✝ α β a b; have w := Submodular.AspValley✝ α β a c; v.M ≤ w.M

theorem Submodular.submodular_of_star {s t : SlipFace} (subS : s.submodular) (subT : t.submodular) : (s ⋆ t).submodular

The product of two submodular slipfaces is submodular. Theorem 4.5 (thm:starExists1) of An extended Demazure product, part 1/5.

Closure of submodularity under residuals

This section proves that the slipface residual operations preserve submodularity.

An extended Demazure product phrases the argument using the rightmost maximizing witness $M_{\alpha \triangleleft \beta}(a,b)$. That maximum may be $\infty$ when the left residual value is zero, since the set of maximizing witnesses may be unbounded above. Rather than extending $\mathbb{Z}$ to include $\infty$, we instead keep the whole witness set and express cutoff conditions on $M$ by quantifying over witnesses: a bound $M \leq m$ becomes a bound on every witness, while $M > m$ becomes the existence of a witness above $m$.

theorem Submodular.lres_candidate_le (α β : AspPerm) (a b l : ℤ) : α.s.func a l - β⁻¹.s.func b l ≤ (α.s ◃ β.s).func a b

Every candidate value for left residual is at most its maximum.

theorem Submodular.submodular_of_lres {s t : SlipFace} (subS : s.submodular) (subT : t.submodular) : (s ◃ t).submodular

The left residual $s \triangleleft t$ of submodular slipfaces is submodular. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 1/11.

theorem Submodular.submodular_of_rres {s t : SlipFace} (subS : s.submodular) (subT : t.submodular) : (s ▹ t).submodular

The right residual $s \triangleright t$ of submodular slipfaces is submodular. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 2/11.

The operations $\star,\; \triangleleft,\; \triangleright$ on AspPerm

Using the slipface construction above, this section defines Demazure product and the two residual operations on ASP permutations and proves its basic structural properties.

theorem AspPerm.eq_of_sf_eq {α β : AspPerm} (eq_sf : α.s = β.s) : α = β

Two ASP permutations are equal if their associated slipfaces are equal.

noncomputable def AspPerm.star (α β : AspPerm) : AspPerm

The Demazure product on ASP permutations, characterized by $$ s_{\alpha \star \beta}(a,b) = \min_{\ell \in \mathbb{Z}} [s_\alpha(a,\ell) + s_\beta(\ell,b)]. $$

In Lean this operation is written α ⋆ β.

Equations

• α ⋆ β = Classical.choose ⋯

@[simp]

theorem AspPerm.star_spec (α β : AspPerm) : (α ⋆ β).s = α.s ⋆ β.s

The Demazure product on ASP is characterized by the equation $s_{\alpha \star \beta} = s_\alpha \star s_\beta$. Theorem 4.5 (thm:starExists1) of An extended Demazure product, part 2/5.

def AspPerm.«term_⋆_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_⋆_» = Lean.ParserDescr.trailingNode `AspPerm.«term_⋆_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ ") (Lean.ParserDescr.cat `term 71))

noncomputable def AspPerm.lres (α β : AspPerm) : AspPerm

Left residual on ASP permutations, characterized by $s_{\alpha \triangleleft \beta} = s_\alpha \triangleleft s_\beta$.

In Lean this operation is written α ◃ β.

Equations

• α ◃ β = Classical.choose ⋯

@[simp]

theorem AspPerm.lres_spec (α β : AspPerm) : (α ◃ β).s = α.s ◃ β.s

Left residual on ASP permutations is characterized by $s_{\alpha \triangleleft \beta} = s_\alpha \triangleleft s_\beta$. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 3/11.

def AspPerm.«term_◃_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_◃_» = Lean.ParserDescr.trailingNode `AspPerm.«term_◃_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 71))

noncomputable def AspPerm.rres (α β : AspPerm) : AspPerm

Right residual on ASP permutations, characterized by $s_{\alpha \triangleright \beta} = s_\alpha \triangleright s_\beta$.

In Lean this operation is written α ▹ β.

Equations

• α ▹ β = Classical.choose ⋯

@[simp]

theorem AspPerm.rres_spec (α β : AspPerm) : (α ▹ β).s = α.s ▹ β.s

Right residual on ASP permutations is characterized by $s_{\alpha \triangleright \beta} = s_\alpha \triangleright s_\beta$. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 4/11.

def AspPerm.«term_▹_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_▹_» = Lean.ParserDescr.trailingNode `AspPerm.«term_▹_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ▹ ") (Lean.ParserDescr.cat `term 70))

theorem AspPerm.star_assoc (α β γ : AspPerm) : α ⋆ β ⋆ γ = α ⋆ (β ⋆ γ)

Demazure product on ASP permutations is associative. Theorem 4.5 (thm:starExists1) of An extended Demazure product, part 3/5.

theorem AspPerm.lres_assoc (α β γ : AspPerm) : α ◃ β ◃ γ = α ◃ (β ⋆ γ)

Left residual associates with Demazure product on ASP permutations. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 5/11.

theorem AspPerm.rres_assoc (α β γ : AspPerm) : α ▹ β ▹ γ = (α ⋆ β) ▹ γ

Right residual associates with Demazure product on ASP permutations. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 6/11.

theorem AspPerm.inverse_lres (α β : AspPerm) : (α ◃ β)⁻¹ = β⁻¹ ▹ α⁻¹

Inversion swaps left residual for right residual. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 7/11.

theorem AspPerm.chi_lres (α β : AspPerm) : (α ◃ β).χ = α.χ + β.χ

The shift of left residual is the sum of shifts. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 8/11.

theorem AspPerm.chi_rres (α β : AspPerm) : (α ▹ β).χ = α.χ + β.χ

The shift of right residual is the sum of shifts. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 9/11.

theorem AspPerm.star_sf_isleast (α β : AspPerm) (a b : ℤ) : IsLeast {x : ℤ | ∃ (l : ℤ), α.s.func a l + β.s.func l b = x} ((α ⋆ β).s.func a b)

The min-plus characterization of the Demazure product on \mathrm{ASP}. This is part of Theorem A (thm:starExists) in An extended Demazure product.

theorem AspPerm.lres_sf_isgreatest (α β : AspPerm) (a b : ℤ) : IsGreatest {x : ℤ | ∃ (l : ℤ), α.s.func a l - β⁻¹.s.func b l = x} ((α ◃ β).s.func a b)

The max-minus characteriztion of the $\triangleleft$ operator on \mathrm{ASP}. This is part of Theorem 1.1 (thm:resL) in An extended Demazure product.

theorem AspPerm.inverse_star (α β : AspPerm) : (α ⋆ β)⁻¹ = β⁻¹ ⋆ α⁻¹

Inversion reverses Demazure products. Theorem 4.5 (thm:starExists1) of An extended Demazure product, part 4/5.

theorem AspPerm.chi_star (α β : AspPerm) : (α ⋆ β).χ = α.χ + β.χ

The shift of a Demazure product satisfies (α ⋆ β).χ = α.χ + β.χ, i.e. $\chi_{\alpha \star \beta} = \chi_\alpha + \chi_\beta$. Theorem 4.5 (thm:starExists1) of An extended Demazure product, part 5/5.

Products and Demazure products of lists of ASP permutations

@[reducible, inline]

noncomputable abbrev AspPerm.DProd (L : List AspPerm) : AspPerm

Demazure product of a list of ASP permutations.

Equations

• AspPerm.DProd L = List.foldr AspPerm.star AspPerm.id L

@[reducible, inline]

noncomputable abbrev AspPerm.OrdProd (L : List AspPerm) : AspPerm

Ordinary product of a list of ASP permutations.

Equations

• AspPerm.OrdProd L = List.foldr (fun (x1 x2 : AspPerm) => x1 * x2) AspPerm.id L

@[simp]

theorem AspPerm.DProd_nil : DProd [] = id

@[simp]

theorem AspPerm.DProd_cons (α : AspPerm) (L : List AspPerm) : DProd (α :: L) = α ⋆ DProd L

@[simp]

theorem AspPerm.OrdProd_nil : OrdProd [] = id

@[simp]

theorem AspPerm.OrdProd_cons (α : AspPerm) (L : List AspPerm) : OrdProd (α :: L) = α * OrdProd L

theorem AspPerm.chi_DProd (L : List AspPerm) : (DProd L).χ = (List.map χ L).sum

The shift of a Demazure list product is the sum of the shifts.

theorem AspPerm.chi_OrdProd (L : List AspPerm) : (OrdProd L).χ = (List.map χ L).sum

The shift of an ordinary list product is the sum of the shifts.

Some properties of the identity permutations

theorem AspPerm.id_s_eq (a b : ℤ) : id.s.func a b = max (a - b) 0

theorem AspPerm.id_sf : id.s = SlipFace.id

theorem AspPerm.id_star (α : AspPerm) : id ⋆ α = α

theorem AspPerm.star_id (α : AspPerm) : α ⋆ id = α

Partial (pre)orders on ASP permutations

@[implicit_reducible]

instance AspPerm.instPartialOrder : PartialOrder AspPerm

The partial order on AspPerm, defined here because antisymmetry uses AspPerm.eq_of_sf_eq.

Equations

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

def AspPerm.le_chi (σ τ : AspPerm) : Prop

The relation $\alpha \leq_\chi \beta$ from An extended Demazure product: Bruhat order together with equality of shifts. In Lean this is the infix ≤χ.

Equations

• (σ ≤χ τ) = (σ ≤ τ ∧ σ.χ = τ.χ)

def AspPerm.«term_≤χ_» : Lean.TrailingParserDescr

Equations

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

theorem AspPerm.s_le_iff (α β : AspPerm) : α.s ≤ β.s ↔ α ≤ β

Bruhat order on ASP permutations agrees with pointwise order on their slipfaces.

theorem AspPerm.le_chi_inv_iff (α β : AspPerm) : α ≤χ β ↔ α⁻¹ ≤χ β⁻¹

Inversion preserves Bruhat comparisons between ASP permutations of the same shift. Lemma 2.1 (lem:bruhatInverse) of An extended Demazure product.

theorem AspPerm.id_le_of_chi_nonneg {τ : AspPerm} (hχ : 0 ≤ τ.χ) : id ≤ τ

An ASP permutation of nonnegative shift lies above the identity in Bruhat order. This is the $\chi = 0$ case of the minimum-shift observation after Definition 2.5 in An extended Demazure product.

theorem AspPerm.star_mono {α₁ α₂ β₁ β₂ : AspPerm} (hα : α₁ ≤ α₂) (hβ : β₁ ≤ β₂) : α₁ ⋆ β₁ ≤ α₂ ⋆ β₂

Demazure product on ASP permutations is Bruhat-increasing in both arguments. This lifts the slipface comparison of Lemma 3.8 in An extended Demazure product.

theorem AspPerm.ge_star_iff_ge_lres (α β τ : AspPerm) : α ≥ τ ◃ β⁻¹ ↔ α ⋆ β ≥ τ

The left residual $\tau \triangleleft \beta^{-1}$ is the Bruhat minimum of the ASP permutations $\alpha$ such that $\alpha \star \beta \geq \tau$. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 10/11.

theorem AspPerm.ge_star_iff_ge_rres (α β τ : AspPerm) : β ≥ α⁻¹ ▹ τ ↔ α ⋆ β ≥ τ

The right residual $\alpha^{-1} \triangleright \tau$ is the Bruhat minimum of the ASP permutations $\beta$ such that $\alpha \star \beta \geq \tau$. Theorem 4.11 (thm:resLExists) of An extended Demazure product, part 11/11.

theorem AspPerm.lres_eq_min (α β : AspPerm) : IsLeast {γ : AspPerm | γ ⋆ β ≥ α} (α ◃ β⁻¹)

The left residual $\alpha \triangleleft \beta^{-1}$ is the minimum permutation $\gamma$ such that $\gamma \star \beta \ge \alpha$. This is the first sentence of Theorem 1.1 (thm:resL) in An extended Demazure product.

theorem AspPerm.rres_eq_min (α β : AspPerm) : IsLeast {γ : AspPerm | α ⋆ γ ≥ β} (α⁻¹ ▹ β)

theorem AspPerm.le_star_iff (τ α β : AspPerm) : τ ≤ α ⋆ β ↔ τ.le_dprod α β

Comparison τ ≤ α ⋆ β is equivalent to the lower Demazure-product inequalities defining τ.le_dprod α β.

theorem AspPerm.ge_star_iff (τ α β : AspPerm) : α ⋆ β ≤ τ ↔ τ.ge_dprod α β

Comparison α ⋆ β ≤ τ is equivalent to the upper Demazure-product inequalities defining τ.ge_dprod α β.

theorem AspPerm.eq_star_iff {τ α β : AspPerm} : τ = α ⋆ β ↔ τ.eq_dprod α β

Equality τ = α ⋆ β is equivalent to satisfying both Demazure comparison conditions.

theorem AspPerm.ess_bdiff (α β : AspPerm) (bdiff : α.is_bdiff) : α ≤ β ↔ α.χ ≤ β.χ ∧ ∀ (a b : ℤ), (a, b) ∈ α.ess → α.s.func a b ≤ β.s.func a b

Comparison of ASP permutations in the Bruhat order using essential set. This is Corollary 7.9 (cor:essBD) in An extended Demazure product. This theorem is delayed until this file since the definition of ≤ on ASP is needed for the statement.

Weak-order consequences of Demazure product

The final results in this file record the weak-order inequalities satisfied by the factors of a Demazure product.

theorem Submodular.lel_of_dprod (α β : AspPerm) : β ≤L α ⋆ β

In a Demazure product α ⋆ β, the factor β lies below the product in left weak order. Lemma 4.10 (lem:invStar) of An extended Demazure product, part 1/2.

theorem Submodular.ler_of_dprod (α β : AspPerm) : α ≤R α ⋆ β

In a Demazure product α ⋆ β, the factor α lies below the product in right weak order. Lemma 4.10 (lem:invStar) of An extended Demazure product, part 2/2.

Weak-order consequences of residuals

theorem Submodular.reducedProduct_of_lres (α β : AspPerm) : (α ◃ β).ReducedProduct β⁻¹

Left residual forms a reduced product with the inverse of its right factor. Lemma 4.15 (lem:invRes) of An extended Demazure product, part 1/2.

theorem Submodular.ler_of_lres (α β : AspPerm) : α ◃ β ≤R α

Left residual is below its left factor in right weak order. Lemma 4.15 (lem:invRes) of An extended Demazure product, part 2/2.

theorem Submodular.reducedProduct_of_rres (α β : AspPerm) : α⁻¹.ReducedProduct (α ▹ β)

Right residual forms a reduced product with the inverse of its left factor. Corollary 4.16 (cor:reducedResR) of An extended Demazure product, part 1/2.

theorem Submodular.lel_of_rres (α β : AspPerm) : α ▹ β ≤L β

Right residual is below its right factor in left weak order. Corollary 4.16 (cor:reducedResR) of An extended Demazure product, part 2/2.