The Demazure product of a word

Let cs : CoxeterSystem M W be a Coxeter system. The Demazure product δ(ω) of a word ω = i₁ ⋯ iᵣ in the simple reflections is the product of its letters in the 0-Hecke monoid, where a simple reflection that would shorten the element is absorbed instead of multiplied:

δ([]) = 1, and δ(i :: ω) = δ(ω) if sᵢ is a left descent of δ(ω), sᵢ δ(ω) otherwise.

For a reduced word it is the ordinary product s_{i₁} ⋯ s_{iᵣ}. For an arbitrary word, reduced or not, Demazure showed that the Bott–Samelson variety of the word maps onto the Schubert variety of δ(ω), and that the composite of the Demazure operators of the letters is the Demazure operator of δ(ω). This file proves the combinatorial side of both statements; no variety is constructed here.

The combinatorial content of the first statement is the subword characterization: δ(ω) is the greatest element, in the Bruhat order, among the products π σ of the subwords σ of ω, and the Bruhat interval below δ(ω) consists exactly of those products (CoxeterSystem.bruhatLE_demazureProd_iff_exists_sublist_wordProd_eq). For a reduced word this is the subword property CoxeterSystem.bruhatLE_iff_exists_sublist_wordProd_eq. The second statement is the universal property of the 0-Hecke monoid: generators of any monoid satisfying the braid relations and f i * f i = f i have the same product along ω as along any reduced word for δ(ω) (CoxeterSystem.prod_map_eq_of_wordProd_eq_demazureProd). It extends Matsumoto's theorem TauCeti.matsumoto from reduced words to all words.

Main definitions

• CoxeterSystem.demazureProd: the Demazure product δ(ω) of a word ω.

Main results

• CoxeterSystem.demazureProd_cons_of_isLeftDescent, CoxeterSystem.demazureProd_cons_of_not_isLeftDescent and their right-hand counterparts CoxeterSystem.demazureProd_append_singleton_of_isRightDescent, CoxeterSystem.demazureProd_append_singleton_of_not_isRightDescent: the recursion on either end.
• CoxeterSystem.demazureProd_eq_wordProd_of_isReduced: on a reduced word, δ(ω) = π ω.
• CoxeterSystem.exists_sublist_isReduced_wordProd_eq_demazureProd: δ(ω) is spelled by a reduced subword of ω; hence CoxeterSystem.length_demazureProd_le, and CoxeterSystem.length_demazureProd_eq_length_iff: ℓ(δ(ω)) = |ω| exactly when ω is reduced.
• CoxeterSystem.bruhatLE_demazureProd_of_sublist: δ is monotone for the sublist order.
• CoxeterSystem.bruhatLE_demazureProd_iff_exists_sublist_wordProd_eq: the subword characterization, u ≤ δ(ω) exactly when some subword of ω spells u.
• CoxeterSystem.demazureProd_reverse: δ(ω.reverse) = δ(ω)⁻¹.
• CoxeterSystem.mul_prod_map_eq_of_isLeftDescent: a 0-Hecke generator f i is absorbed into the product along a reduced word whose element has sᵢ as a left descent.
• CoxeterSystem.prod_map_eq_of_wordProd_eq_demazureProd: the universal property of the 0-Hecke monoid.

References

• M. Demazure, Désingularisation des variétés de Schubert généralisées, Ann. Sci. École Norm. Sup. (4) 7 (1974).
• A. Knutson, E. Miller, Subword complexes in Coxeter groups, Adv. Math. 184 (2004), 161–176, Section 3.

noncomputable def CoxeterSystem.demazureProd {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : W

The Demazure product of a word ω in the simple reflections: the product of its letters in the 0-Hecke monoid. Reading the word from the right, a letter i multiplies the product w of the letters after it on the left by sᵢ, unless sᵢ is a left descent of w, in which case w is kept.

@[simp]

theorem CoxeterSystem.demazureProd_nil {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : cs.demazureProd [] = 1

@[simp]

theorem CoxeterSystem.demazureProd_cons_of_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {ω : List B} (h : cs.IsLeftDescent (cs.demazureProd ω) i) : cs.demazureProd (i :: ω) = cs.demazureProd ω

A letter i is absorbed when sᵢ is a left descent of the Demazure product of the rest.

@[simp]

theorem CoxeterSystem.demazureProd_cons_of_not_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {ω : List B} (h : ¬cs.IsLeftDescent (cs.demazureProd ω) i) : cs.demazureProd (i :: ω) = cs.simple i * cs.demazureProd ω

A letter i multiplies on the left when sᵢ is not a left descent of the Demazure product of the rest.

@[simp]

theorem CoxeterSystem.demazureProd_singleton {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.demazureProd [i] = cs.simple i

theorem CoxeterSystem.isLeftDescent_demazureProd_cons {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω : List B) : cs.IsLeftDescent (cs.demazureProd (i :: ω)) i

The first letter of a word is always a left descent of its Demazure product.

@[simp]

theorem CoxeterSystem.demazureProd_cons_cons_self {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω : List B) : cs.demazureProd (i :: i :: ω) = cs.demazureProd (i :: ω)

A repeated letter is absorbed: δ(i i ω) = δ(i ω).

theorem CoxeterSystem.demazureProd_eq_wordProd_of_isReduced {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : cs.IsReduced ω) : cs.demazureProd ω = cs.wordProd ω

The Demazure product of a reduced word is its product.

theorem CoxeterSystem.exists_sublist_isReduced_wordProd_eq_demazureProd {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : ∃ (σ : List B), σ.Sublist ω ∧ cs.IsReduced σ ∧ cs.wordProd σ = cs.demazureProd ω

The Demazure product is spelled by a reduced subword.

theorem CoxeterSystem.length_demazureProd_le {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : cs.length (cs.demazureProd ω) ≤ ω.length

The Demazure product of a word is no longer than the word.

theorem CoxeterSystem.length_demazureProd_eq_length_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} : cs.length (cs.demazureProd ω) = ω.length ↔ cs.IsReduced ω

The Demazure product of a word has the length of the word exactly when the word is reduced.

The Bruhat order

theorem CoxeterSystem.bruhatLE_demazureProd_cons {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω : List B) : cs.BruhatLE (cs.demazureProd ω) (cs.demazureProd (i :: ω))

Prepending a letter moves the Demazure product up in the Bruhat order.

theorem CoxeterSystem.bruhatLE_demazureProd_of_sublist {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {σ ω : List B} (h : σ.Sublist ω) : cs.BruhatLE (cs.demazureProd σ) (cs.demazureProd ω)

The Demazure product is monotone for the sublist order.

theorem CoxeterSystem.bruhatLE_wordProd_demazureProd {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : cs.BruhatLE (cs.wordProd ω) (cs.demazureProd ω)

The product of a word lies below its Demazure product.

theorem CoxeterSystem.bruhatLE_demazureProd_iff_exists_sublist_wordProd_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {u : W} {ω : List B} : cs.BruhatLE u (cs.demazureProd ω) ↔ ∃ (σ : List B), σ.Sublist ω ∧ cs.wordProd σ = u

The subword characterization of the Demazure product. An element lies below δ(ω) in the Bruhat order exactly when some subword of ω, reduced or not, spells it. Together with CoxeterSystem.exists_sublist_isReduced_wordProd_eq_demazureProd this says that δ(ω) is the greatest of the products of the subwords of ω.

@[simp]

theorem CoxeterSystem.demazureProd_reverse {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : cs.demazureProd ω.reverse = (cs.demazureProd ω)⁻¹

The Demazure product of the reversed word is the inverse.

@[simp]

theorem CoxeterSystem.demazureProd_append_singleton_of_isRightDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {ω : List B} (h : cs.IsRightDescent (cs.demazureProd ω) i) : cs.demazureProd (ω ++ [i]) = cs.demazureProd ω

A last letter i is absorbed when sᵢ is a right descent of the Demazure product of the rest.

@[simp]

theorem CoxeterSystem.demazureProd_append_singleton_of_not_isRightDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {ω : List B} (h : ¬cs.IsRightDescent (cs.demazureProd ω) i) : cs.demazureProd (ω ++ [i]) = cs.demazureProd ω * cs.simple i

A last letter i multiplies on the right when sᵢ is not a right descent of the Demazure product of the rest.

The universal property of the 0-Hecke monoid

theorem CoxeterSystem.mul_prod_map_eq_of_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_3} [Monoid G] (f : B → G) (hbraid : ∀ (i j : B), (List.map f (braidWord M i j)).prod = (List.map f (braidWord M j i)).prod) {i : B} (hidem : f i * f i = f i) {ω : List B} (hω : cs.IsReduced ω) (hi : cs.IsLeftDescent (cs.wordProd ω) i) : f i * (List.map f ω).prod = (List.map f ω).prod

A 0-Hecke generator absorbs into a product along a word it can start. Let f assign to each simple reflection an element of a monoid, satisfying the braid relations, and let f i * f i = f i. If ω is a reduced word and sᵢ is a left descent of π ω, then f i * f(ω) = f(ω): some reduced word for π ω starts with i.

theorem CoxeterSystem.prod_map_eq_of_wordProd_eq_demazureProd {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_3} [Monoid G] (f : B → G) (hbraid : ∀ (i j : B), (List.map f (braidWord M i j)).prod = (List.map f (braidWord M j i)).prod) (hidem : ∀ (i : B), f i * f i = f i) {ω σ : List B} (hσ : cs.IsReduced σ) (h : cs.wordProd σ = cs.demazureProd ω) : (List.map f ω).prod = (List.map f σ).prod

The universal property of the 0-Hecke monoid. Let f assign to each simple reflection an element of a monoid, satisfying the braid relations and f i * f i = f i. Then the product of f along an arbitrary word ω equals its product along any reduced word σ for the Demazure product δ(ω). For reduced ω this is Matsumoto's theorem TauCeti.matsumoto.