lemmaroutineunresolved_ref

Lifting lemma: polynomial algebra over B

If x2+y3=hsx^2+y^3=hs and (h,y)=B(h,y)=B, then C≅B[T]C\cong B[T]
turns the unit ideal (h,y)(h,y) into a polynomial fibre algebra
Lemma·lem:lift·§2 An elementary lifting lemma

Statement (paper)

Let BB be a ring and let h,x,y,s∈Bh,x,y,s\in B satisfy x2+y3=hs,(h,y)=B. x^2+y^3=hs,\qquad (h,y)=B. Then the BB-algebra C=B[U,V,W]/(U3+hV−x, −U2+hW−y, S(h,U,V,W)−s) C=B[U,V,W]/\bigl(U^3+hV-x,\,-U^2+hW-y,\, S(h,U,V,W)-s\bigr) is isomorphic to B[T]B[T], where TT is an indeterminate.

In plain English

If x2+y3=hsx^2+y^3=hs in a ring BB and (h,y)=B(h,y)=B, then C=B[U,V,W]/(U3+hV−x, −U2+hW−y, S(h,U,V,W)−s)C=B[U,V,W]/(U^3+hV-x,\,-U^2+hW-y,\,S(h,U,V,W)-s) is isomorphic to the polynomial ring B[T]B[T] as a BB-algebra.

Why it's here

The lemma lets one pass from a base ring where hh and yy are comaximal to a one-variable polynomial extension, which the main theorem uses to identify a fibre algebra with a polynomial ring. The proof substitutes G=V+UWG=V+UW and eliminates WW using the unimodular pair (h,y2)(h,y^2). It then solves the one remaining linear relation hG−yU=xhG-yU=x with a single free parameter TT.
Classified routine:
This is an elementary elimination argument: the substitution G=V+UW reduces the presentation to a linear relation, which is solved using the unimodular pair (h,y²). Its particular form serves this paper, but the method is standard.

Uses

Nothing else in the paper

Used by

thmNoncoordinate polynomial with affine three-space zero fibreclaimUnit ideal gives affine three-space fibre

Inside the proof

claimChange of variable makes first relation linearclaimRemaining equations are compatible and unimodularclaimCompatible solution eliminates the variable WclaimExplicit parameter identifies A with B[T]

Sources

PaperOpen
Section
§2 An elementary lifting lemma
Page
—
Label
lem:lift
Line
paper.tex:164
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    The key expansion at lines 186–189 uses the universal polynomial S defined in equation eq:xyz, outside the skeleton statements.