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.

The coefficientwise limits multiply back to the original polynomial

Statement

Let $A$ be $I$ -adically complete and separated, and let $(g_{r}, h_{r})_{r \geq 1}$ be monic polynomial lifts of fixed degrees such that:

$f - g_{r} h_{r} \in I^{r} [T]$ for every $r \geq 1$ , and
the coefficient sequences of $g_{r}$ and $h_{r}$ are $I$ -adically Cauchy.

Then the coefficientwise limits $g, h \in A [T]$ exist and satisfy $f = g h$ .

Facts & Assumptions

Given: An $I$ -adically complete and separated ring $A$ , a polynomial $f \in A [T]$ , and stagewise lifts $(g_{r}, h_{r})$ as above.

[L1]

The Hensel correction sequences are coefficientwise $I$ -adically Cauchy (Successive Hensel corrections are Cauchy).

[L2]

Completeness gives limits of $I$ -adic Cauchy sequences, and separatedness means that an element lying in every $I^{r}$ is zero (Separated and complete filtered modules).

Proof

technique · take coefficientwise limits and use separatedness on each coefficient

1.1L1L2given

By completeness and [L2], each coefficient sequence of $g_{r}$ and of $h_{r}$ has a limit in $A$ . Since the degrees are fixed and the leading coefficients are always $1$ , these limits assemble into monic polynomials $g, h \in A [T]$ of the same degrees.

2.1step 1.1givenalgebra

Fix a coefficient index $j$ of the product. Only finitely many coefficient pairs contribute to the $T^{j}$ -coefficient of $g_{r} h_{r}$ , so ordinary continuity of finite sums and products shows that the $T^{j}$ -coefficient of $g_{r} h_{r}$ converges to the $T^{j}$ -coefficient of $g h$ .

3.1L2step 2.1givenalgebra

For every $r$ , the coefficient of $T^{j}$ in $f - g_{r} h_{r}$ lies in $I^{r}$ by hypothesis. Passing to the limit in step 2.1 shows that the coefficient of $T^{j}$ in $f - g h$ lies in every $I^{r}$ . By separatedness and [L2], that coefficient is $0$ . Since this holds for every $j$ , one has $f = g h$ .

4.1step 1.1step 3.1∎

Therefore the coefficientwise limits of the iterative factors multiply back to the original polynomial.

Depends on

Used by

Complete separated adic pairs are Henselian Corollary

Dependency tree · two levels

5 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)
The Stacks Project, Section 15.11: Henselian pairs (standard reference, not scraped)