claimroutineinferred_dep

Explicit parameter identifies A with B[T]

Sets U=hT−βxU=hT-\beta x, G=yT+αxG=yT+\alpha x to identify AA with B[T]B[T]
final step: solves the linear relation with one parameter
Claim·§2 An elementary lifting lemma·inside lemLifting lemma: polynomial algebra over B

Statement (paper)

The BB-algebra map A→B[T]A\to B[T] defined by U=hT−βxU=hT-\beta x, G=yT+αxG=yT+\alpha x is an isomorphism with inverse T↦αU+βGT\mapsto \alpha U+\beta G, so A≅B[T]A\cong B[T] and hence C≅A≅B[T]C\cong A\cong B[T]; in the original variables the parameter is T=αU+β(V+UW)T=\alpha U+\beta(V+UW).

In plain English

The BB-algebra A=B[U,G]/(hG−yU−x)A=B[U,G]/(hG-yU-x) is isomorphic to the polynomial ring B[T]B[T] via U=hT−βxU=hT-\beta x, G=yT+αxG=yT+\alpha x, with inverse T↦αU+βGT\mapsto \alpha U+\beta G. Therefore C≅A≅B[T]C\cong A\cong B[T], and in the original variables T=αU+β(V+UW)T=\alpha U+\beta(V+UW).

Why it's here

This is the final step of the lifting lemma: after the earlier claims reduce CC to AA, the unimodularity (h,y)=B(h,y)=B (with α,β\alpha,\beta the coefficients expressing it) lets the single linear relation hG−yU=xhG-yU=x be solved by one free parameter TT. This gives C≅B[T]C\cong B[T] and thus the lemma.
Classified routine:
This is an explicit parametrization of the linear relation using the Bézout identity b1h+b2y=1, followed by the earlier elimination of W that gives Ca0c5a0A.

Uses

claimChange of variable makes first relation linearclaimCompatible solution eliminates the variable W

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Explicit parameter trivializes the remaining algebra" rests on claim-lem-lift-1
  • info
    inferred_dep
    outline: "Explicit parameter trivializes the remaining algebra" rests on claim-lem-lift-3