Documentation

TauCeti.Algebra.Lie.HighestWeight.CentralCharacter.Injective

The Harish-Chandra projection is injective #

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of characteristic zero, H a splitting Cartan subalgebra and b a base of its root system. This file proves that the Harish-Chandra projection TauCeti.hcProjection b : Z(U(L)) →ₐ[K] S(H) is injective (TauCeti.hcProjection_injective), and so is its linear normalization TauCeti.hcProjectionLinear b (TauCeti.hcProjectionLinear_injective).

More precisely, the projection matches the PBW filtration of the centre with the degree filtration of S(H) exactly: a central element z has PBW degree at most n if and only if its projection has degree at most n (TauCeti.hcProjection_mem_wordFiltration_iff). One direction is TauCeti.hcProjection_mem_wordFiltration. For the other, it suffices to show that the degree of a central element z drops below m once its projection does. Let p ∈ S^m(L) be the PBW symbol of z; it is a Lie invariant (TauCeti.UniversalEnvelopingAlgebra.mem_lieInvariants_of_pbwHomogeneousComponentMap_eq_mk), so its symmetrization s is central and agrees with z up to degree below m. The projection of s is the Chevalley restriction of p up to degree below m (TauCeti.hcProjection_sub_lieCartanRestriction_mem_wordFiltrationPrevious), so the restriction of p, which is homogeneous of degree m, has degree below m and therefore vanishes. Chevalley's restriction theorem is injective on the invariants (LieSubalgebra.lieCartanRestriction_injOn_lieInvariants), so p = 0 and z has degree below m.

Injectivity is one half of the Harish-Chandra isomorphism Z(U(L)) ≃ S(H)^{W·}, the other being that the projection is onto the dot-invariants (TauCeti.range_hcProjection, over an algebraically closed field). Since the projection records the central characters χ_λ, a central element is determined by its central characters (TauCeti.eq_of_forall_vermaCentralCharacter_eq).

Main results #

References #

source
@[simp]
theorem TauCeti.hcProjection_mem_wordFiltration_iff {K : Type} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {n : ℕ} {z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))} :
(hcProjection b) z ∈ Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n ↔ ↑z ∈ UniversalEnvelopingAlgebra.pbwFiltration K L n

The Harish-Chandra projection detects the PBW degree: a central element has PBW degree at most n exactly when its Harish-Chandra projection has degree at most n in S(H).

source
@[simp]
theorem TauCeti.hcProjection_mem_wordFiltrationPrevious_iff {K : Type} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {n : ℕ} {z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))} :
(hcProjection b) z ∈ Algebra.wordFiltrationPrevious (SymmetricAlgebra.ι K ↥H) n ↔ ↑z ∈ UniversalEnvelopingAlgebra.pbwFiltrationPrevious K L n

The Harish-Chandra projection detects the strict PBW degree: a central element has PBW degree below n exactly when its Harish-Chandra projection has degree below n in S(H).

source
theorem TauCeti.hcProjection_injective {K : Type} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) :
Function.Injective ⇑(hcProjection b)

The Harish-Chandra projection is injective: a central element of U(L) is determined by its Harish-Chandra projection.

source
theorem TauCeti.eq_of_forall_vermaCentralCharacter_eq {K : Type} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {z w : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))} (h : ∀ (lam : Module.Dual K ↥H), (vermaCentralCharacter b lam) z = (vermaCentralCharacter b lam) w) :
z = w

A central element is determined by its central characters: if χ_lam(z) = χ_lam(w) for every weight lam, then z = w.

source
@[simp]
theorem TauCeti.hcProjectionLinear_mem_wordFiltration_iff {K : Type} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {n : ℕ} {z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))} :
(hcProjectionLinear b) z ∈ Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n ↔ ↑z ∈ UniversalEnvelopingAlgebra.pbwFiltration K L n

The linear Harish-Chandra projection detects the PBW degree: a central element has PBW degree at most n exactly when its linear Harish-Chandra projection has degree at most n.

source
theorem TauCeti.hcProjectionLinear_injective {K : Type} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) :
Function.Injective ⇑(hcProjectionLinear b)

The linear Harish-Chandra projection is injective.