claimroutineinferred_dep

Unit ideal gives affine three-space fibre

Shows (h,y)=B(h,y)=B, so R/(F)≅B[T]≅C[X,Y,T]R/(F)\cong B[T]\cong\CC[X,Y,T]
applies the lifting lemma to get the three-space fibre
Claim·§3 The affine-space fibre and the critical point·inside thmNoncoordinate polynomial with affine three-space zero fibre

Statement (paper)

The elements h,yh,y generate the unit ideal in BB, i.e. B/(h,y)B/(h,y) is the zero ring. Consequently, for the algebra 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) of Lemma  one has C≅R/(F)C\cong R/(F) and R/(F)≅C≅B[T]≅C[X,Y,T]R/(F)\cong C\cong B[T]\cong\CC[X,Y,T].

In plain English

In BB the elements hh and yy generate the unit ideal, so B/(h,y)=0B/(h,y)=0. Hence the lifted algebra CC is isomorphic to R/(F)R/(F), and R/(F)≅C≅B[T]≅C[X,Y,T]R/(F)\cong C\cong B[T]\cong\CC[X,Y,T].

Why it's here

This checks the comaximality hypothesis (h,y)=B(h,y)=B of the lifting lemma, so C≅B[T]C\cong B[T]. Since B≅C[X,Y]B\cong\CC[X,Y] by the previous claim, B[T]B[T] is a polynomial ring in three variables. Together with C≅R/(F)C\cong R/(F) this gives the isomorphism R/(F)≅C[3]R/(F)\cong\CC^{[3]} in the main theorem.
Classified routine:
The unit-ideal check is a calculation from the defining equations of B. The affine-three-space conclusion then follows directly from the lifting lemma and the preceding isomorphism B ≅ ℂ[X,Y].

Uses

lemLifting lemma: polynomial algebra over BclaimCusp and translation identitiesclaimBase algebra is a polynomial ring

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Unit ideal permits lifting the fibre presentation" rests on claim-thm-main-1
  • info
    inferred_dep
    outline: "Unit ideal permits lifting the fibre presentation" rests on claim-thm-main-2