The bond of two weights related by a positive reflection

If two weights satisfy y = s_β x for a positive root β of a root pairing with a base, their bond is ⟨y, β^∨⟩ = -⟨x, β^∨⟩. For y ≠ x in a reduced root pairing the positive root β is unique (TauCeti.eq_of_isPos_of_reflection_eq), so the bond depends only on the two weights. For a cover y ⋖ x of the parabolic quotient W / W_λ, the bond of x λ and y λ is the positive cover bond b_λ(x, y) of Chirivì–Fang–Littelmann, studied in TauCeti.LinearAlgebra.RootSystem.Weyl.CoverBond.

Main definitions

• RootPairing.reflectionBond is the bond ⟨y, β^∨⟩ = -⟨x, β^∨⟩ of two weights with y = s_β x for a positive root β.

Main results

• RootPairing.reflectionBond_eq_coroot' and RootPairing.reflectionBond_eq_neg_coroot' compute the bond in terms of any positive root label.
• RootPairing.reflectionBond_eq_zero_of_not_exists says the bond of two weights not related by a positive reflection is 0, and RootPairing.reflectionBond_self says the bond of a weight with itself is 0.
• RootPairing.reflectionBond_reflection: the bond of x and s_β x is -⟨x, β^∨⟩.
• RootPairing.reflectionBond_dvd_sub: when y = s_β x for a positive root β, the bond of x and y divides f x - f y for every linear form f.
• RootPairing.abs_reflectionBond_smul_smul: the bond is invariant under the Weyl group, up to sign.

References

R. Chirivì, X. Fang, P. Littelmann, LS algebras, valuations and Schubert varieties, arXiv:2203.12992, Definition 2.1.

noncomputable def RootPairing.reflectionBond {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (b : P.Base) (x y : M) : R

The bond of two weights related by a reflection in a positive root: if y = s_β x for a positive root β, it is ⟨y, β^∨⟩ = -⟨x, β^∨⟩. For y ≠ x and a reduced root pairing the positive root β is unique (TauCeti.eq_of_isPos_of_reflection_eq), so the bond is well defined (RootPairing.reflectionBond_eq_coroot'). If no reflection in a positive root sends x to y, the bond is 0. For a cover y ⋖ x of the parabolic quotient W / W_λ, the bond of x λ and y λ is the positive cover bond b_λ(x, y).

theorem RootPairing.reflectionBond_eq_coroot' {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} [P.IsReduced] {β : ι} (hβ : b.IsPos β) {x y : M} (h : (P.reflection β) x = y) (hne : y ≠ x) : P.reflectionBond b x y = (P.coroot' β) y

The bond of two weights related by a reflection in a positive root β is ⟨y, β^∨⟩.

theorem RootPairing.reflectionBond_eq_neg_coroot' {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} [P.IsReduced] {β : ι} (hβ : b.IsPos β) {x y : M} (h : (P.reflection β) x = y) (hne : y ≠ x) : P.reflectionBond b x y = -(P.coroot' β) x

The bond of two weights related by a reflection in a positive root β is -⟨x, β^∨⟩.

theorem RootPairing.reflectionBond_eq_zero_of_not_exists {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} {x y : M} (h : ¬∃ (β : ι), b.IsPos β ∧ (P.reflection β) x = y) : P.reflectionBond b x y = 0

The bond of two weights not related by any reflection in a positive root is 0.

@[simp]

theorem RootPairing.reflectionBond_self {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} [NoZeroDivisors R] (x : M) : P.reflectionBond b x x = 0

The bond of a weight with itself is 0: a reflection fixing x has a coroot vanishing on x.

theorem RootPairing.reflectionBond_reflection {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} [P.IsReduced] [NoZeroDivisors R] {β : ι} (hβ : b.IsPos β) (x : M) : P.reflectionBond b x ((P.reflection β) x) = -(P.coroot' β) x

The bond of a weight x and its reflection s_β x in a positive root β is -⟨x, β^∨⟩. This holds also when s_β x = x, where both sides vanish.

theorem RootPairing.reflectionBond_dvd_sub {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} [P.IsReduced] {β : ι} (hβ : b.IsPos β) {x y : M} (h : (P.reflection β) x = y) (f : Module.Dual R M) : P.reflectionBond b x y ∣ f x - f y

The bond divides the change of every linear form. If y = s_β x for a positive root β, then x - y = -⟨y, β^∨⟩ β, so the bond of x and y divides f x - f y for every linear form f.

theorem RootPairing.abs_reflectionBond_smul_smul {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} [LinearOrder R] [P.IsReduced] {β : ι} (hβ : b.IsPos β) {x y : M} (h : (P.reflection β) x = y) (hne : y ≠ x) (w : ↥P.weylGroup) : |P.reflectionBond b (w • x) (w • y)| = |P.reflectionBond b x y|

The bond is invariant under the Weyl group, up to sign. If y = s_β x ≠ x for a positive root β, then |b(w x, w y)| = |b(x, y)| for every element w of the Weyl group: w y is the reflection of w x in the root w β, of which either w β or -w β is positive.

theorem RootPairing.reflectionBond_smul {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} [IsDomain R] [P.IsReduced] (c : R) (x y : M) : P.reflectionBond b (c • x) (c • y) = c * P.reflectionBond b x y

Scaling both weights scales their reflection bond. The zero scalar is allowed.

theorem RootPairing.reflectionBond_smul_nsmul {ι : Type u} {M : Type w} {N : Type x} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (b : P.Base) [P.IsReduced] (n : ℕ) (lam : M) (x y : ↥P.weylGroup) : P.reflectionBond b (x • n • lam) (y • n • lam) = ↑n * P.reflectionBond b (x • lam) (y • lam)

Scaling the shape by a natural number multiplies each orbit bond by that number.

theorem RootPairing.reflectionBond_add_add {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} {b : P.Base} [P.IsReduced] [NoZeroDivisors R] {χ : M} (hχ : ∀ (i : ι), (P.coroot' i) χ = 0) (x y : M) : P.reflectionBond b (x + χ) (y + χ) = P.reflectionBond b x y

Translating by a weight on every wall leaves bonds unchanged. If every coroot vanishes on χ, as for a central weight, every reflection fixes χ, so s_β (x + χ) = y + χ exactly when s_β x = y, with the same pairing ⟨y + χ, β^∨⟩ = ⟨y, β^∨⟩.