Reduction theorems

This file formalizes the main theorems from the introduction of An extended Demazure product: Theorem B (thm:starGreedy) characterizes α ⋆ β as a greedy maximum, and Theorem C (thm:reduce) reduces inequalities α ⋆ β ≥ γ to equalities of reduced products. It corresponds roughly to Section 6 of the paper.

Bookkeeping helpers

theorem LeanPool.DemazureProduct.Reduction.star_left_witness (α β : AspPerm) : have α₁ := α ⋆ β * β⁻¹; α₁ * β = α ⋆ β ∧ α₁ ⋆ β = α ⋆ β ∧ α₁ ≤χ α

Multiplying α ⋆ β on the right by β⁻¹ recovers a permutation that lies weakly below α in Bruhat order, has the same shift as α, and whose product with β (ordinary or Demazure) returns α ⋆ β.

theorem LeanPool.DemazureProduct.Reduction.star_right_witness (α β : AspPerm) : have β₁ := α⁻¹ * (α ⋆ β); α * β₁ = α ⋆ β ∧ α ⋆ β₁ = α ⋆ β ∧ β₁ ≤χ β

Multiplying α ⋆ β on the left by α⁻¹ recovers a permutation that lies weakly below β in Bruhat order, has the same shift as β, and whose product with α (ordinary or Demazure) returns α ⋆ β.

theorem LeanPool.DemazureProduct.Reduction.mul_le_star_of_le {α₁ α₂ β₁ β₂ : AspPerm} (hα : α₁ ≤ α₂) (hβ : β₁ ≤ β₂) : α₁ * β₁ ≤ α₂ ⋆ β₂

The ordinary product of Bruhat-smaller factors lies below the Demazure product of the original factors. This is the ASP form of the bound used in the equation labeled eq:astarbBound in An extended Demazure product.

Theorem B: greedy characterization of ⋆

theorem LeanPool.DemazureProduct.Reduction.starGreedy_alpha (α β : AspPerm) : IsGreatest {x : AspPerm | ∃ (α₁ : AspPerm) (_ : α₁ ≤χ α), α₁ * β = x} (α ⋆ β)

Theorem B (thm:starGreedy) of An extended Demazure product, part 1/3, formula eq:starGreedyAlpha.

α ⋆ β is the Bruhat-maximum of the set $\{ \alpha_1 \beta : \alpha_1 \leq_\chi \alpha\}$.

theorem LeanPool.DemazureProduct.Reduction.starGreedy_beta (α β : AspPerm) : IsGreatest {x : AspPerm | ∃ (β₁ : AspPerm) (_ : β₁ ≤χ β), α * β₁ = x} (α ⋆ β)

Theorem B (thm:starGreedy) of An extended Demazure product, part 2/3, formula eq:starGreedyBeta.

α ⋆ β is the Bruhat-maximum of the set $\{ \alpha \beta_1 : \beta_1 \leq_\chi \beta\}$.

theorem LeanPool.DemazureProduct.Reduction.starGreedy (α β : AspPerm) : IsGreatest {x : AspPerm | ∃ (α₁ : AspPerm) (_ : α₁ ≤ α) (β₁ : AspPerm) (_ : β₁ ≤ β), α₁ * β₁ = x} (α ⋆ β)

Theorem B (thm:starGreedy) of An extended Demazure product, part 3/3, formula eq:starGreedy.

α ⋆ β is the Bruhat-maximum of the set $\{ \alpha_1 \beta_1 : \alpha_1 \leq \alpha, \beta_1 \leq \beta\}$.

Theorem C: reduction theorem for α ⋆ β ≥ γ

theorem LeanPool.DemazureProduct.Reduction.reduce_witness (α β γ : AspPerm) (h : α ⋆ β ≥ γ) : have α₁ := γ ◃ β⁻¹; have β₁ := α₁⁻¹ ▹ γ; α₁ * β₁ = γ ∧ α₁ ⋆ β₁ = γ ∧ α₁ ≤ α ∧ β₁ ≤ β

Theorem C (thm:reduce) of An extended Demazure product, second paragraph, Bruhat component, part 1/3.

If α ⋆ β ≥ γ, then α₁ = γ ◃ β⁻¹ and β₁ = α₁⁻¹ ▹ γ satisfy α₁ ⋆ β₁ = α₁ * β₁ = γ and α₁ ≤ α, β₁ ≤ β.

theorem LeanPool.DemazureProduct.Reduction.reduce_witness_chi (α β γ : AspPerm) (hχ : α.χ + β.χ = γ.χ) (h : α ⋆ β ≥ γ) : have α₁ := γ ◃ β⁻¹; have β₁ := α₁⁻¹ ▹ γ; α₁ * β₁ = γ ∧ α₁ ⋆ β₁ = γ ∧ α₁ ≤χ α ∧ β₁ ≤χ β

Theorem C (thm:reduce) of An extended Demazure product, second paragraph, including the shift identities, part 2/3. Under the additional hypothesis $\chi_\alpha + \chi_\beta = \chi_\gamma$ (which makes both shift equalities meaningful), we further have $\alpha_1 \leq_\chi \alpha$ and $\beta_1 \leq_\chi \beta$.

theorem LeanPool.DemazureProduct.Reduction.reduce (α β γ : AspPerm) (hχ : α.χ + β.χ = γ.χ) : α ⋆ β ≥ γ ↔ ∃ (α₁ : AspPerm) (β₁ : AspPerm), α₁ ≤χ α ∧ β₁ ≤χ β ∧ α₁ ⋆ β₁ = γ ∧ α₁ * β₁ = γ

Theorem C (thm:reduce) of An extended Demazure product, first paragraph, ASP form, part 3/3.

For all α, β, γ ∈ ASP with α.χ + β.χ = γ.χ, the inequality α ⋆ β ≥ γ is equivalent to the existence of α₁, β₁ with α₁ ≤χ α, β₁ ≤χ β, and α₁ ⋆ β₁ = α₁ * β₁ = γ.

Theorem 6.1 (resLStingy): stingy characterization of ◃

The dual story for ◃, mirroring Theorem B. This is the formula labeled eq:resLGreedyAlpha in An extended Demazure product.

theorem LeanPool.DemazureProduct.Reduction.lres_stingy_alpha (α β : AspPerm) : IsLeast {x : AspPerm | ∃ (α₁ : AspPerm) (_ : α ≤χ α₁), α₁ * β⁻¹ = x} (α ◃ β⁻¹)

Theorem 6.1 (thm:resLStingy) of An extended Demazure product, part 1/3, formula eq:resLGreedyAlpha.

α ◃ β⁻¹ is the Bruhat-minimum of the set $\{\alpha_1 \beta^{-1}: \alpha_1 \geq_\chi \alpha\}$.

theorem LeanPool.DemazureProduct.Reduction.lres_stingy_beta (α β : AspPerm) : IsLeast {x : AspPerm | ∃ (β₁ : AspPerm) (_ : β₁ ≤χ β), α * β₁⁻¹ = x} (α ◃ β⁻¹)

Theorem 6.1 (thm:resLStingy) of An extended Demazure product, part 2/3, formula eq:resLGreedyBeta.

α ◃ β⁻¹ is the Bruhat-minimum of the set $\{\alpha \beta_1^{-1}: \beta_1 \leq_\chi \beta\}$.

theorem LeanPool.DemazureProduct.Reduction.lres_stingy (α β : AspPerm) : IsLeast {x : AspPerm | ∃ (α₁ : AspPerm) (_ : α ≤ α₁) (β₁ : AspPerm) (_ : β₁ ≤ β), α₁ * β₁⁻¹ = x} (α ◃ β⁻¹)

Theorem 6.1 (thm:resLStingy) of An extended Demazure product, part 3/3, formula eq:resLGreedy.

α ◃ β⁻¹ is the Bruhat-minimum of the set $\{\alpha_1 \beta_1^{-1}: \alpha_1 \geq \alpha,\, \beta_1 \leq \beta\}$.

Theorem 6.5 (reduceSeveral): three- and many-fold reduction

The reduction theorem for products of three or more permutations follows from reduce by induction. The list form below packages that induction.

theorem LeanPool.DemazureProduct.Reduction.reduceList (αs : List AspPerm) (γ : AspPerm) : (List.map AspPerm.χ αs).sum = γ.χ → AspPerm.DProd αs ≥ γ → ∃ (βs : List AspPerm), List.Forall₂ (fun (α β : AspPerm) => β ≤χ α) αs βs ∧ AspPerm.DProd βs = γ ∧ AspPerm.OrdProd βs = γ

Theorem 6.5 (thm:reduceSeveral) of An extended Demazure product, ASP-level (list version).

For any list of permutations αs and a target γ ∈ ASP with matching total shift, if the Demazure product over αs is Bruhat-≥ γ, then there exists a list of "reduced witnesses" βs of the same length, with βᵢ ≤χ αᵢ pointwise, whose Demazure product and ordinary product both equal γ.