Documentation

TauCeti.LinearAlgebra.RootSystem.Weyl.Demazure.Braid

Braid relations for the Demazure operators #

Let P be a root datum with weight lattice M, and let Dᵢ be the integral Demazure operator of the root αᵢ on ℤ[M] (RootPairing.demazureOperator). This file proves that the Demazure operators of two roots satisfy the braid relation of the dihedral group they generate: for roots αᵢ, αⱼ with Cartan entries ⟨αᵢ, αⱼ^∨⟩ = -1 and ⟨αⱼ, αᵢ^∨⟩ = -k (k = 1, 2, 3), the two alternating products of Dᵢ and Dⱼ of length 3, 4, 6 agree, and orthogonal roots give commuting operators. For the simple roots of a base these are exactly the braid relations of the Coxeter matrix of the base, so by Matsumoto's theorem the product D_{i₁} ⋯ D_{iᵣ} along a reduced word depends only on the Weyl group element s_{i₁} ⋯ s_{iᵣ}. This word independence is what makes D_w = D_{i₁} ⋯ D_{iᵣ} a well-defined operator for each Weyl group element w, the operator in the Demazure character formula char H⁰(X(w), L_λ) = D_w(e^λ).

Method #

Write a = e^{-αᵢ}, b = e^{-αⱼ} and sᵢ, sⱼ for the reindexing of ℤ[M] along the two reflections. Let w₀ be the longest element of the rank-two Weyl group ⟨sᵢ, sⱼ⟩ and Δ the product of the factors 1 - e^{-β} over its positive roots β (those of the rank-two subsystem with simple roots αᵢ, αⱼ). For either reduced word of w₀ the operator D_{w₀} satisfies Demazure's formula

Δ · D_{w₀}(f) = ∑_{w ∈ ⟨sᵢ, sⱼ⟩} (-1)^{ℓ(w)} e^{w ρ - ρ} w(f),

where ρ is the half sum of those positive roots; only the differences w ρ - ρ, which lie in the root lattice, occur. The right-hand side does not depend on the word. Each instance is derived from the localization identity (1 - e^{-αₖ}) Dₖ(g) = g - e^{-αₖ} sₖ(g) of TauCeti.LinearAlgebra.RootSystem.Weyl.Demazure.Basic, transported by the reflections already applied, and from the invariance sₖ(Dₖ g) = Dₖ g: peeling off the operators from the outside in, the coefficient of each term w(Dₖ g) is divisible by 1 - e^{-w αₖ} with w αₖ positive, and the resulting linear_combination certificate is checked by ring. Since multiplication by 1 - e^{-β} is injective (RootPairing.isLeftRegular_one_sub_single_neg_root), the two words give the same operator. No rank-two root system needs to be classified: the computation only uses the two Cartan entries.

Main results #

References #

Matsumoto's theorem is TauCeti.matsumoto.

The localization identity transported by a ring automorphism #

Demazure's formula for the longest element of a rank-two subsystem #

Each lemma below proves Δ · D_{w₀}(f) = ∑ (-1)^{ℓ(w)} e^{w ρ - ρ} w(f) for one reduced word of w₀, with a = e^{-αᵢ}, b = e^{-αⱼ}, S = sᵢ, T = sⱼ. Writing the word as D_{k₁}(D_{k₂}(⋯ D_{k_m}(f))), the hypothesis hₙ is the localization identity of one operator D_{k_l}, transported by the product w of reflections that multiplies it after the outer operators have been expanded: (1 - e^{-w α_{k_l}}) w(D_{k_l} g) = w(g) - e^{-w α_{k_l}} w(s_{k_l} g). The linear_combination coefficient of hₙ is the coefficient of w(D_{k_l} g) at that stage divided by 1 - e^{-w α_{k_l}}; the simp only [iS, iT] step uses sₖ(Dₖ g) = Dₖ g to merge the terms w sₖ(Dₖ g) and w(Dₖ g).

The braid relations #

source
theorem RootPairing.commute_demazureOperator_of_isOrthogonal {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) {i j : ι} (h : P.IsOrthogonal i j) :
Commute (P.demazureOperator i) (P.demazureOperator j)

The Demazure operators of orthogonal roots commute.

source
theorem RootPairing.demazureOperator_braid_three {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) {i j : ι} (hij : P.pairing i j = -1) (hji : P.pairing j i = -1) :
P.demazureOperator i * P.demazureOperator j * P.demazureOperator i = P.demazureOperator j * P.demazureOperator i * P.demazureOperator j

The braid relation of length three for the Demazure operators of two roots with Cartan entries -1 and -1, the A₂ configuration: Dᵢ Dⱼ Dᵢ = Dⱼ Dᵢ Dⱼ.

source
theorem RootPairing.demazureOperator_braid_four {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) {i j : ι} (hij : P.pairing i j = -1) (hji : P.pairing j i = -2) :
P.demazureOperator i * P.demazureOperator j * P.demazureOperator i * P.demazureOperator j = P.demazureOperator j * P.demazureOperator i * P.demazureOperator j * P.demazureOperator i

The braid relation of length four for the Demazure operators of two roots with Cartan entries ⟨αᵢ, αⱼ^∨⟩ = -1 and ⟨αⱼ, αᵢ^∨⟩ = -2, the B₂ configuration: Dᵢ Dⱼ Dᵢ Dⱼ = Dⱼ Dᵢ Dⱼ Dᵢ.

source
theorem RootPairing.demazureOperator_braid_six {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) {i j : ι} (hij : P.pairing i j = -1) (hji : P.pairing j i = -3) :
P.demazureOperator i * P.demazureOperator j * P.demazureOperator i * P.demazureOperator j * P.demazureOperator i * P.demazureOperator j = P.demazureOperator j * P.demazureOperator i * P.demazureOperator j * P.demazureOperator i * P.demazureOperator j * P.demazureOperator i

The braid relation of length six for the Demazure operators of two roots with Cartan entries ⟨αᵢ, αⱼ^∨⟩ = -1 and ⟨αⱼ, αᵢ^∨⟩ = -3, the G₂ configuration: (Dᵢ Dⱼ)³ = (Dⱼ Dᵢ)³.

The braid relations of a base and word independence #

source
theorem RootPairing.prod_map_demazureOperator_braidWord {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) (k l : ↥b.support) :
(List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) (CoxeterSystem.braidWord (TauCeti.coxeterMatrixOfBase P b) k l)).prod = (List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) (CoxeterSystem.braidWord (TauCeti.coxeterMatrixOfBase P b) l k)).prod

The Demazure operators of the simple roots of a base satisfy the braid relations of its Coxeter matrix: for simple roots αₖ, αₗ with Coxeter entry m, the two alternating products of Dₖ and Dₗ of length m agree.

source
theorem RootPairing.prod_map_demazureOperator_eq_of_wordProd_eq {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced] {ω ω' : List ↥b.support} (hω : (TauCeti.weylCoxeterSystem P b).IsReduced ω) (hω' : (TauCeti.weylCoxeterSystem P b).IsReduced ω') (h : (TauCeti.weylCoxeterSystem P b).wordProd ω = (TauCeti.weylCoxeterSystem P b).wordProd ω') :
(List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω).prod = (List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω').prod

Word independence of the Demazure operators: the product D_{k₁} ⋯ D_{kᵣ} of the Demazure operators along a reduced word in the simple reflections of a base depends only on the element s_{k₁} ⋯ s_{kᵣ} of the Weyl group that the word spells.

source
theorem RootPairing.demazureOperator_mul_prod_map_demazureOperator_of_isLeftDescent {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced] {ω : List ↥b.support} (hω : (TauCeti.weylCoxeterSystem P b).IsReduced ω) {i : ↥b.support} (hi : (TauCeti.weylCoxeterSystem P b).IsLeftDescent ((TauCeti.weylCoxeterSystem P b).wordProd ω) i) :
P.demazureOperator ↑i * (List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω).prod = (List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω).prod

A Demazure operator absorbs into a product along a word it can start. If ω is a reduced word and sᵢ is a left descent of w = s_{k₁} ⋯ s_{kᵣ}, then Dᵢ D_{k₁} ⋯ D_{kᵣ} = D_{k₁} ⋯ D_{kᵣ}: some reduced word for w starts with i, and Dᵢ² = Dᵢ.

source
theorem RootPairing.prod_map_demazureOperator_eq_of_wordProd_eq_demazureProd {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced] {ω ν : List ↥b.support} (hν : (TauCeti.weylCoxeterSystem P b).IsReduced ν) (h : (TauCeti.weylCoxeterSystem P b).wordProd ν = (TauCeti.weylCoxeterSystem P b).demazureProd ω) :
(List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ω).prod = (List.map (fun (m : ↥b.support) => P.demazureOperator ↑m) ν).prod

Word independence along arbitrary words. For any word ω in the simple reflections of a base, reduced or not, the product D_{i₁} ⋯ D_{iᵣ} of the Demazure operators along ω equals their product along any reduced word ν for the Demazure product δ(ω) (CoxeterSystem.demazureProd). So D_{i₁} ⋯ D_{iᵣ} = D_{δ(ω)}, the Demazure operator of a single Weyl group element.