TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-08 (Codex)

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.

Noetherian and Artinian conditions are each exact in short exact sequences

Statement

In a short exact sequence $0 \to N \to M \to Q \to 0$ , the module $M$ is Noetherian if and only if $N$ and $Q$ are Noetherian; the same equivalence holds with “Artinian” in place of “Noetherian”. See Noetherian modules: every submodule is finitely generated.

Facts & Assumptions

Given: A short exact sequence $0 \to N \overset{i}{\to} M \overset{p}{\to} Q \to 0$ of left $R$ -modules.

[F1]

Noetherian means that every submodule is finitely generated (Noetherian modules: every submodule is finitely generated). Artinian means that every descending sequence of submodules stabilizes (Artinian modules by the descending chain condition).

[F2]

The submodule generated by a set is the smallest submodule containing it; finitely generated means generated by a finite set (Generated submodule, cyclic and finitely generated modules, module basis and free module).

[F3]

Exactness gives injective $i$ , surjective $p$ , and $i (N) = \ker p$ (Exact sequences and short exact sequences of modules).

[L1]

Finitely many nonempty fibres admit a choice of representatives in ZF (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

Proof

technique · direct

1.1F2F3given

Identify $N$ with $i (N) \subseteq M$ using the injective homomorphism in [F3]. The generated submodule of a finite set is precisely its finite linear combinations: these combinations form a submodule containing the set, and every submodule containing it contains all such combinations. This follows from [F2] and the module laws. Thus homomorphisms carry finite generating sets to generating sets of their images.

2.1F1F3step 1.1

Suppose $M$ is Noetherian. Every submodule of $N$ is a submodule of $M$ , hence finitely generated. If $V \leq Q$ , its preimage $p^{- 1} (V)$ is a submodule of $M$ and has finite generators; their images generate $V$ because $p$ is surjective. Consequently $N$ and $Q$ are Noetherian.

2.2F1F3L1step 1.1choose

Conversely suppose $N$ and $Q$ are Noetherian, and let $L \leq M$ . Choose finite generators $a_{1}, \dots, a_{r}$ of $L \cap N$ and $q_{1}, \dots, q_{s}$ of $p (L)$ . By [L1], lift the finitely many $q_{j}$ to $b_{j} \in L$ . For $x \in L$ , write $p (x) = \sum_{j} c_{j} q_{j}$ . Then $x - \sum_{j} c_{j} b_{j}$ belongs to $L \cap \ker p = L \cap N$ , so is a linear combination of the $a_{i}$ . Thus the $a_{i}$ and $b_{j}$ generate $L$ . Empty generating lists cause no change to this argument. Since $L$ was arbitrary, $M$ is Noetherian, without any countable or dependent choice.

2.3F1F3step 1.1

Suppose $M$ is Artinian. A descending chain of submodules of $N$ is one in $M$ , hence stabilizes. A descending chain $(V_{j})$ in $Q$ lifts to the descending chain $(p^{- 1} (V_{j}))$ in $M$ ; after it stabilizes, its images $V_{j}$ stabilize by surjectivity. Thus $N$ and $Q$ are Artinian.

2.4F1F3step 1.1

Conversely suppose $N$ and $Q$ are Artinian and $L_{0} \supseteq L_{1} \supseteq \dots$ is a descending chain in $M$ . The chains $L_{j} \cap N$ and $p (L_{j})$ stabilize. Take an index $j_{0}$ beyond both stabilization indices. For $j \geq j_{0}$ and $x \in L_{j_{0}}$ , equality of images gives $y \in L_{j}$ with $p (y) = p (x)$ . Then $x - y \in L_{j_{0}} \cap N = L_{j} \cap N$ , so $x \in L_{j}$ . Hence $L_{j} = L_{j_{0}}$ for all $j \geq j_{0}$ , and $M$ is Artinian.

3.1step 2.1step 2.2step 2.3step 2.4∎

Steps 2.1 and 2.2 prove the Noetherian equivalence, and steps 2.3 and 2.4 prove the Artinian equivalence.

Depends on

Used by

Dependency tree · two levels

15 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

The Stacks Project, Lemma 10.5.3, finite-generation extension argument (standard reference, not scraped)
William Crawley-Boevey, Noncommutative Algebra, Chapter 1 Sections 1.1-1.9 (standard reference, not scraped)