claimroutineinferred_dep

Compatible solution eliminates the variable W

Eliminates WW via W0=ra+qbW_0=ra+qb, so C≅AC\cong A
reduces CC to the single-relation algebra AA
Claim·§2 An elementary lifting lemma·inside lemLifting lemma: polynomial algebra over B

Statement (paper)

In A[W]A[W], with W0=ra+qb∈AW_0=ra+qb\in A, one has (hW−a, y2W−b)=(W−W0)(hW-a,\ y^2W-b)=(W-W_0), and hence A[W]/(hW−a, y2W−b)≅AA[W]/(hW-a,\,y^2W-b)\cong A via evaluation at W0W_0; consequently C≅AC\cong A.

In plain English

In A[W]A[W], with W0=ra+qbW_0=ra+qb, the ideal (hW−a, y2W−b)(hW-a,\ y^2W-b) equals (W−W0)(W-W_0), so A[W]/(hW−a, y2W−b)≅AA[W]/(hW-a,\ y^2W-b)\cong A by evaluating at W0W_0. Hence C≅AC\cong A.

Why it's here

Since rh+qy2=1rh+qy^2=1, the two linear equations in WW have unimodular coefficients, and the compatibility y2a=hby^2a=hb makes W0=ra+qbW_0=ra+qb a common solution. So the pair of equations is equivalent to the single equation W=W0W=W_0, which removes WW and reduces CC to A=B[U,G]/(hG−yU−x)A=B[U,G]/(hG-yU-x), the form the next claim trivializes.
Classified routine:
This follows directly from the preceding compatibility and Bézout identity: both equations vanish at W₀, and their linear combination with coefficients r and q gives W−W₀. The quotient is then A by evaluation.

Uses

claimRemaining equations are compatible and unimodularclaimChange of variable makes first relation linear

Used by

claimExplicit parameter identifies A with B[T]

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Compatible solution eliminates the variable W" rests on claim-lem-lift-2
  • info
    inferred_dep
    critique: The conclusion C≅AC\cong A at paper.tex:224–225 explicitly invokes , established in claim-lem-lift-1 at lines 193–195. Compatibility alone does not supply that presentation.