TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

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: The hypotheses and objects in the Statement.

[L1]

A left $R$ -module $M$ is Noetherian when every submodule of $M$ 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).

[L2]

A left $R$ -module $M$ is Artinian when every descending chain $M_{0} \supseteq M_{1} \supseteq \dots$ of submodules stabilizes: there is $N$ such that $M_{n} = M_{N}$ for all $n \geq N$ . This is the descending chain condition. (Artinian modules by the descending chain condition).

[L3]

For submodules $L, N \leq M$ , there is a canonical isomorphism $L / (L \cap N) ≅ (L + N) / N .$ . (Second isomorphism theorem for modules).

[L4]

For $N \leq M$ , inverse image and quotient induce mutually inverse inclusion-preserving bijections between submodules of $M / N$ and submodules of $M$ containing $N$ . They preserve sums, intersections, and successive quotients. (Correspondence theorem for submodules of a quotient module).

[L5]

A short exact sequence is an exact sequence $0 ⟶ N \overset{i}{\to} M \overset{p}{\to} Q ⟶ 0;$ thus $i$ is injective, $p$ is surjective, and $im i = \ker p$ . (Exact sequences and short exact sequences of modules).

[L6]

A module is Noetherian if and only if every ascending chain of submodules stabilizes. (Finite generation, ACC, and maximal-condition characterizations of Noetherian modules).

[L7]

A module is Artinian if and only if every descending chain of submodules stabilizes. (DCC and minimal-condition characterizations of Artinian modules).

Proof

technique · direct

1.1

Identify $N$ with its image in $M$ . A chain in $N$ is a chain in $M$ , and the correspondence theorem lifts every chain in $Q = M / N$ to a chain of submodules of $M$ containing $N$ ; hence both ACC and DCC pass from $M$ to $N$ and $Q$ .

L1L2L3L4L5L6L7givenalgebra

2.1

Conversely, for a chain $(M_{i})$ in $M$ , the chains $(M_{i} \cap N)$ and $((M_{i} + N) / N)$ stabilize when $N$ and $Q$ have the relevant chain condition. If $M_{i} \subseteq M_{j}$ are beyond both stabilization indices and $x \in M_{j}$ , equality of the images gives $y \in M_{i}$ with $x - y \in N$ ; equality of the intersections then puts $x - y \in M_{i}$ , so $x \in M_{i}$ . The same argument with the inclusions reversed handles descending chains.

step 1.1givenalgebra

3.1

Thus $M$ has ACC exactly when $N$ and $Q$ do, and it has DCC exactly when $N$ and $Q$ do. Facts [L6] and [L7] convert these chain statements into the asserted Noetherian and Artinian equivalences.

L6L7step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 27 results over 9 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

William Crawley-Boevey, Noncommutative Algebra, Chapter 1 Sections 1.1-1.9 (standard reference, not scraped)