Alphabeta MathHow 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.
Finite generation, ACC, and maximal-condition characterizations of Noetherian modules
Statement
For a left -module , the following are equivalent: every submodule is finitely generated; every ascending chain of submodules stabilizes; and every nonempty family of submodules has a maximal member. The implication from ACC to the maximal condition uses dependent choice; the other displayed implications are choice-free. See Noetherian modules: every submodule is finitely generated.
Facts & Assumptions
Given: The hypotheses and objects in the Statement. The adopted axiom of dependent choice is assumed for the one direction identified in the Statement; it is not cited as a forward dependency.
A left -module is Noetherian when every submodule of is finitely generated (def-generated-cyclic-finitely-generated-and-free-modules). This finite-generation definition is the convention; its equivalence with ACC and the maximal condition is proved in thm-equivalent-characterizations-of-noetherian-modules. (Noetherian modules: every submodule is finitely generated).
Proof
We prove that finite generation of every submodule implies ACC by taking the union of a chain and locating a finite generating set in one stage.
Assuming the adopted dependent-choice axiom in Facts, ACC implies the maximal condition: if a nonempty family had no maximal member, recursively choose a strict ascending chain in it.
Choice-free: for a submodule N, the maximal condition applied to its finitely generated submodules gives a maximal L; if L is proper in N, adjoining one element of N minus L contradicts maximality.
Thus the finite-generation condition, ACC, and the maximal condition are equivalent. Only the recursive construction in step 2.1 uses the adopted dependent-choice axiom. This proves the stated claim.
Depends on
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 7 results over 5 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
- Keith Conrad, Noetherian Modules, Sections 1-2 (standard reference, not scraped)