Alphabeta Math
CorollaryStatement: Literature-sourcedProof: Literature-sourcedSession-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.

Every algebra of finite type over a Noetherian ring is a Noetherian ring

Statement

Let R be a Noetherian commutative ring and let A be a commutative R-algebra of finite type (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras). Then A is a Noetherian ring.

Facts & Assumptions

Given: A Noetherian commutative ring R and a commutative R-algebra A of finite type, with structure map ηA ⁣:R→A.

[L1]

An R-algebra A is of finite type over R when A=R[a1,…,an] for some n∈N and a1,…,an∈A, where R[a1,…,an] is the image of the unital ring homomorphism R[x1,…,xn]→A agreeing with ηA on constants and sending xi to ai (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

For a ring homomorphism f ⁣:R→S there is a ring isomorphism R/ker⁡f≅im⁡f (First isomorphism theorem for rings: R/ker⁡f≅im⁡f).

[L3]

If R is a Noetherian commutative ring then R[x1,…,xn] is Noetherian for every n∈N (If R is Noetherian then R[x1,…,xn] is Noetherian for every n∈N).

[L4]

Every quotient R/I of a Noetherian commutative ring by an ideal is Noetherian (Every quotient and every localisation of a Noetherian ring is Noetherian).

Proof

technique · direct
1.1

By the finite-type hypothesis there are n∈N and a1,…,an∈A with A=R[a1,…,an], so the evaluation homomorphism ev⁡ ⁣:R[x1,…,xn]→A sending xi to ai has image all of A and is therefore surjective.

L1given
2.1

The first isomorphism theorem applied to ev⁡ gives a ring isomorphism R[x1,…,xn]/ker⁡ev⁡≅A.

L2step 1.1
3.1

The ring R[x1,…,xn] is Noetherian because R is, so its quotient by the ideal ker⁡ev⁡ is Noetherian; a ring isomorphism carries ideals to ideals and finite generating lists to finite generating lists, so A is Noetherian.

L3L4step 2.1algebra∎

Remarks

  • This is the form of the Hilbert basis theorem later pages use. A ring presented by finitely many generators and any relations at all is Noetherian, with no hypothesis on the relations; the number of generators is what matters, not their independence.

  • The converse is false and is not claimed. A Noetherian ring need not be of finite type over a Noetherian subring: a field extension generated by infinitely many algebraic elements is a field, hence Noetherian, and is not of finite type over the base field as an algebra.

Depends on

Used by

Dependency tree · two levels

21 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