Reduced products

This file compares the Demazure operations with ordinary multiplication on ASP permutations. It corresponds roughly to Section 5 of An extended Demazure product.

Reduced products and ordinary products

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

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

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

theorem LeanPool.DemazureProduct.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) of An extended Demazure product, part 2/2.

theorem LeanPool.DemazureProduct.ReducedProducts.lres_le_mul (α β : AspPerm) : α ◃ β ≤ α * β

Left residual lies below ordinary multiplication in Bruhat order. Lemma 5.2 (lem:reducedRes) of An extended Demazure product, part 1/4.

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

Left residual 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:reducedRes) of An extended Demazure product, part 2/4.

theorem LeanPool.DemazureProduct.ReducedProducts.rres_le_mul (α β : AspPerm) : α ▹ β ≤ α * β

Right residual lies below ordinary multiplication in Bruhat order. Lemma 5.2 (lem:reducedRes) of An extended Demazure product, part 3/4.

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

Right residual 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:reducedRes) of An extended Demazure product, part 4/4.

Weak order implies strong order

theorem LeanPool.DemazureProduct.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) of An extended Demazure product, part 1/2.

theorem LeanPool.DemazureProduct.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) of An extended Demazure product, part 2/2.

Reduced factorizations

structure LeanPool.DemazureProduct.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 : α * β = γ

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

Construct a reduced fact from its defining two properties.

theorem LeanPool.DemazureProduct.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.

theorem LeanPool.DemazureProduct.ReducedFact.of_ler_rres {α β γ : AspPerm} (h_ler : α ≤R γ) (h_rres : α⁻¹ ▹ γ = β) : ReducedFact α β γ

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

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

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

Left residual by the inverse right factor collapses to ordinary multiplication in a reduced factorization.