Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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.

A product of two Noetherian rings is Noetherian

Statement

Let R and S be Noetherian commutative rings. Then the product ring R×S (The product ring R×S with componentwise operations, its identity (1R,1S) and its units R××S×) is Noetherian.

Facts & Assumptions

Given: Noetherian commutative rings R and S, and their product ring R×S with componentwise operations.

[L1]

The product ring R×S is the cartesian product of the underlying sets with the componentwise operations (a,b)+(a,b)=(a+a,b+b) and (a,b)(a,b)=(aa,bb), zero (0R,0S) and identity (1R,1S) (The product ring R×S with componentwise operations, its identity (1R,1S) and its units R××S×).

[L2]

For a ring homomorphism f ⁣:RS there is a ring isomorphism R/kerfimf (First isomorphism theorem for rings: R/kerfimf).

[L3]

If a commutative ring T has ideals a1,,ar with r1 and zero intersection, and every quotient ring T/ai is Noetherian, then T is Noetherian (A ring with finitely many ideals of zero intersection whose quotients are Noetherian rings is Noetherian).

Proof

technique · direct
1.1

Put a1={0R}×S and a2=R×{0S}. Each is an additive subgroup of R×S closed under multiplication by an arbitrary element, since (a,b)(0R,t)=(0R,bt) and (a,b)(u,0S)=(au,0S), so each is an ideal; and a1a2={(0R,0S)}=0. The ring R×S is commutative because R and S are and the operations are componentwise.

L1givenalgebra
2.1

The coordinate maps p1(a,b)=a and p2(a,b)=b are ring homomorphisms, since the operations are componentwise and p1(1R,1S)=1R, p2(1R,1S)=1S; they are surjective, with kerp1=a1 and kerp2=a2. The first isomorphism theorem therefore gives ring isomorphisms (R×S)/a1R and (R×S)/a2S.

L1L2step 1.1algebra
3.1

A ring isomorphism carries ideals to ideals and finite generating lists to finite generating lists, so a ring isomorphic to a Noetherian ring is Noetherian; hence both quotients in step 2.1 are Noetherian. With the zero intersection of step 1.1 this is the hypothesis of the preceding corollary at r=2, and it gives that R×S is Noetherian.

L3step 1.1step 2.1algebra

Remarks

  • Every finite product of Noetherian rings is Noetherian, by induction on the number of factors using R1××Rn+1(R1××Rn)×Rn+1; the base case of one factor is tautological. A product indexed by an infinite set is not defined by The product ring R×S with componentwise operations, its identity (1R,1S) and its units R××S×, which introduces the product of two rings only, so no claim is made about one here.

  • The converse holds as well, though it is not what is claimed above: step 2.1 exhibits each factor as isomorphic to a quotient of R×S, and Every quotient and every localisation of a Noetherian ring is Noetherian makes every quotient of a Noetherian ring Noetherian. So R×S is Noetherian exactly when both factors are.

  • When both factors are nonzero, the two coordinate ideals are incomparable, and their intersection is zero while their sum is the unit ideal. If one factor is the zero ring, one coordinate ideal is the whole product and the other is zero, so they are comparable; the proof uses only their zero intersection and covers that degenerate case as well.

Depends on

Used by

Dependency tree · two levels

23 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