Documentation

LeanPool.BrillNoetherGraphs.Demazure.ReducedProducts

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.

source
theorem 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.

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

source
theorem 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.

source
theorem 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.

source
theorem 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.

source
theorem 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 #

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

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

Reduced factorizations #

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

Instances For
    source
    theorem ReducedFact.of_mul_reduced {α β γ : AspPerm} (h_mul : α * β = γ) (h_reduced : α.ReducedProduct β) :
    ReducedFact α β γ

    Construct a reduced fact from its defining two properties.

    source
    theorem 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.

    source
    theorem ReducedFact.of_ler_rres {α β γ : AspPerm} (h_ler : α ≤R γ) (h_rres : α⁻¹ ▹ γ = β) :
    ReducedFact α β γ
    source
    theorem ReducedFact.star_eq {α β γ : AspPerm} (h : ReducedFact α β γ) :
    α ⋆ β = γ

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

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

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