The interval bond gcd d_λ(x, y) of W / W_λ

Let λ be a dominant weight for a base of a finite reduced root datum, and let y ≤ x be minimal coset representatives of the stabilizer W_λ. Each saturated chain C : x = x₀ ⋗ x₁ ⋗ ⋯ ⋗ x_l = y of the parabolic quotient W / W_λ has a bond gcd d(C), the gcd of the bonds b_λ(x_{h-1}, x_h) of its covers (TauCeti.bondGcd). The main result of this file is that d(C) does not depend on the chain C, only on its ends. This defines the interval bond gcd d_λ(x, y) of Chirivì–Fang–Littelmann, with d_λ(x, x) = 0.

With it, Littelmann's a-chain condition becomes a condition on the pair (x, y) alone: writing a = p / q in lowest terms with q > 0, one saturated chain from x down to y is an a-chain exactly when q ∣ d_λ(x, y), exactly when every saturated chain from x down to y is an a-chain. So in the description of the Lakshmibai–Seshadri paths of shape λ, the existence of an a-chain at a break does not depend on which saturated chain is tested.

The proof is a chain-sorting induction on the length of x, along a left descent sᵢ of x. Two kinds of local moves compare chains. If z ⋖ x is a cover with z ≠ sᵢ x, then sᵢ is also a left descent of z and sᵢ z ⋖ sᵢ x, so the length-two interval from sᵢ z to x has the two intermediate elements z and sᵢ x. Its two chains have the same bond gcd: the bonds of z ⋖ x and sᵢ z ⋖ sᵢ x agree, since sᵢ carries the root label of one to that of the other, and the bonds |⟨x λ, αᵢ^∨⟩| and |⟨z λ, αᵢ^∨⟩| of sᵢ x ⋖ x and sᵢ z ⋖ z are congruent modulo it. Second, a chain x ⋗ sᵢ x ⋗ ⋯ ⋗ y with sᵢ y < y is compared with the chain obtained from its tail by appending sᵢ y ⋖ y: the two simple bonds |⟨x λ, αᵢ^∨⟩| and |⟨y λ, αᵢ^∨⟩| are congruent modulo the bond gcd of the tail, which divides ⟨sᵢ x λ - y λ, αᵢ^∨⟩ (TauCeti.bondGcd_dvd_sub). Every chain is moved by these steps onto one from sᵢ x to sᵢ y when sᵢ is a left descent of y, and onto one through sᵢ x when it is not; the lifting property of the Bruhat order provides the required comparisons.

Main definitions

• TauCeti.intervalBondGcd: the interval bond gcd d_λ(x, y), the bond gcd of any saturated chain of W / W_λ from x down to y, and 0 when there is none.

Main results

• TauCeti.bondGcd_eq_of_head_eq_of_last_eq and TauCeti.bondGcd_eq_intervalBondGcd: the bond gcd of a saturated chain of W / W_λ depends only on its ends.
• TauCeti.isAChain_iff_den_dvd_intervalBondGcd, TauCeti.exists_isAChain_iff_den_dvd_intervalBondGcd and TauCeti.forall_isAChain_iff_den_dvd_intervalBondGcd: some saturated chain from x down to y is an a-chain exactly when the denominator of a divides d_λ(x, y), exactly when every such chain is an a-chain.
• TauCeti.intervalBondGcd_self, TauCeti.intervalBondGcd_of_minimalCosetRepCovBy and TauCeti.intervalBondGcd_eq_gcd: d_λ(x, x) = 0, the interval gcd of a cover is its bond, and d_λ(x, z) = gcd(d_λ(x, y), d_λ(y, z)) for z ≤ y ≤ x.
• TauCeti.intervalBondGcd_eq_zero_iff and TauCeti.intervalBondGcd_eq_zero_of_not_bruhatLE: for minimal coset representatives y ≤ x, d_λ(x, y) = 0 exactly when x = y, and d_λ(x, y) = 0 unless y ≤ x; TauCeti.intervalBondGcd_eq_zero_of_not_isMinimalCosetRep_left and TauCeti.intervalBondGcd_eq_zero_of_not_isMinimalCosetRep_right: d_λ(x, y) = 0 unless both x and y are minimal coset representatives.

References

• R. Chirivì, X. Fang and P. Littelmann, LS algebras, valuations and Schubert varieties, arXiv:2203.12992, Definition 2.1 and Section 7.1.
• P. Littelmann, A Littlewood–Richardson rule for symmetrizable Kac–Moody algebras, Invent. Math. 116 (1994), 329--346, Section 4.
• V. V. Deodhar, Some characterizations of Bruhat ordering on a Coxeter group and determination of the relative Möbius function, Invent. Math. 39 (1977), 187--198.

Chain independence of the bond gcd

theorem TauCeti.bondGcd_eq_of_head_eq_of_last_eq {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] [P.flip.IsReduced] {lam : M} (hlam : lam ∈ P.dominantChamber b) {C C' : (weylCoxeterSystem P b).MinimalCosetRepChain (P.wallIndices b lam)} (hhead : RelSeries.head C = RelSeries.head C') (hlast : RelSeries.last C = RelSeries.last C') : bondGcd lam C = bondGcd lam C'

The bond gcd of a saturated chain of W / W_λ depends only on its ends. Two saturated chains from x down to y have the same bond gcd.

The interval bond gcd

noncomputable def TauCeti.intervalBondGcd {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} (b : P.Base) [Finite ι] [P.IsReduced] (lam : M) (x y : ↥P.weylGroup) : ℕ

The interval bond gcd d_λ(x, y) of minimal coset representatives y ≤ x of the stabilizer of λ: the bond gcd of any saturated chain of W / W_λ from x down to y. It does not depend on the chain (TauCeti.bondGcd_eq_intervalBondGcd), and d_λ(x, x) = 0. It is 0 unless y ≤ x are both minimal coset representatives of W_λ, that is when there is no saturated chain from x down to y.

theorem TauCeti.bondGcd_eq_intervalBondGcd {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] [P.flip.IsReduced] {lam : M} (hlam : lam ∈ P.dominantChamber b) (C : (weylCoxeterSystem P b).MinimalCosetRepChain (P.wallIndices b lam)) : bondGcd lam C = intervalBondGcd b lam ↑(RelSeries.head C) ↑(RelSeries.last C)

The bond gcd of a saturated chain of W / W_λ is the interval bond gcd of its ends.

@[simp]

theorem TauCeti.intervalBondGcd_self {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] {lam : M} (x : ↥P.weylGroup) : intervalBondGcd b lam x x = 0

The interval bond gcd d_λ(x, x) vanishes.

theorem TauCeti.intervalBondGcd_eq_zero_of_not_bruhatLE {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] {lam : M} {x y : ↥P.weylGroup} (h : ¬(weylCoxeterSystem P b).BruhatLE y x) : intervalBondGcd b lam x y = 0

The interval bond gcd d_λ(x, y) vanishes unless y ≤ x: then no saturated chain runs from x down to y.

theorem TauCeti.intervalBondGcd_eq_zero_of_not_isMinimalCosetRep_left {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] {lam : M} {x y : ↥P.weylGroup} (hx : ¬(weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) x) : intervalBondGcd b lam x y = 0

The interval bond gcd d_λ(x, y) vanishes unless x is a minimal coset representative of W_λ: then no saturated chain of W / W_λ starts at x.

theorem TauCeti.intervalBondGcd_eq_zero_of_not_isMinimalCosetRep_right {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] {lam : M} {x y : ↥P.weylGroup} (hy : ¬(weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) y) : intervalBondGcd b lam x y = 0

The interval bond gcd d_λ(x, y) vanishes unless y is a minimal coset representative of W_λ: then no saturated chain of W / W_λ ends at y.

theorem TauCeti.intervalBondGcd_eq_zero_iff {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] [P.flip.IsReduced] {lam : M} (hlam : lam ∈ P.dominantChamber b) {x y : ↥P.weylGroup} (hx : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) x) (hy : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) y) (hyx : (weylCoxeterSystem P b).BruhatLE y x) : intervalBondGcd b lam x y = 0 ↔ x = y

For minimal coset representatives y ≤ x, the interval bond gcd d_λ(x, y) vanishes exactly when x = y: the bonds of covers are positive.

theorem TauCeti.intervalBondGcd_of_minimalCosetRepCovBy {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] [P.flip.IsReduced] {lam : M} (hlam : lam ∈ P.dominantChamber b) {x y : ↥P.weylGroup} (h : (weylCoxeterSystem P b).MinimalCosetRepCovBy (P.wallIndices b lam) y x) : intervalBondGcd b lam x y = (P.reflectionBond b (x • lam) (y • lam)).natAbs

The interval bond gcd of a cover y ⋖ x of W / W_λ is its bond b_λ(x, y).

theorem TauCeti.intervalBondGcd_eq_gcd {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] [P.flip.IsReduced] {lam : M} (hlam : lam ∈ P.dominantChamber b) {x y z : ↥P.weylGroup} (hx : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) x) (hy : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) y) (hz : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) z) (hyx : (weylCoxeterSystem P b).BruhatLE y x) (hzy : (weylCoxeterSystem P b).BruhatLE z y) : intervalBondGcd b lam x z = (intervalBondGcd b lam x y).gcd (intervalBondGcd b lam y z)

The interval bond gcd of a concatenation. For minimal coset representatives z ≤ y ≤ x, d_λ(x, z) = gcd(d_λ(x, y), d_λ(y, z)).

The a-chain criterion

theorem TauCeti.isAChain_iff_den_dvd_intervalBondGcd {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] [P.flip.IsReduced] {lam : M} {a : ℚ} (hlam : lam ∈ P.dominantChamber b) {C : (weylCoxeterSystem P b).MinimalCosetRepChain (P.wallIndices b lam)} : IsAChain a lam C ↔ a.den ∣ intervalBondGcd b lam ↑(RelSeries.head C) ↑(RelSeries.last C)

A saturated chain is an a-chain exactly when the denominator of a divides the interval bond gcd of its ends.

theorem TauCeti.exists_isAChain_iff_den_dvd_intervalBondGcd {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] [P.flip.IsReduced] {lam : M} {a : ℚ} (hlam : lam ∈ P.dominantChamber b) {x y : ↥P.weylGroup} (hx : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) x) (hy : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) y) (hyx : (weylCoxeterSystem P b).BruhatLE y x) : (∃ (C : (weylCoxeterSystem P b).MinimalCosetRepChain (P.wallIndices b lam)), ↑(RelSeries.head C) = x ∧ ↑(RelSeries.last C) = y ∧ IsAChain a lam C) ↔ a.den ∣ intervalBondGcd b lam x y

Littelmann's a-chain condition depends only on the ends. For minimal coset representatives y ≤ x, there is an a-chain from x down to y exactly when the denominator of a divides d_λ(x, y).

theorem TauCeti.forall_isAChain_iff_den_dvd_intervalBondGcd {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] {P : RootPairing ι ℤ M N} {b : P.Base} [Finite ι] [P.IsReduced] [P.flip.IsReduced] {lam : M} {a : ℚ} (hlam : lam ∈ P.dominantChamber b) {x y : ↥P.weylGroup} (hx : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) x) (hy : (weylCoxeterSystem P b).IsMinimalCosetRep (P.wallIndices b lam) y) (hyx : (weylCoxeterSystem P b).BruhatLE y x) : (∀ (C : (weylCoxeterSystem P b).MinimalCosetRepChain (P.wallIndices b lam)), ↑(RelSeries.head C) = x → ↑(RelSeries.last C) = y → IsAChain a lam C) ↔ a.den ∣ intervalBondGcd b lam x y

Every saturated chain is an a-chain as soon as one is. For minimal coset representatives y ≤ x, every saturated chain from x down to y is an a-chain exactly when the denominator of a divides d_λ(x, y).