Reduced Products and Ordinary Products

This file formalizes Section 5 of the paper, comparing the Demazure operations ⋆, ◃, and ▹ with ordinary multiplication on AspPerm.

noncomputable def ReducedProducts.star_hi_error (α β : AspPerm) (a b l : ℤ) : Finset ℤ

The part of $s_\alpha(a,\ell)$ coming from indices above $\ell$ whose preimages under $\beta$ lie below $b$.

Equations

• ReducedProducts.star_hi_error α β a b l = {n ∈ α.se_finset a l | β⁻¹.func n < b}

noncomputable def ReducedProducts.star_lo_error (α β : AspPerm) (a b l : ℤ) : Finset ℤ

The part of $s_\beta(\ell,b)$ coming from indices below $\ell$ whose images under $\alpha$ lie above $a$.

Equations

• ReducedProducts.star_lo_error α β a b l = {n ∈ β⁻¹.nw_finset b l | a ≤ α.func n}

@[simp]

theorem ReducedProducts.mem_star_hi_error (α β : AspPerm) (a b l n : ℤ) : n ∈ star_hi_error α β a b l ↔ l ≤ n ∧ α.func n < a ∧ β⁻¹.func n < b

@[simp]

theorem ReducedProducts.mem_star_lo_error (α β : AspPerm) (a b l n : ℤ) : n ∈ star_lo_error α β a b l ↔ n < l ∧ b ≤ β⁻¹.func n ∧ a ≤ α.func n

theorem ReducedProducts.star_sum_eq_mul_add_errors (α β : AspPerm) (a b l : ℤ) : α.s a l + β.s l b = (α * β).s a b + ↑(star_hi_error α β a b l).card + ↑(star_lo_error α β a b l).card

The two nonnegative error terms in the product-counting formula for Lemma 5.1. This is the paper's partition of $s_\alpha(a,\ell) + s_\beta(\ell,b)$ into the ordinary-product count $s_{\alpha\beta}(a,b)$ and the two remaining quadrants.

Proof component for Lemma 5.1 (lem:reducedStar).

theorem ReducedProducts.mul_le_star (α β : AspPerm) : α * β ≤ α ⋆ β

An ordinary product lies below the corresponding Demazure product in Bruhat order. Lemma 5.1 (lem:reducedStar), part 1/2.

theorem ReducedProducts.reducedProduct_of_star_le_mul (α β : AspPerm) (hupper : α ⋆ β ≤ α * β) : α.ReducedProduct β

If the Demazure product lies below the ordinary product, then the ordinary product is reduced. Proof component for Lemma 5.1 (lem:reducedStar).

theorem ReducedProducts.star_le_mul_of_reducedProduct (α β : AspPerm) (h_reduced : α.ReducedProduct β) : α ⋆ β ≤ α * β

A reduced ordinary product is an upper bound for the Demazure product. Proof component for Lemma 5.1 (lem:reducedStar).

theorem ReducedProducts.star_eq_mul_iff_reducedProduct (α β : AspPerm) : α ⋆ β = α * β ↔ α.ReducedProduct β

The Demazure product agrees with ordinary multiplication exactly for a reduced product. Lemma 5.1 (lem:reducedStar), part 2/2.

noncomputable def ReducedProducts.lc_lo_error (α β : AspPerm) (a b l : ℤ) : Finset ℤ

The left-contraction error below the cutoff $\ell$: indices counted by $s_{\alpha\beta}(a,b)$ but omitted from the candidate $s_\alpha(a,\ell)-s_{\beta^{-1}}(b,\ell)$.

Equations

• ReducedProducts.lc_lo_error α β a b l = {n ∈ β⁻¹.nw_finset b l | α.func n < a}

noncomputable def ReducedProducts.lc_hi_error (α β : AspPerm) (a b l : ℤ) : Finset ℤ

The left-contraction error above the cutoff $\ell$: indices subtracted by $s_{\beta^{-1}}(b,\ell)$ but not counted by $s_\alpha(a,\ell)$.

Equations

• ReducedProducts.lc_hi_error α β a b l = {n ∈ β⁻¹.se_finset b l | a ≤ α.func n}

@[simp]

theorem ReducedProducts.mem_lc_lo_error (α β : AspPerm) (a b l n : ℤ) : n ∈ lc_lo_error α β a b l ↔ n < l ∧ b ≤ β⁻¹.func n ∧ α.func n < a

@[simp]

theorem ReducedProducts.mem_lc_hi_error (α β : AspPerm) (a b l n : ℤ) : n ∈ lc_hi_error α β a b l ↔ l ≤ n ∧ β⁻¹.func n < b ∧ a ≤ α.func n

theorem ReducedProducts.lc_diff_eq_mul_sub_errors (α β : AspPerm) (a b l : ℤ) : α.s a l - β⁻¹.s b l = (α * β).s a b - ↑(lc_lo_error α β a b l).card - ↑(lc_hi_error α β a b l).card

The two nonnegative error terms in the left-contraction counting formula for Lemma 5.2. The paper's candidate $s_\alpha(a,\ell)-s_{\beta^{-1}}(b,\ell)$ is the ordinary-product count $s_{\alpha\beta}(a,b)$ minus these two errors.

Proof component for Lemma 5.2 (lem:reducedTri).

theorem ReducedProducts.left_contract_le_mul (α β : AspPerm) : α ◃ β ≤ α * β

Left contraction lies below ordinary multiplication in Bruhat order. Lemma 5.2 (lem:reducedTri), part 1/4.

theorem ReducedProducts.le_weak_L_of_mul_le_left_contract (α β : AspPerm) (hle : α * β ≤ α ◃ β) : β⁻¹ ≤L α

If ordinary multiplication lies below left contraction, then the inverse of the right factor lies below the left factor in left weak order. Proof component for Lemma 5.2 (lem:reducedTri).

theorem ReducedProducts.mul_le_left_contract_of_le_weak_L (α β : AspPerm) (hweak : β⁻¹ ≤L α) : α * β ≤ α ◃ β

If the inverse of the right factor lies below the left factor in left weak order, then ordinary multiplication lies below left contraction. Proof component for Lemma 5.2 (lem:reducedTri).

theorem ReducedProducts.left_contract_eq_mul_iff (α β : AspPerm) : α ◃ β = α * β ↔ β⁻¹ ≤L α

Left contraction agrees with ordinary multiplication exactly when the inverse of the right factor is below the left factor in left weak order. Lemma 5.2 (lem:reducedTri), part 2/4.

theorem ReducedProducts.right_contract_le_mul (α β : AspPerm) : α ▹ β ≤ α * β

Right contraction lies below ordinary multiplication in Bruhat order. Lemma 5.2 (lem:reducedTri), part 3/4.

theorem ReducedProducts.right_contract_eq_mul_iff (α β : AspPerm) : α ▹ β = α * β ↔ α⁻¹ ≤R β

Right contraction agrees with ordinary multiplication exactly when the inverse of the left factor is below the right factor in right weak order. Lemma 5.2 (lem:reducedTri), part 4/4.

Weak order implies strong order

theorem ReducedProducts.le_of_le_weak_L_of_chi_le {α β : AspPerm} (hweak : α ≤L β) (hχ : α.χ ≤ β.χ) : α ≤ β

Left weak order implies Bruhat order when the shifts are weakly ordered. Corollary 5.3 (cor:weakStrong), part 1/2.

theorem ReducedProducts.le_of_le_weak_R_of_chi_le {α β : AspPerm} (hweak : α ≤R β) (hχ : α.χ ≤ β.χ) : α ≤ β

Right weak order implies Bruhat order when the shifts are weakly ordered. Corollary 5.3 (cor:weakStrong), part 2/2.

Reduced Factorizations

structure ReducedFact (α β γ : AspPerm) : Prop

A reduced factorization of γ into the ordinary product of α and β.

This bundles the ordinary-product equality with reducedness so that the other equivalent descriptions from Section 5 can be recovered from one object.

• reduced : α.ReducedProduct β
• mul_eq : α * β = γ

def ReducedFact.of_mul_reduced {α β γ : AspPerm} (h_mul : α * β = γ) (h_reduced : α.ReducedProduct β) : ReducedFact α β γ

Construct a reduced fact from its defining two properties.

Equations

• ⋯ = ⋯

def ReducedFact.of_mul_star {α β γ : AspPerm} (h_mul : α * β = γ) (h_star : α ⋆ β = γ) : ReducedFact α β γ

Construct a reduced fact when ordinary and Demazure multiplication have the same value.

Equations

• ⋯ = ⋯

def ReducedFact.of_mul_ler {α β γ : AspPerm} (h_mul : α * β = γ) (h_weak : α ≤R γ) : ReducedFact α β γ

Construct a reduced fact from an ordinary product and the right weak-order inequality for its left factor.

Equations

• ⋯ = ⋯

def ReducedFact.of_mul_lel {α β γ : AspPerm} (h_mul : α * β = γ) (h_weak : β ≤L γ) : ReducedFact α β γ

Construct a reduced fact from an ordinary product and the left weak-order inequality for its right factor.

Equations

• ⋯ = ⋯

def ReducedFact.of_mul_rc {α β γ : AspPerm} (h_mul : α * β = γ) (h_contract : α⁻¹ ▹ γ = α⁻¹ * γ) : ReducedFact α β γ

Construct a reduced fact when the right contraction by the inverse left factor collapses to ordinary multiplication.

Equations

• ⋯ = ⋯

def ReducedFact.of_mul_lc {α β γ : AspPerm} (h_mul : α * β = γ) (h_contract : γ ◃ β⁻¹ = γ * β⁻¹) : ReducedFact α β γ

Construct a reduced fact when the left contraction by the inverse right factor collapses to ordinary multiplication.

Equations

• ⋯ = ⋯

def ReducedFact.of_reduced_star {α β γ : AspPerm} (h_red : α.ReducedProduct β) (h_star : α ⋆ β = γ) : ReducedFact α β γ

Equations

• ⋯ = ⋯

def ReducedFact.of_lel_rc {α β γ : AspPerm} (h_lel : β ≤L γ) (h_lc : γ ◃ β⁻¹ = α) : ReducedFact α β γ

Equations

• ⋯ = ⋯

def ReducedFact.of_ler_lc {α β γ : AspPerm} (h_ler : α ≤R γ) (h_rc : α⁻¹ ▹ γ = β) : ReducedFact α β γ

Equations

• ⋯ = ⋯

theorem ReducedFact.star_eq {α β γ : AspPerm} (h : ReducedFact α β γ) : α ⋆ β = γ

The Demazure product in a reduced fact has the same value as its ordinary product.

theorem ReducedFact.ler {α β γ : AspPerm} (h : ReducedFact α β γ) : α ≤R γ

The left factor of a reduced fact is below the product in right weak order.

theorem ReducedFact.lel {α β γ : AspPerm} (h : ReducedFact α β γ) : β ≤L γ

The right factor of a reduced fact is below the product in left weak order.

theorem ReducedFact.rc_eq {α β γ : AspPerm} (h : ReducedFact α β γ) : α⁻¹ ▹ γ = α⁻¹ * γ

Right contraction by the inverse left factor collapses to ordinary multiplication in a reduced fact.

theorem ReducedFact.lc_eq {α β γ : AspPerm} (h : ReducedFact α β γ) : γ ◃ β⁻¹ = γ * β⁻¹

Left contraction by the inverse right factor collapses to ordinary multiplication in a reduced fact.