Documentation

TauCeti.LinearAlgebra.RootSystem.Weyl.Demazure.Basic

The integral Demazure operator of a root #

Let P be a root datum with weight lattice M, and write e^x for the basis element of the integral group algebra ℤ[M] at a weight x. For a root α = αᵢ with coroot α^∨, the Demazure operator Dᵢ : ℤ[M] → ℤ[M] is the ℤ-linear map sending e^x, where m = ⟨x, α^∨⟩, to the signed α-string

Geometrically, these strings are the torus characters of H⁰ - H¹ of the degree-m line bundle on the projective line Pᵢ/B, which is the role Dᵢ plays in computing Euler characteristics of line bundles on Bott–Samelson and Schubert varieties; this file treats only the combinatorial operator. Every case is the single localization identity

(1 - e^{-α}) Dᵢ(f) = f - e^{-α} sᵢ(f),

where sᵢ acts on ℤ[M] by reindexing along the reflection of M; that is, Dᵢ(e^x) = (e^x - e^{-α} e^{sᵢ x}) / (1 - e^{-α}).

Since 1 - e^{-α} is not a zero divisor in ℤ[M], the localization identity characterizes Dᵢ, and the remaining results follow from it algebraically: the image of Dᵢ is fixed by sᵢ, Dᵢ fixes exactly the sᵢ-invariant elements, so Dᵢ² = Dᵢ, and Dᵢ is linear over the sᵢ-invariant elements. In particular Dᵢ fixes every Weyl-invariant element.

Main definitions #

Main results #

References #

source
noncomputable def RootPairing.demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) :
AddMonoidAlgebra ℤ M →ₗ[ℤ] AddMonoidAlgebra ℤ M

The integral Demazure operator Dᵢ of the root αᵢ: the ℤ-linear endomorphism of ℤ[M] sending e^x, with m = ⟨x, αᵢ^∨⟩, to e^x + e^{x - αᵢ} + ⋯ + e^{x - m αᵢ} when m ≥ 0 and to -(e^{x + αᵢ} + ⋯ + e^{x + (-m - 1) αᵢ}) when m < 0. At most one of the two sums in the defining formula is nonempty.

Instances For
    source
    theorem RootPairing.demazureOperator_single {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) (x : M) (c : ℤ) :
    (P.demazureOperator i) (AddMonoidAlgebra.single x c) = c • (∑ j ∈ Finset.range ((P.coroot' i) x + 1).toNat, AddMonoidAlgebra.single (x - j • P.root i) 1 - ∑ j ∈ Finset.range (-(P.coroot' i) x - 1).toNat, AddMonoidAlgebra.single (x + (j + 1) • P.root i) 1)

    The defining formula of RootPairing.demazureOperator on a basis element.

    source
    theorem RootPairing.demazureOperator_single_of_coroot'_eq_natCast {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) {x : M} {n : ℕ} (h : (P.coroot' i) x = ↑n) :
    (P.demazureOperator i) (AddMonoidAlgebra.single x 1) = ∑ j ∈ Finset.range (n + 1), AddMonoidAlgebra.single (x - j • P.root i) 1

    On a weight x with ⟨x, αᵢ^∨⟩ = n ≥ 0, the Demazure operator is the root string e^x + e^{x - αᵢ} + ⋯ + e^{x - n αᵢ} from x down to sᵢ x.

    source
    theorem RootPairing.demazureOperator_single_of_coroot'_eq_neg_natCast_sub_one {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) {x : M} {n : ℕ} (h : (P.coroot' i) x = -↑n - 1) :
    (P.demazureOperator i) (AddMonoidAlgebra.single x 1) = -∑ j ∈ Finset.range n, AddMonoidAlgebra.single (x + (j + 1) • P.root i) 1

    On a weight x with ⟨x, αᵢ^∨⟩ = -n - 1 < 0, the Demazure operator is the negative of the root string e^{x + αᵢ} + ⋯ + e^{x + n αᵢ} strictly between x and sᵢ x.

    source
    @[simp]
    theorem RootPairing.demazureOperator_single_of_coroot'_eq_neg_one {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) {x : M} (h : (P.coroot' i) x = -1) :
    (P.demazureOperator i) (AddMonoidAlgebra.single x 1) = 0

    On a weight x with ⟨x, αᵢ^∨⟩ = -1, the Demazure operator vanishes.

    source
    @[simp]
    theorem RootPairing.demazureOperator_one {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) :
    (P.demazureOperator i) 1 = 1

    The Demazure operator fixes the unit e^0.

    The localization identity #

    source
    theorem RootPairing.one_sub_single_neg_root_mul_demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) (f : AddMonoidAlgebra ℤ M) :
    (1 - AddMonoidAlgebra.single (-P.root i) 1) * (P.demazureOperator i) f = f - AddMonoidAlgebra.single (-P.root i) 1 * (AddMonoidAlgebra.mapDomainRingEquiv ℤ (P.reflection i).toAddEquiv) f

    The localization identity of the Demazure operator: (1 - e^{-αᵢ}) Dᵢ(f) = f - e^{-αᵢ} sᵢ(f), where sᵢ reindexes ℤ[M] along the reflection of M. Equivalently, Dᵢ(e^x) = (e^x - e^{-αᵢ} e^{sᵢ x}) / (1 - e^{-αᵢ}).

    source
    theorem RootPairing.isLeftRegular_one_sub_single_neg_root {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) :
    IsLeftRegular (1 - AddMonoidAlgebra.single (-P.root i) 1)

    Multiplication by 1 - e^{-αᵢ} is injective on ℤ[M], since -αᵢ has infinite order.

    source
    theorem RootPairing.demazureOperator_eq_iff {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) {f g : AddMonoidAlgebra ℤ M} :
    (P.demazureOperator i) f = g ↔ (1 - AddMonoidAlgebra.single (-P.root i) 1) * g = f - AddMonoidAlgebra.single (-P.root i) 1 * (AddMonoidAlgebra.mapDomainRingEquiv ℤ (P.reflection i).toAddEquiv) f

    The localization identity characterizes the Demazure operator: Dᵢ f is the unique g with (1 - e^{-αᵢ}) g = f - e^{-αᵢ} sᵢ(f).

    Consequences of the localization identity #

    source
    @[simp]
    theorem RootPairing.mapDomainRingEquiv_reflection_demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) (f : AddMonoidAlgebra ℤ M) :
    (AddMonoidAlgebra.mapDomainRingEquiv ℤ (P.reflection i).toAddEquiv) ((P.demazureOperator i) f) = (P.demazureOperator i) f

    The image of the Demazure operator is fixed by the reflection sᵢ.

    source
    theorem RootPairing.coeff_reflection_demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) (f : AddMonoidAlgebra ℤ M) (x : M) :
    ((P.demazureOperator i) f).coeff ((P.reflection i) x) = ((P.demazureOperator i) f).coeff x

    The coefficients of the image of the Demazure operator are constant along the reflection sᵢ: the coefficient form of RootPairing.mapDomainRingEquiv_reflection_demazureOperator.

    source
    theorem RootPairing.demazureOperator_eq_self_iff {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) {f : AddMonoidAlgebra ℤ M} :
    (P.demazureOperator i) f = f ↔ (AddMonoidAlgebra.mapDomainRingEquiv ℤ (P.reflection i).toAddEquiv) f = f

    The Demazure operator fixes f exactly when f is fixed by the reflection sᵢ.

    source
    @[simp]
    theorem RootPairing.demazureOperator_demazureOperator {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) (f : AddMonoidAlgebra ℤ M) :
    (P.demazureOperator i) ((P.demazureOperator i) f) = (P.demazureOperator i) f

    The Demazure operator is idempotent, Dᵢ² = Dᵢ.

    source
    theorem RootPairing.demazureOperator_mul_of_reflection_eq {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) {g : AddMonoidAlgebra ℤ M} (hg : (AddMonoidAlgebra.mapDomainRingEquiv ℤ (P.reflection i).toAddEquiv) g = g) (f : AddMonoidAlgebra ℤ M) :
    (P.demazureOperator i) (g * f) = g * (P.demazureOperator i) f

    The Demazure operator is linear over the elements fixed by the reflection sᵢ.

    source
    theorem RootPairing.demazureOperator_eq_self_of_isWeylInvariant {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) (i : ι) {f : AddMonoidAlgebra ℤ M} (hf : TauCeti.IsWeylInvariant P f) :
    (P.demazureOperator i) f = f

    The Demazure operator fixes every Weyl-invariant element.