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 module has a composition series if and only if it is Noetherian and Artinian, the converse using dependent choice
Statement
A module with a composition series is both Noetherian and Artinian. Conversely, assuming dependent choice, a module that is both Noetherian and Artinian has a composition series. The zero module has the empty composition series. See Composition series and length of a module.
Facts & Assumptions
Given: The hypotheses and objects in the Statement. Dependent choice (The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain) is assumed only for the converse and is available under the Axiom of Choice (The Axiom of Choice).
A composition series of a left -module is a finite chain whose factors are simple. If such a series exists, the length is its number of factors; thm-jordan-holder-theorem-for-modules proves independence of the chosen series. The zero module has the empty series and length . (Composition series and length of a module).
For a left -module , write (1) every submodule is finitely generated, (2) ACC, and (3) every nonempty set of submodules has a maximal member. The implications and are choice-free; assumes DC, under which the three conditions are equivalent. (Finite generation, ACC, and maximal-condition characterizations of Noetherian modules).
For a left -module , DCC is equivalent to the condition that every nonempty family of submodules has a minimal member. The implication from DCC to the minimal condition uses dependent choice. (DCC and minimal-condition characterizations of Artinian modules).
In a short exact sequence , the module is Noetherian if and only if and are Noetherian; the same equivalence holds with “Artinian” in place of “Noetherian”. (Noetherian and Artinian conditions are each exact in short exact sequences).
Proof
Let be a composition series [L1] and induct on that is Noetherian and Artinian. The zero module satisfies both conditions vacuously. A simple factor has only the submodules and itself; any one nonzero element generates it, since its cyclic submodule is nonzero. Thus all its submodules are finitely generated and all descending chains stabilize. Applying [L4] to carries both conditions to . At this gives the forward implication, without any choice principle.
Conversely, assume dependent choice and let be Noetherian and Artinian. Every submodule of is Noetherian by [L4], so a nonzero submodule has a maximal proper submodule by the nonempty maximal condition of [L2], using DC. Define a relation on the submodules of by taking a maximal proper submodule at each nonzero term and letting zero be its own successor. This relation is serial. DC, available from the assumed AC, supplies a sequence starting at ; it strictly decreases until it reaches zero and is then constant. These are the precise choice uses in the converse.
The chain of step 1.2 is strictly descending while its terms are nonzero, so the descending chain condition forces some . Since is maximal proper in , the quotient is nonzero and has no proper nonzero submodule, hence is simple. Reversing the chain gives , a composition series. For the empty chain is already the required series, so no choice is consumed in that case. This proves the stated claim.
Depends on
Composition series and length of a module
Finite generation, ACC, and maximal-condition characterizations of Noetherian modules
DCC and minimal-condition characterizations of Artinian modules
Noetherian and Artinian conditions are each exact in short exact sequences
The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain
The Axiom of Choice