CorollaryStatement: 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.

Module length is additive in short exact sequences

Statement

For a short exact sequence $0 \to N \to M \to Q \to 0$ , the module $M$ has finite length if and only if $N$ and $Q$ do, and then $ℓ_{R} (M) = ℓ_{R} (N) + ℓ_{R} (Q) .$ See Jordan–Hölder theorem for modules.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

Any two composition series of a module have the same length, and their simple factors agree up to permutation and isomorphism. (Jordan–Hölder theorem for modules).

[L2]

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).

[L3]

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

If $N$ and $Q$ have composition series, lift the series of $Q$ along $M \to Q$ and splice it above the series of $N$ . Correspondence identifies all lifted factors, so this is a composition series of $M$ with $ℓ_{R} (N) + ℓ_{R} (Q)$ factors.

L1L2L3givenalgebra

1.2

Conversely, let $0 = M_{0} < \dots < M_{n} = M$ be a composition series. Put $N_{i} = M_{i} \cap N$ and let $Q_{i}$ be the image of $M_{i}$ in $Q$ . For each $i$ , the simple factor $M_{i} / M_{i - 1}$ has submodule $N_{i} / N_{i - 1}$ and corresponding quotient $Q_{i} / Q_{i - 1}$ ; exactly one is that simple factor and the other is zero. Deleting repetitions therefore gives composition series of $N$ and $Q$ , and their numbers of factors add to $n$ .

L2L3givenalgebra

2.1

Jordan–Hölder makes all three lengths independent of the chosen series, so steps 1.1 and 1.2 prove both directions and the formula. If $N = 0$ , $Q = 0$ , or $M = 0$ , the relevant series is empty and the same count applies.

L1L2step 1.1step 1.2given∎

Depends on

Used by

The ℤ-module ℤ/pᵏ has length k Example

Dependency tree · next 3 levels

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