claimroutineinferred_dep

Base algebra is a polynomial ring

Shows B≅C[X,Y,s]/(X2+Y3−s)≅C[X,Y]B\cong\CC[X,Y,s]/(X^2+Y^3-s)\cong\CC[X,Y]
identifies the base algebra as a polynomial ring
Claim·§3 The affine-space fibre and the critical point·inside thmNoncoordinate polynomial with affine three-space zero fibre

Statement (paper)

The algebra B=C[h,x,y,s]/(h−1−p(x,y,s), x2+y3−sh)B=\CC[h,x,y,s]/\bigl(h-1-p(x,y,s),\ x^2+y^3-sh\bigr) is isomorphic to C[X,Y,s]/(X2+Y3−s)≅C[X,Y]\CC[X,Y,s]/(X^2+Y^3-s)\cong\CC[X,Y], a polynomial ring in two variables, where X=x+s3X=x+s^3 and Y=y−s2Y=y-s^2; explicitly, the inverse presentation is s=X2+Y3s=X^2+Y^3, x=X−s3x=X-s^3, y=Y+s2y=Y+s^2, h=1+p(x,y,s)h=1+p(x,y,s).

In plain English

The algebra B=C[h,x,y,s]/(h−1−p(x,y,s), x2+y3−sh)B=\CC[h,x,y,s]/(h-1-p(x,y,s),\ x^2+y^3-sh) is isomorphic to C[X,Y,s]/(X2+Y3−s)≅C[X,Y]\CC[X,Y,s]/(X^2+Y^3-s)\cong\CC[X,Y], with X=x+s3X=x+s^3 and Y=y−s2Y=y-s^2. The inverse is given by s=X2+Y3s=X^2+Y^3, x=X−s3x=X-s^3, y=Y+s2y=Y+s^2, h=1+p(x,y,s)h=1+p(x,y,s).

Why it's here

Eliminating hh via its defining relation turns the cusp relation x2+y3=hsx^2+y^3=hs into X2+Y3=sX^2+Y^3=s after the translation, using the identity from the previous claim. This relation is linear in ss, so ss can be eliminated and BB is a polynomial ring in X,YX,Y. This explicit description lets the later claims analyse BB, for example the ideal (h,y)(h,y), and lift the fibre presentation.
Classified routine:
This follows by substituting the earlier cusp-and-translation identity into the defining relations of B, then eliminating h and the linearly occurring variable s.

Uses

claimCusp and translation identities

Used by

claimUnit ideal gives affine three-space fibre

Sources

PaperOpen
Section
§3 The affine-space fibre and the critical point
Page
—
Label
—
Line
paper.tex:269
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Translation makes the auxiliary base polynomial" rests on claim-thm-main-1