Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass
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.

The SL2 flag charts realize the stated rho shift

Example

Let G=SL2(C), X=G/B≅P1, and use the repository basis h=(100−1),e=(0100),f=(0010). Let ρ satisfy ρ(h)=1. For an integer c, set κ=cρ and d=−c−1. Then Dcρ=Diff⁡(OP1(d)). On U0={x≠0} with coordinate z=y/x and frame e0=xd, the infinitesimal action is e=z2∂z+(c+1)z,f=−∂z,h=2z∂z+(c+1). On U1={y≠0} with coordinate w=x/y and frame e1=yd, it is e=−∂w,f=w2∂w+(c+1)w,h=−2w∂w−(c+1). These formulas glue, satisfy the sl2 relations, and give D−ρ=Diff⁡(OP1) when c=−1.

Facts & Assumptions

Given: The TDO and line-bundle convention of Flag-variety twisted differential operators and their modules, the standard sl2 basis of The special linear Lie algebra sl_2, and the integral identification PBW and integral line-bundle twisting for flag TDOs.

[F1]

The chosen basis satisfies [h,e]=2e, [h,f]=−2f, [e,f]=h (The special linear Lie algebra sl_2).

[F2]

For integral κ, Dκ is Diff⁡(OX(κ+ρ)); in particular the TDO parameter is shifted by ρ (PBW and integral line-bundle twisting for flag TDOs).

Verification

1.1F1F2givenalgebra

The weight of the unique positive root is 2ρ, so ρ(h)=1. With d=−c−1, the associated line is OX((c+1)ρ)=OP1(d) by [F2]. On U0, the inverse upper-unipotent matrix sends (1,z) to (1−tz,z); therefore its action on a local coefficient g(z)e0 is (1−tz)dg(z/(1−tz))e0. Differentiating at t=0 gives z2∂z−dz=z2∂z+(c+1)z for e. The inverse lower unipotent sends (1,z) to (1,z−t), giving −∂z for f. The inverse diagonal matrix sends (1,z) to (e−t,etz); the homogeneous frame contributes e−dt, so differentiation gives 2z∂z−d=2z∂z+(c+1) for h.

2.1F1step 1.1algebra

On U0∩U1, the frames satisfy e1=zde0, so a coefficient g1(w) on U1 corresponds to g0(z)=zdg1(1/z) on U0. If Tg1=zdg1(1/z), direct differentiation gives T−1∂zT=dw−w2∂w. Conjugating the three operators from step 1.1 by T and using d=−(c+1) gives, respectively, −∂w, w2∂w+(c+1)w and −2w∂w−(c+1). Thus the two formulas glue. Since they are obtained by differentiating the algebraic G-action, their commutators are the brackets in [F1]; direct substitution gives the same relations.

3.1F2step 1.1∎

At c=−1 one has d=0, so the line bundle is the trivial bundle and [F2] gives D−ρ=Diff⁡(OX), as claimed.

Depends on

Used by

Dependency tree · two levels

18 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