claimroutine

Change of variable makes first relation linear

Substituting G=V+UWG=V+UW makes the first relation linear: hG−yU=xhG-yU=x
puts CC in the form the elimination steps work on
Claim·§2 An elementary lifting lemma·inside lemLifting lemma: polynomial algebra over B

Statement (paper)

Under the substitution G=V+UWG=V+UW (with inverse V=G−UWV=G-UW), modulo the relation hW=y+U2hW=y+U^2 one has S(h,U,G−UW,W)=hG2−2UyG+y2WS(h,U,G-UW,W)=hG^2-2UyG+y^2W, and the relation U3+hV−xU^3+hV-x becomes hG−yU−xhG-yU-x. Consequently C≅B[U,G,W]/(hG−yU−x, hW−y−U2, y2W−s+hG2−2UyG)C\cong B[U,G,W]/\bigl(hG-yU-x,\ hW-y-U^2,\ y^2W-s+hG^2-2UyG\bigr).

In plain English

Substituting G=V+UWG=V+UW turns the relations defining CC into hG−yU−xhG-yU-x, hW−y−U2hW-y-U^2, and y2W−s+hG2−2UyGy^2W-s+hG^2-2UyG, so C≅B[U,G,W]/(hG−yU−x, hW−y−U2, y2W−s+hG2−2UyG)C\cong B[U,G,W]/(hG-yU-x,\ hW-y-U^2,\ y^2W-s+hG^2-2UyG).

Why it's here

The substitution is an invertible change of variables, so it does not change the algebra, and it makes the first relation linear in UU and GG using x2+y3=hsx^2+y^3=hs and hW=y+U2hW=y+U^2. This gives the form that the later steps use: they build A=B[U,G]/(hG−yU−x)A=B[U,G]/(hG-yU-x) and eliminate WW from the remaining two equations.
Classified routine:
This follows by the invertible triangular substitution G=V+UW, direct expansion, and reduction using hW=y+U². It is an algebraic calculation rather than a new lifting principle.

Uses

Nothing else in the paper

Used by

claimRemaining 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
—
Line
paper.tex:178
Leannot aligned

Phase 2 aligns this node to a Lean declaration.