Slipfaces

This file defines slipface functions and develops their basic properties, including the $\star$ (Demazure product) and residuals $\triangleleft$ and $\triangleright$. It corresponds roughly to Section 3, with some essential-set material from Section 7.1, of An extended Demazure product.

structure LeanPool.DemazureProduct.SlipFace : Type

A slipface function of shift χ, i.e. a function $s : \mathbb{Z}^2 \to \mathbb{N}$ satisfying conditions (S1) to (S3) from An extended Demazure product:

• first differences in the a- and b-directions are in {0,1}
• $s(a,b) \ge \max\{0, \chi + a - b\}$
• each row and column eventually agrees with $\max\{0, \chi + a - b\}$

Lean stores the function as func and the shift as χ; the article writes this as $s \in \mathrm{SF}_\chi$. Definition 3.1 (defn:slipface) of An extended Demazure product.

• func : ℤ → ℤ → ℤ

  The integer-valued slipface function.

• χ : ℤ

  The shift of the slipface.

• a_step (a b : ℤ) : self.func a b ≤ self.func (a + 1) b ∧ self.func (a + 1) b ≤ self.func a b + 1
• b_step (a b : ℤ) : self.func a (b + 1) ≤ self.func a b ∧ self.func a b ≤ self.func a (b + 1) + 1
• nonneg (a b : ℤ) : self.func a b ≥ 0
• ge_diff (a b : ℤ) : self.func a b ≥ a - b + self.χ
• small_a (b : ℤ) : ∃ (A : ℤ), ∀ a ≤ A, self.func a b = 0
• large_a (b : ℤ) : ∃ (A : ℤ), ∀ a ≥ A, self.func a b = a - b + self.χ
• small_b (a : ℤ) : ∃ (B : ℤ), ∀ b ≤ B, self.func a b = a - b + self.χ
• large_b (a : ℤ) : ∃ (B : ℤ), ∀ b ≥ B, self.func a b = 0

@[implicit_reducible]

instance LeanPool.DemazureProduct.instCoeFunSlipFaceForallIntForall : CoeFun SlipFace fun (x : SlipFace) => ℤ → ℤ → ℤ

Equations

• LeanPool.DemazureProduct.instCoeFunSlipFaceForallIntForall = { coe := LeanPool.DemazureProduct.SlipFace.func }

theorem LeanPool.DemazureProduct.SF_ext (s t : SlipFace) : s = t ↔ ∀ (a b : ℤ), s.func a b = t.func a b

def LeanPool.DemazureProduct.SlipFace.dual (sf : SlipFace) : SlipFace

The dual slipface $s^\vee$, characterized by $$ s(a,b) - s^\vee(b,a) = \chi + a - b. $$

In Lean the dual is sf.dual, and its value at (b,a) is written sf.dual b a. Definition 3.4 (defn:sdual) of An extended Demazure product.

Equations

• sf.dual = { func := fun (b a : ℤ) => sf.func a b - a + b - sf.χ, χ := -sf.χ, a_step := ⋯, b_step := ⋯, nonneg := ⋯, ge_diff := ⋯, small_a := ⋯, large_a := ⋯, small_b := ⋯, large_b := ⋯ }

theorem LeanPool.DemazureProduct.SlipFace.dual_dual (s : SlipFace) : s.dual.dual = s

theorem LeanPool.DemazureProduct.SlipFace.duality (sf : SlipFace) (a b : ℤ) : sf.func a b - sf.dual.func b a = a - b + sf.χ

theorem LeanPool.DemazureProduct.SlipFace.s_eq (sf : SlipFace) (a b : ℤ) : sf.func a b = a - b + sf.χ + sf.dual.func b a

theorem LeanPool.DemazureProduct.SlipFace.s'_eq (sf : SlipFace) (b a : ℤ) : sf.dual.func b a = sf.func a b - a + b - sf.χ

theorem LeanPool.DemazureProduct.SlipFace.ge_max (sf : SlipFace) (a b : ℤ) : sf.func a b ≥ max 0 (a - b + sf.χ)

theorem LeanPool.DemazureProduct.SlipFace.gt_iff_special (sf : SlipFace) (a b : ℤ) : sf.func a b > max 0 (a - b + sf.χ) ↔ sf.func a b > 0 ∧ sf.dual.func b a > 0

theorem LeanPool.DemazureProduct.SlipFace.eq_iff_nonspecial (sf : SlipFace) (a b : ℤ) : sf.func a b = max 0 (a - b + sf.χ) ↔ sf.func a b = 0 ∨ sf.dual.func b a = 0

structure LeanPool.DemazureProduct.SlipFace.D_props (f : ℤ → ℤ → ℤ) : Prop

The one-sided monotonicity and vanishing conditions providing a simplified criterion for slipfaces.

These are conditions (D1) and (D2) from An extended Demazure product, extracted into a reusable Lean structure. Properties D1 and D2.

• a_step (a b : ℤ) : f (a + 1) b ≥ f a b
• b_step (a b : ℤ) : f a (b + 1) ≤ f a b
• large_b (a : ℤ) : ∃ (B : ℤ), ∀ b ≥ B, f a b = 0
• small_a (b : ℤ) : ∃ (A : ℤ), ∀ a ≤ A, f a b = 0

theorem LeanPool.DemazureProduct.SlipFace.mono_a_of_D_props (f : ℤ → ℤ → ℤ) (h : D_props f) (a a' b : ℤ) : a ≤ a' → f a' b ≥ f a b

theorem LeanPool.DemazureProduct.SlipFace.mono_b_of_D_props (f : ℤ → ℤ → ℤ) (h : D_props f) (a b b' : ℤ) : b ≤ b' → f a b' ≤ f a b

theorem LeanPool.DemazureProduct.SlipFace.sf_of_D_props {s t : ℤ → ℤ → ℤ} {χ : ℤ} (h : ∀ (a b : ℤ), s a b - t b a = a - b + χ) : D_props s ∧ D_props t → ∃ (sf : SlipFace), (sf.func = s ∧ sf.χ = χ) ∧ sf.dual.func = t

Construct a slipface from a pair of functions satisfying D_props and the duality relation s a b - t b a = a - b + χ. Lemma 3.6 (lem:dualCrit) of An extended Demazure product, part 1/2.

theorem LeanPool.DemazureProduct.SlipFace.D_props_of_sf (sf : SlipFace) : D_props sf.func ∧ D_props sf.dual.func

Every slipface function and its dual satisfies the D_props, denoted (D1) and (D2). Lemma 3.6 (lem:dualCrit) of An extended Demazure product, part 2/2.

theorem LeanPool.DemazureProduct.SlipFace.nondec (sf : SlipFace) {a a' b b' : ℤ} (a_le_a' : a ≤ a') (b'_le_b : b' ≤ b) : sf.func a b ≤ sf.func a' b'

theorem LeanPool.DemazureProduct.SlipFace.zero_below (sf : SlipFace) {a a' b b' : ℤ} (a_le_a' : a ≤ a') (b'_le_b : b' ≤ b) : sf.func a' b' = 0 → sf.func a b = 0

Slip valleys and the product formula

A Valley is an integer function rising on both sides, which therefore has a well-defined minimum achieved at finitely many places.

This section packages the minimization problem defining slipface product into a Valley, then uses it to construct the product s ⋆ t and prove its basic properties.

noncomputable def LeanPool.DemazureProduct.SlipFace.SlipValley (s t : SlipFace) (a b : ℤ) : Valley

The valley $\ell \mapsto s(a,\ell) + t(\ell,b)$ whose minimum computes the slipface product at (a,b).

Equations

• s.SlipValley t a b = { f := fun (l : ℤ) => s.func a l + t.func l b, rises := ⋯ }

noncomputable def LeanPool.DemazureProduct.SlipFace.starFunc (s t : SlipFace) : ℤ → ℤ → ℤ

The min-plus product formula $$ (s \star t)(a,b) = \min_{\ell \in \mathbb{Z}} [s(a,\ell) + t(\ell,b)]. $$

In Lean, starFunc s t a b is this integer value, while s ⋆ t is the resulting SlipFace. See Definition 3.7 (defn:sfAlgebra) of An extended Demazure product.

Equations

• s.starFunc t a b = (s.SlipValley t a b).min

theorem LeanPool.DemazureProduct.SlipFace.star_dual_ineq (s t : SlipFace) (a b : ℤ) : t.dual.starFunc s.dual b a ≤ s.starFunc t a b - a + b - s.χ - t.χ

theorem LeanPool.DemazureProduct.SlipFace.star_dual_eq (s t : SlipFace) (a b : ℤ) : s.starFunc t a b - t.dual.starFunc s.dual b a = a - b + s.χ + t.χ

noncomputable def LeanPool.DemazureProduct.SlipFace.star (s t : SlipFace) : SlipFace

The product of two slipfaces, obtained from the minimum formula starFunc. See Definition 3.7 (defn:sfAlgebra) of An extended Demazure product.*

Equations

• s ⋆ t = Classical.choose ⋯

@[implicit_reducible]

noncomputable instance LeanPool.DemazureProduct.SlipFace.instMul : Mul SlipFace

Equations

• LeanPool.DemazureProduct.SlipFace.instMul = { mul := LeanPool.DemazureProduct.SlipFace.star }

def LeanPool.DemazureProduct.SlipFace.«term_⋆_» : Lean.TrailingParserDescr

Infix notation for the slipface Demazure product.

Equations

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

theorem LeanPool.DemazureProduct.SlipFace.star_func_eq (s t : SlipFace) : (s ⋆ t).func = s.starFunc t

theorem LeanPool.DemazureProduct.SlipFace.star_eq_min (s t : SlipFace) (a b : ℤ) : IsLeast {x : ℤ | ∃ (l : ℤ), s.func a l + t.func l b = x} ((s ⋆ t).func a b)

The formula for the Demazure product of slipfaces: $s \star t(a,b) = \min_{l \in \mathbb{Z}} (s(a,l) + t(l,b))$. This unpacks the formal definition of $\star$ into the form of Definition 3.7 (defn:sfAlgebra) of An extended Demazure product, part 1/3.*

@[simp]

theorem LeanPool.DemazureProduct.SlipFace.chi_star (s t : SlipFace) : (s ⋆ t).χ = s.χ + t.χ

The shift is additive under $\star$. Proposition 3.9 (prop:sfAlgebraDefined) of An extended Demazure product, part 1/6.*

@[simp]

theorem LeanPool.DemazureProduct.SlipFace.star_dual (s t : SlipFace) : (s ⋆ t).dual = t.dual ⋆ s.dual

Duality reverses the product ⋆. Proposition 3.9 (prop:sfAlgebraDefined) of An extended Demazure product, part 2/6.

Order structure and comparison with ⋆

This section defines the Bruhat order on SlipFace and records the basic comparison lemmas relating that order to the product ⋆. Definition 3.2 of An extended Demazure product.

@[implicit_reducible]

instance LeanPool.DemazureProduct.SlipFace.instPartialOrder : PartialOrder SlipFace

Equations

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

theorem LeanPool.DemazureProduct.SlipFace.star_val_le (s t : SlipFace) (a b l : ℤ) : (s ⋆ t).func a b ≤ s.func a l + t.func l b

noncomputable def LeanPool.DemazureProduct.SlipFace.starWit (s t : SlipFace) (a b : ℤ) : ℤ

A minimizer witnessing the slipface Demazure product value at (a, b).

Equations

• s.starWit t a b = (s.SlipValley t a b).M

theorem LeanPool.DemazureProduct.SlipFace.star_wit_spec (s t : SlipFace) (a b : ℤ) : (s ⋆ t).func a b = s.func a (s.starWit t a b) + t.func (s.starWit t a b) b

theorem LeanPool.DemazureProduct.SlipFace.le_star_val_iff (r s t : SlipFace) (a b : ℤ) : r.func a b ≤ (s ⋆ t).func a b ↔ ∀ (l : ℤ), r.func a b ≤ s.func a l + t.func l b

A lower bound for (s ⋆ t) a b is equivalent to a uniform lower bound against every witness l.

theorem LeanPool.DemazureProduct.SlipFace.ge_star_val_iff (r s t : SlipFace) (a b : ℤ) : r.func a b ≥ (s ⋆ t).func a b ↔ ∃ (l : ℤ), r.func a b ≥ s.func a l + t.func l b

An upper bound for (s ⋆ t) a b is equivalent to exhibiting a single witness l that realizes it.

Monoid structure

The product ⋆ is associative and has the positive-part function as identity, giving SlipFace a monoid structure.

theorem LeanPool.DemazureProduct.SlipFace.star_assoc (r s t : SlipFace) : r ⋆ s ⋆ t = r ⋆ (s ⋆ t)

Slipface product is associative. Lemma 3.12 (lem:sfAlgebra) of An extended Demazure product, part 1/3.

def LeanPool.DemazureProduct.SlipFace.id : SlipFace

The identity slipface, given by the positive part of a - b.

Equations

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

theorem LeanPool.DemazureProduct.SlipFace.id_mul (s : SlipFace) : id ⋆ s = s

theorem LeanPool.DemazureProduct.SlipFace.mul_id (s : SlipFace) : s ⋆ id = s

@[implicit_reducible]

noncomputable instance LeanPool.DemazureProduct.SlipFace.instMonoid : Monoid SlipFace

Equations

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

The residual operations ◃ and ▹

This section develops the basic properties of the operations $s \triangleleft t$ and $s \triangleright t$ at the level of slipface functions.

theorem LeanPool.DemazureProduct.SlipFace.lres_wit_exists (s t : SlipFace) (a b : ℤ) : ∃ (m : ℤ), ∀ (l : ℤ), s.func a l - t.dual.func b l ≤ s.func a m - t.dual.func b m

noncomputable def LeanPool.DemazureProduct.SlipFace.lresWit (s t : SlipFace) (a b : ℤ) : ℤ

The argmax witnessing the left residual value $s \triangleleft t (a,b)$.

Equations

• s.lresWit t a b = Classical.choose ⋯

noncomputable def LeanPool.DemazureProduct.SlipFace.lresFunc (s t : SlipFace) : ℤ → ℤ → ℤ

The left residual function $$ (s \triangleleft t)(a,b) = \max_{\ell \in \mathbb{Z}} \bigl[s(a,\ell) - t^\vee(b,\ell)\bigr]. $$ See Definition 3.7 (defn:sfAlgebra) of An extended Demazure product.

Equations

• s.lresFunc t a b = s.func a (s.lresWit t a b) - t.dual.func b (s.lresWit t a b)

theorem LeanPool.DemazureProduct.SlipFace.lres_val_ge (s t : SlipFace) (a b l : ℤ) : s.func a l - t.dual.func b l ≤ s.lresFunc t a b

Every value $s(a,\ell) - t^\vee(b,\ell)$ is at most $s \triangleleft t (a,b)$.

theorem LeanPool.DemazureProduct.SlipFace.lres_func_nonneg (s t : SlipFace) (a b : ℤ) : 0 ≤ s.lresFunc t a b

The left residual is nonnegative, since for l ≫ 0 both terms in the maximizing expression vanish.

noncomputable def LeanPool.DemazureProduct.SlipFace.rresWit (s t : SlipFace) (a b : ℤ) : ℤ

The argmax witnessing the right residual value $s \triangleright t (a,b)$.

Equations

• s.rresWit t a b = Classical.choose ⋯

noncomputable def LeanPool.DemazureProduct.SlipFace.rresFunc (s t : SlipFace) : ℤ → ℤ → ℤ

The right residual function $$ (s \triangleright t)(a,b) = \max_{\ell \in \mathbb{Z}} \bigl[t(\ell,b) - s^\vee(\ell,a)\bigr]. $$ Definition 3.7 (defn:sfAlgebra) of An extended Demazure product.

Equations

• s.rresFunc t a b = t.func (s.rresWit t a b) b - s.dual.func (s.rresWit t a b) a

theorem LeanPool.DemazureProduct.SlipFace.rres_val_ge (s t : SlipFace) (a b l : ℤ) : t.func l b - s.dual.func l a ≤ s.rresFunc t a b

Every value $t(\ell,b) - s^\vee(\ell,a)$ is at most $s \triangleright t (a,b)$.

theorem LeanPool.DemazureProduct.SlipFace.rres_func_nonneg (s t : SlipFace) (a b : ℤ) : 0 ≤ s.rresFunc t a b

The right residual is nonnegative, since for l ≪ 0 both terms in the maximizing expression vanish.

noncomputable def LeanPool.DemazureProduct.SlipFace.lres (s t : SlipFace) : SlipFace

The left residual of two slipfaces, obtained from the maximum formula lresFunc. See Definition 3.7 (defn:sfAlgebra) of An extended Demazure product.

Equations

• s ◃ t = Classical.choose ⋯

def LeanPool.DemazureProduct.SlipFace.«term_◃_» : Lean.TrailingParserDescr

Infix notation for the slipface left residual.

Equations

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

theorem LeanPool.DemazureProduct.SlipFace.lres_func_eq (s t : SlipFace) : (s ◃ t).func = s.lresFunc t

theorem LeanPool.DemazureProduct.SlipFace.lres_wit_spec (s t : SlipFace) (a b : ℤ) : (s ◃ t).func a b = s.func a (s.lresWit t a b) - t.dual.func b (s.lresWit t a b)

theorem LeanPool.DemazureProduct.SlipFace.lres_eq_max (s t : SlipFace) (a b : ℤ) : IsGreatest {x : ℤ | ∃ (l : ℤ), s.func a l - t.dual.func b l = x} ((s ◃ t).func a b)

The left residual $s \triangleleft t$ of slipfaces satisfies the defining equation $(s ◃ t)(a,b) = \max_{\ell \in \mathbb{Z}} (s(a,\ell) - t^\vee(b,\ell))$. This is simply an unwinding of the formal definition to obtain the formula as stated in Definition 3.7 (defn:sfAlgebra) of An extended Demazure product, part 2/3.*

@[simp]

theorem LeanPool.DemazureProduct.SlipFace.chi_lres (s t : SlipFace) : (s ◃ t).χ = s.χ + t.χ

The shift is additive under left residual. Proposition 3.9 (prop:sfAlgebraDefined) of An extended Demazure product, part 3/6.*

noncomputable def LeanPool.DemazureProduct.SlipFace.rres (s t : SlipFace) : SlipFace

The right residual of two slipfaces, defined by duality from left residual. See Definition 3.7 (defn:sfAlgebra) of An extended Demazure product.

Equations

• s ▹ t = (t.dual ◃ s.dual).dual

def LeanPool.DemazureProduct.SlipFace.«term_▹_» : Lean.TrailingParserDescr

Infix notation for the slipface right residual.

Equations

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

theorem LeanPool.DemazureProduct.SlipFace.rres_func_eq (s t : SlipFace) : (s ▹ t).func = s.rresFunc t

theorem LeanPool.DemazureProduct.SlipFace.rres_wit_spec (s t : SlipFace) (a b : ℤ) : (s ▹ t).func a b = t.func (s.rresWit t a b) b - s.dual.func (s.rresWit t a b) a

theorem LeanPool.DemazureProduct.SlipFace.rres_eq_max (s t : SlipFace) (a b : ℤ) : IsGreatest {x : ℤ | ∃ (l : ℤ), t.func l b - s.dual.func l a = x} ((s ▹ t).func a b)

The right residual $s \triangleright t$ of slipfaces satisfies the defining equation $(s ▹ t)(a,b) = \max_{\ell \in \mathbb{Z}} (t(\ell,b) - s^\vee(\ell,a))$. This is simply an unwinding of the formal definition to obtain the formula as stated in Definition 3.7 (defn:sfAlgebra) of An extended Demazure product, part 3/3.*

@[simp]

theorem LeanPool.DemazureProduct.SlipFace.chi_rres (s t : SlipFace) : (s ▹ t).χ = s.χ + t.χ

The shift is additive under right residual. Proposition 3.9 (prop:sfAlgebraDefined) of An extended Demazure product, part 4/6.*

@[simp]

theorem LeanPool.DemazureProduct.SlipFace.lres_dual (s t : SlipFace) : (s ◃ t).dual = t.dual ▹ s.dual

The stated left/right residual duality. Proposition 3.9 (prop:sfAlgebraDefined) of An extended Demazure product, part 5/6.

@[simp]

theorem LeanPool.DemazureProduct.SlipFace.rres_dual (s t : SlipFace) : (s ▹ t).dual = t.dual ◃ s.dual

The corresponding right/left residual duality, obtained by applying the left/right duality to dual slipfaces. Consequence of Proposition 3.9 (prop:sfAlgebraDefined) in An extended Demazure product, part 6/6.

def LeanPool.DemazureProduct.SlipFace.bendSet (t : SlipFace) (b : ℤ) : Set ℤ

A small set on which witnesses to the value $s \star t (a,b)$ always occur. Lemma 3.13 (lem:setL) of An extended Demazure product, part 1/5.

Equations

• t.bendSet b = {l : ℤ | t.func (l - 1) b = t.func l b ∧ t.func l b ≠ t.func (l + 1) b}

theorem LeanPool.DemazureProduct.SlipFace.bend_set_finite (t : SlipFace) (b : ℤ) : Finite ↑(t.bendSet b)

Lemma 3.13 (lem:setL) of An extended Demazure product, part 2/5.

theorem LeanPool.DemazureProduct.SlipFace.bend_set_witness (s t : SlipFace) (a b : ℤ) : ∃ l ∈ t.bendSet b, (s ⋆ t).func a b = s.func a l + t.func l b

Lemma 3.13 (lem:setL) of An extended Demazure product, part 3/5.

theorem LeanPool.DemazureProduct.SlipFace.bend_set_witness_lres (s t : SlipFace) (a b : ℤ) : ∃ l ∈ t.bendSet b, (s ◃ t).func a b = s.func a l - t.dual.func b l

Lemma 3.13 (lem:setL) of An extended Demazure product, part 4/5.

Minimal slipfaces in each shift

def LeanPool.DemazureProduct.SlipFace.iotaSf (n : ℤ) : SlipFace

The slipface $s_{\iota_n}$, which is the minimal slipface of shift $n$. It is given simply by $s(a,b) = \max(a - b + n, 0)$.

Equations

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

Monotonicity, adjointness, and associativity

theorem LeanPool.DemazureProduct.SlipFace.star_mono {s₁ s₂ t₁ t₂ : SlipFace} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : s₁ ⋆ t₁ ≤ s₂ ⋆ t₂

The $\star$ operation is Bruhat-increasing in both arguments. Lemma 3.8 (lem:compatLeq) of An extended Demazure product, part 1/3.

theorem LeanPool.DemazureProduct.SlipFace.lres_mono {s₁ s₂ t₁ t₂ : SlipFace} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : s₁ ◃ t₂.dual ≤ s₂ ◃ t₁.dual

The residual (s, t) ↦ s ◃ t.dual is increasing in s and decreasing in t. Lemma 3.8 (lem:compatLeq) of An extended Demazure product, part 2/3.

theorem LeanPool.DemazureProduct.SlipFace.rres_mono {s₁ s₂ t₁ t₂ : SlipFace} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : t₂.dual ▹ s₁ ≤ t₁.dual ▹ s₂

The residual (s, t) ↦ t.dual ▹ s is increasing in s and decreasing in t. Lemma 3.8 (lem:compatLeq) of An extended Demazure product, part 3/3.

theorem LeanPool.DemazureProduct.SlipFace.ge_star_iff_ge_lres (s t u : SlipFace) : s ≥ u ◃ t.dual ↔ s ⋆ t ≥ u

The left residual $u \triangleleft t^∨$ as a Bruhat minimum: the minimum slipface such that $s \star t ≥ u$. Lemma 3.10 (lem:sfOpChar) of An extended Demazure product, part 1/2.

theorem LeanPool.DemazureProduct.SlipFace.ge_star_iff_ge_rres (s t u : SlipFace) : t ≥ s.dual ▹ u ↔ s ⋆ t ≥ u

The right residual $s^∨ \triangleright u$ as a Bruhat minimum: the minimum slipface such that $s \star t ≥ u$. Lemma 3.10 (lem:sfOpChar) of An extended Demazure product, part 2/2.

theorem LeanPool.DemazureProduct.SlipFace.lres_assoc (s t u : SlipFace) : s ◃ t ◃ u = s ◃ (t ⋆ u)

Left residual associates with the product on the right. Lemma 3.12 (lem:sfAlgebra) of An extended Demazure product, part 2/3.

theorem LeanPool.DemazureProduct.SlipFace.rres_assoc (s t u : SlipFace) : s ▹ t ▹ u = (s ⋆ t) ▹ u

Right residual associates with the product on the left. Lemma 3.12 (lem:sfAlgebra) of An extended Demazure product, part 3/3.

The mixed difference Δ

This section studies the discrete mixed difference Δ, its behavior under duality, and the finite summation identities used later in submodularity arguments.

def LeanPool.DemazureProduct.SlipFace.Δ (sf : SlipFace) (a b : ℤ) : ℤ

The mixed difference $$ \Delta s(a,b) = s(a+1,b) - s(a,b) - s(a+1,b+1) + s(a,b+1). $$

In Lean this is written sf.Δ a b.

Equations

• sf.Δ a b = sf.func (a + 1) b - sf.func a b - sf.func (a + 1) (b + 1) + sf.func a (b + 1)

theorem LeanPool.DemazureProduct.SlipFace.Δ_dual (sf : SlipFace) (a b : ℤ) : sf.dual.Δ b a = sf.Δ a b

Duality preserves the mixed difference Δ after swapping the coordinates. Equation (20) (eq:DeltasDual) of An extended Demazure product.

theorem LeanPool.DemazureProduct.SlipFace.Δ_values (sf : SlipFace) (a b : ℤ) : sf.Δ a b = 0 ∨ sf.Δ a b = 1 ∨ sf.Δ a b = -1

theorem LeanPool.DemazureProduct.SlipFace.Δ_zero_of_s_zero (sf : SlipFace) (a b : ℤ) (h0 : sf.func (a + 1) b = 0) : sf.Δ a b = 0

theorem LeanPool.DemazureProduct.SlipFace.sum_a (sf : SlipFace) {a₁ a₂ : ℤ} (ha : a₁ ≤ a₂) (b : ℤ) : ∑ a ∈ Finset.Ico a₁ a₂, sf.Δ a b = sf.func a₂ b - sf.func a₂ (b + 1) - (sf.func a₁ b - sf.func a₁ (b + 1))

theorem LeanPool.DemazureProduct.SlipFace.sum_b (sf : SlipFace) (a : ℤ) {b₁ b₂ : ℤ} (hb : b₁ ≤ b₂) : ∑ b ∈ Finset.Ico b₁ b₂, sf.Δ a b = sf.func (a + 1) b₁ - sf.func a b₁ - (sf.func (a + 1) b₂ - sf.func a b₂)

theorem LeanPool.DemazureProduct.SlipFace.sum_ab (sf : SlipFace) {a₁ a₂ b₁ b₂ : ℤ} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : ∑ b ∈ Finset.Ico b₁ b₂, ∑ a ∈ Finset.Ico a₁ a₂, sf.Δ a b = sf.func a₂ b₁ - sf.func a₁ b₁ - (sf.func a₂ b₂ - sf.func a₁ b₂)

Summing Δ over a rectangle recovers the corresponding boundary term in sf. Modification of Equation (19) (eq:sumDelta) of An extended Demazure product to a finite sum.

def LeanPool.DemazureProduct.SlipFace.submodular (sf : SlipFace) : Prop

A slipface is submodular if $\Delta s(a,b) \ge 0$ for all a, b. Definition 4.2 (defn:submodular) of An extended Demazure product.

Equations

• sf.submodular = ∀ (a b : ℤ), sf.Δ a b ≥ 0

def LeanPool.DemazureProduct.SlipFace.Γ (sf : SlipFace) : Set (ℤ × ℤ)

The set of boxes where the mixed difference Δ is equal to 1, as defined in the proof of Proposition 4.3 (prop:imageASP) of An extended Demazure product.*

Equations

• sf.Γ = {(a, b) : ℤ × ℤ | sf.Δ a b = 1}

theorem LeanPool.DemazureProduct.SlipFace.Γ_dual (sf : SlipFace) (a b : ℤ) : (a, b) ∈ sf.Γ ↔ (b, a) ∈ sf.dual.Γ

The essential set of a slipface

This section includes the content of §7.1 of An extended Demazure product, about the essential set of a slipface.

def LeanPool.DemazureProduct.SlipFace.ess (sf : SlipFace) : Set (ℤ × ℤ)

The essential set of a slipface $s$ is the set $\operatorname{Ess}(s) = \{ (a,b) \in \mathbb{Z}^2: s(a-1,b) < s(a,b) = s(a+1,b) \mbox{ and } s(a,b+1) < s(a,b) = s(a,b-1) \}.$

Equations

• sf.ess = {(a, b) : ℤ × ℤ | sf.func (a - 1) b < sf.func a b ∧ sf.func a b = sf.func (a + 1) b ∧ sf.func a (b + 1) < sf.func a b ∧ sf.func a b = sf.func a (b - 1)}

theorem LeanPool.DemazureProduct.SlipFace.ess_step (s t : SlipFace) (a b : ℤ) (wit : s.func a b > t.func a b) : (a, b) ∉ s.ess → ∃ (a' : ℤ) (b' : ℤ), (a', b') ∈ {(a - 1, b), (a + 1, b), (a, b - 1), (a, b + 1)} ∧ s.func a' b' > t.func a' b' ∧ s.func a b + s.dual.func b a < s.func a' b' + s.dual.func b' a'

Lemma 7.2 (lem:essSetMoves) of An extended Demazure product.

def LeanPool.DemazureProduct.SlipFace.isClifford (sf : SlipFace) : Prop

Definition 7.3 (defn:cliffordSF) of An extended Demazure product.

Equations

• sf.isClifford = ∃ (M : ℕ), ∀ (a b : ℤ), sf.func a b + sf.dual.func b a ≥ ↑M → sf.func a b = 0 ∨ sf.dual.func b a = 0

theorem LeanPool.DemazureProduct.SlipFace.ess_clifford (s t : SlipFace) (cliff : s.isClifford) : s ≤ t ↔ s.χ ≤ t.χ ∧ ∀ (a b : ℤ), (a, b) ∈ s.ess → s.func a b ≤ t.func a b