LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

One correction step raises factor lifting by one ideal power

Statement

Let $A$ be a commutative ring, let $I \subseteq A$ be an ideal, let $f, g, h \in A [T]$ with $f$ monic and $g, h$ monic of degrees $m, n$ , and let $r \geq 1$ . Assume:

$\deg f = m + n$ ,
$f - g h \in I^{r} [T]$ , and
there exist $a, b \in A [T]$ with $a g + b h \equiv 1 (m o d I)$ .

Then there exist $u, v \in I^{r} [T]$ with $\deg u < m$ and $\deg v < n$ such that for $g^{'} = g + u$ and $h^{'} = h + v$ one has $f - g^{'} h^{'} \in I^{r + 1} [T] .$

Facts & Assumptions

Given: A commutative ring $A$ , an ideal $I$ , monic polynomials $f, g, h$ as above, an integer $r \geq 1$ , an error term $e = f - g h \in I^{r} [T]$ , and a lifted Bezout relation $a g + b h \equiv 1 (m o d I)$ , with $\deg f = m + n$ .

[L1]

A coprime residue factorization admits such a lifted Bezout identity modulo $I$ (Lift a Bezout identity for coprime residue factors).

[L2]

Corrections of degrees $< m$ and $< n$ preserve the monicity and degrees of the factors (Monicity and degree stay fixed during Hensel factor lifting).

Proof

technique · solve the linearized correction equation modulo $I^{r+1}$

1.1

Put $M = I^{r} / I^{r + 1}$ , viewed as an $A / I$ -module, and write $ε \in M [T]$ for the class of $e = f - g h$ . Since $f$ and $g h$ are monic of the same degree $m + n$ , one has $\deg ε < m + n$ . Multiplying $a g + b h \equiv 1 (m o d I)$ by $ε$ gives $ε = (a ε) g + (b ε) h in M [T] .$

L1givenalgebra

2.1

Divide $b ε \in M [T]$ by the monic polynomial $g$ to write $b ε = q g + \overset{ˉ}{u}, \deg \overset{ˉ}{u} < m .$ Substitution in step 1.1 gives $ε = \overset{ˉ}{u} h + \overset{ˉ}{v} g, \overset{ˉ}{v} : = a ε + q h .$ The polynomial $ε - \overset{ˉ}{u} h = \overset{ˉ}{v} g$ has degree less than $m + n$ ; because $g$ is monic of degree $m$ , this forces $\deg \overset{ˉ}{v} < n$ . Lift $\overset{ˉ}{u}, \overset{ˉ}{v}$ coefficientwise to polynomials $u, v \in I^{r} [T]$ with the same degree bounds.

step 1.1choosealgebra

3.1

Set $g^{'} = g + u$ and $h^{'} = h + v$ . Then $g^{'} h^{'} = g h + u h + v g + u v .$ By step 2.1, the first three terms agree with $f$ modulo $I^{r + 1}$ , while $u v \in I^{2 r} [T] \subseteq I^{r + 1} [T]$ because $r \geq 1$ . Hence $f - g^{'} h^{'} \in I^{r + 1} [T]$ . By [L2], $g^{'}$ and $h^{'}$ remain monic of degrees $m, n$ .

L2step 2.1givenalgebra

4.1

Therefore one Hensel correction step improves a lift modulo $I^{r}$ to a lift modulo $I^{r + 1}$ without changing the prescribed degrees.

step 3.1∎

Depends on

Used by

Complete separated adic pairs are Henselian Corollary
A coprime factorisation lifted modulo three successive powers Example
Successive Hensel corrections are Cauchy Lemma

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Chapter 22 (standard reference, not scraped)
Melvin Hochster, The structure theory of complete local rings (standard reference, not scraped)