Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Harish-Chandra isomorphism for the center

Statement

The shifted Harish-Chandra map

HCρ ⁣:Z(U(g))S(h)W,HCρ(z)(λ)=pr(z)(λρ),

is an algebra isomorphism.

Facts & Assumptions

Given: The shifted Harish-Chandra map HCρ(z)(λ):=pr(z)(λρ) on the center of U(g).

[F1]

The Harish-Chandra projection is multiplicative on the center (The Harish-Chandra projection is multiplicative on the center).

[F2]

The leading PBW symbol of a central element is invariant, and Chevalley restriction identifies symmetric invariants on g with Weyl invariants on h (The leading PBW symbol of a central element is invariant, Chevalley restriction for symmetric invariants).

Proof

technique · direct
1.1

Let fz(μ):=pr(z)(μ) for zZ(U(g)). Multiplicativity from [F1] shows that HCρ(z)(λ)=fz(λρ) defines an algebra homomorphism. To identify its image, fix a simple reflection si and a weight μ with μ+ρ,αi=mZ>0. In the cyclic highest-weight quotient generated by a highest vector vμ, the standard rank-one sl2 calculation gives eifimvμ=0, so fimvμ is a highest-weight vector of weight siμ. Because z is central, it acts by one scalar on the whole module, and The Harish-Chandra projection computes the highest-weight scalar therefore gives fz(μ)=fz(siμ). These weights are Zariski dense, so fz is invariant under the dot action of every simple reflection, hence under W. By The rho-shift intertwines the dot and ordinary Weyl actions, HCρ(z) lies in S(h)W.

F1given
2.1

The PBW filtration on U(g) induces a filtration on the center, and the Harish-Chandra projection does not increase PBW degree because it is defined by projecting the PBW decomposition onto the U(h) summand. Translation by ρ preserves polynomial degree on S(h), so HCρ is a filtered algebra homomorphism.

step 1.1
3.1

The PBW theorem gives the symmetrization map sym:S(g)U(g),x1xm1m!σSmxσ(1)xσ(m), as a filtration-preserving vector-space isomorphism whose associated graded map is the identity. The adjoint action is a derivation on both sides, so sym is g-equivariant. Since an element of U(g) is central exactly when it is killed by the adjoint action of the generators g, symmetrization restricts to invariant lifts and gives grZ(U(g))=S(g)g. PBW gives an ordered monomial basis for the enveloping algebra

step 2.1algebra
4.1

In the PBW decomposition, the top-degree part of pr(z) is obtained by discarding every monomial whose symbol contains a factor from n or n+. Translation by ρ changes only lower-degree terms. Thus the associated-graded Harish-Chandra map is exactly restriction S(g)gS(h)W, which is an isomorphism by [F2].

F2step 3.1algebra
5.1

A filtered algebra homomorphism whose associated graded map is an isomorphism is itself an isomorphism: lift target elements degree by degree for surjectivity, and take the leading symbol of a kernel element for injectivity. Applying this to steps 2.1 and 4.1 shows that HCρ is an algebra isomorphism Z(U(g))S(h)W.

step 2.1step 4.1

Depends on

Used by

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources