CounterexampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

For a field $F$ , the ideal $(x,y)$ in $F[x,y]$ is not principal

Statement refuted

If $F$ is a field, then every ideal of $F[x,y]$ is principal.

Facts & Assumptions

Given: A field $F$ , the iterated ring $F[x,y]=F[x][y]$ , and the ideal $I=(x,y)$ generated by $x$ and $y$ .

[L1]

The bivariate polynomial ring is obtained by adjoining $x$ and then $y$ (Polynomial rings in finitely many commuting indeterminates by iteration).

[L2]

A polynomial ring in finitely many indeterminates over a field is an integral domain (A polynomial ring in finitely many indeterminates over an integral domain is an integral domain).

[L3]

The ideal generated by a set is the smallest ideal containing that set, and $(h)$ denotes the ideal generated by one element $h$ (The ideal generated by a subset and principal ideals).

[L4]

Chosen images of the indeterminates determine evaluation homomorphisms (Universal property of $R[x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

Counterexample

technique · contradiction

1.1

In a commutative ring the multiples of $h$ form an ideal containing $h$ and lie in every ideal containing $h$ , so [L3] identifies $(h)$ with the set of multiples of $h$ . Suppose for contradiction that $I=(h)$ ; since $x,y\in I$ , the element $h$ divides both. Treating the ring as $F[x][y]$ by [L1], degree in $y$ and the domain property [L2] show from $h\mid x$ that $h\in F[x]$ .

assume-contragivenL1L2L3algebra

2.1

From $h\mid y$ , comparison of the leading coefficient in $y$ gives $1=h c$ for some $c\in F[x]$ , so $h$ is a unit and $(h)$ is the whole ring.

step 1.1L1L2L3algebra

3.1

Evaluation at $x=0,y=0$ exists by [L4] and has kernel an ideal containing $x,y$ , so [L3] gives $I$ inside that proper kernel; thus $I$ is proper, contradicting step 2.1, and $I$ is not principal.

step 2.1L3L4discharge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 33 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Thomas W. Judson, Abstract Algebra: Theory and Applications, Example 17.21 (standard reference, not scraped)

For a field FFF, the ideal (x,y)(x,y)(x,y) in F[x,y]F[x,y]F[x,y] is not principal