Submodular Slipfaces and Recovery of ASP Permutations

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

theorem Submodular.unique_a_helper {s : SlipFace} (hsub : s.submodular) (A A' b : ℤ) (hA : ∀ a ≤ A, s.func a b = 0) (hA' : ∀ a ≥ A', s.dual.func (b + 1) a = 0) : A ≤ A' ∧ ∑ a ∈ Finset.Ico A A', s.Δ a b = 1

theorem Submodular.unique_a {s : SlipFace} (hsub : s.submodular) (b : ℤ) : ∃! a : ℤ, (a, b) ∈ s.Γ

theorem Submodular.unique_b {s : SlipFace} (hsub : s.submodular) (a : ℤ) : ∃! b : ℤ, (a, b) ∈ s.Γ

noncomputable def Submodular.asp_func {s : SlipFace} (hsub : s.submodular) : ℤ → ℤ

Equations

• Submodular.asp_func hsub b = Exists.choose ⋯

theorem Submodular.asp_func_spec {s : SlipFace} (hsub : s.submodular) (a b : ℤ) : asp_func hsub b = a ↔ (a, b) ∈ s.Γ

theorem Submodular.asp_bijective {s : SlipFace} (hsub : s.submodular) : Function.Bijective (asp_func hsub)

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

Equations

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

theorem Submodular.asp_spec (s : SlipFace) (hsub : s.submodular) : (asp hsub).sf = s

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

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

This is the paper's identification of $\mathrm{ASP}$ with the submodular slipfaces; in Lean the map $\alpha \mapsto s_\alpha$ is implemented as α ↦ α.sf. Proposition 4.3.

noncomputable def Submodular.AspValley (α β : AspPerm) (a b : ℤ) : Valley

The valley $\ell \mapsto s_\alpha(a,\ell) + s_\beta(\ell,b)$.

Its minimum is $s_{\alpha \star \beta}(a,b)$, and its rightmost minimizer is the paper's $M_{\alpha \star \beta}(a,b)$. In Lean that rightmost minimizer is (AspValley α β a b).M. Definition 4.5.

Equations

• Submodular.AspValley α β a b = { f := fun (l : ℤ) => α.s a l + β.s l b, rises := ⋯ }

theorem Submodular.AspSlipValley (α β : AspPerm) (a b : ℤ) : AspValley α β a b = α.sf.SlipValley β.sf a b

theorem Submodular.AspValley_min_eq_s {α β τ : AspPerm} (dprod : τ.eq_dprod α β) (a b : ℤ) : (AspValley α β a b).min = τ.s a b

If τ = α ⋆ β in the Demazure sense, then the minimum of AspValley α β a b is τ.s a b.

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

theorem Submodular.AspValley_step_a (α β : AspPerm) (a b : ℤ) : have v := AspValley α β a b; have w := 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.7, in slightly different phrasing.

theorem Submodular.AspValley_step_b (α β : AspPerm) (a b : ℤ) : have v := AspValley α β a b; have w := 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.8, in slightly different phrasing.

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

theorem Submodular.submodular_of_basepoint_preserved (s : SlipFace) (a b : ℤ) : s.Δ a b ≥ 0 ↔ s.func (a + 1) b = s.func (a + 1) (b + 1) → s.func a b = s.func a (b + 1)

A local criterion for submodularity: if s (a + 1) b does not drop when b increases, then s a b does not drop either.

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.4, part 1/5.

Demazure Product on AspPerm

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

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

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

theorem AspPerm.star_exists (α β : AspPerm) : ∃! τ : AspPerm, τ.sf = α.sf ⋆ β.sf

The slipface product of two ASP permutations is represented by a unique ASP permutation. Theorem 4.4, part 2/5.

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) : (α ⋆ β).sf = α.sf ⋆ β.sf

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))

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

Demazure product on ASP permutations is associative. Theorem 4.4, part 3/5.

theorem AspPerm.star_valley (α β : AspPerm) (a b : ℤ) : (α ⋆ β).s a b = (Submodular.AspValley α β a b).min

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

Inversion reverses Demazure products. Theorem 4.4, 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.4, part 5/5.

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

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

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

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

instance AspPerm.instPartialOrder : PartialOrder AspPerm

Equations

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

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

The paper's relation $\alpha \leq_\chi \beta$: 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.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.

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.9, part 1.

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

In a Demazure product α ⋆ β, the factor α lies below the product in right weak order. Lemma 4.9, part 2.