TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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.

Jordan–Hölder theorem for modules

Statement

Any two composition series of a module have the same length, and their simple factors agree up to permutation and isomorphism. See Composition series and length of a module.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

A composition series of a left $R$ -module $M$ is a finite chain $0 = M_{0} < M_{1} < \dots < M_{n} = M$ whose factors $M_{i} / M_{i - 1}$ are simple. If such a series exists, the length $ℓ_{R} (M)$ is its number $n$ of factors; thm-jordan-holder-theorem-for-modules proves independence of the chosen series. The zero module has the empty series and length $0$ . (Composition series and length of a module).

[L2]

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

[L3]

If $N \leq L \leq M$ , then $L / N$ is a submodule of $M / N$ and $(M / N) / (L / N) ≅ M / L .$ . (Third 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).

Proof

technique · direct

1.1

Fix a composition series $0 = M_{0} < \dots < M_{n} = M$ and prove by induction on $n$ that it has the asserted comparison with every other composition series of $M$ . We use simultaneously the elementary consequence that, for any $C \leq M$ , intersecting the fixed series with $C$ and deleting repetitions gives a composition series of $C$ : each remaining factor embeds in the corresponding simple factor $M_{i} / M_{i - 1}$ and is therefore simple.

L1L2L3L4givenalgebra

2.1

The case $n = 0$ is $M = 0$ . For $n > 0$ , let $A = M_{n - 1}$ and let $B$ be the penultimate term of a second series. If $A = B$ , the induction hypothesis applied in $A$ matches all lower factors, and the common top factor finishes.

step 1.1given

3.1

Suppose $A \neq B$ . Since $A$ and $B$ are maximal proper submodules, $A + B = M$ . Put $C = A \cap B$ . The second isomorphism theorem gives $A / C ≅ M / B, B / C ≅ M / A,$ so both quotients are simple.

L2step 1.1step 2.1givenalgebra

4.1

By step 1.1, $C$ has a composition series. Appending $A$ gives a composition series of $A$ ending in $A / C$ . Compare it with $0 = M_{0} < \dots < M_{n - 1} = A$ using the induction hypothesis, whose fixed first series has length $n - 1$ . It follows that the series of $C$ has length $n - 2$ and that its factors together with $A / C$ are exactly the factors below $M / A$ in the fixed series.

L3L4step 1.1step 3.1given

5.1

Appending $B$ to the same series of $C$ gives a composition series of $B$ of length $n - 1$ . Using this as the fixed first series, the induction hypothesis compares it with the lower part of the second series. The isomorphisms in step 3.1 exchange the two top simple factors $A / C$ and $M / A$ with $M / B$ and $B / C$ . Hence the two original series have length $n$ and the same factors up to permutation. This also covers $n = 1$ , when $C = 0$ .

step 2.1step 3.1step 4.1given∎

Depends on

Used by

Module length is additive in short exact sequences Corollary
The ℤ-module ℤ/pᵏ has length k Example
Choice-free semisimple characterizations for finite-length modules Theorem
Uniqueness of the Wedderburn–Artin factors Theorem

Cited to discharge well-definedness by Composition series and length of a module.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 19 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

Arvind Nair, Algebra I, Lecture 5 (standard reference, not scraped)