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.
Composition series and length of a module
Definition
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; Jordan–Hölder theorem for modules ↗ proves independence of the chosen series. The zero module has the empty series and length .
Depends on
Used by
- Module length is additive in short exact sequences Corollary
- koszul euler characteristic and degree indexed multiplicity Definition
- The Hilbert function and formal Hilbert series of a graded module with finite-length pieces Definition
- The Hilbert-Samuel function and eventual Hilbert-Samuel polynomial of a finite local module Definition
- Total length of a zero-dimensional projective scheme Definition
- A field has module length one over itself Example
- A tangent line and conic have one intersection point of local length two Example
- In dimension zero the Hilbert-Samuel polynomial is constant and equals the module length Example
- The ℤ-module ℤ/pᵏ has length k Example
- A zero-dimensional projective scheme has finitely many closed points with finite-dimensional local rings Lemma
- Field extension preserves the graded pieces and the total length of a zero-dimensional projective quotient Lemma
- For a finite-length module, the radical is a superfluous submodule Lemma
- Hilbert series and eventual Hilbert value of a two-form plane complete intersection Lemma
- Local flatness criterion by regular parameters Lemma
- Projective representations and twisted algebra modules Lemma
- The eventual Hilbert function of a zero-dimensional projective quotient equals its total length Lemma
- The module-relative Hilbert–Samuel polynomial exists without a dimension theorem Lemma
- A commutative ring is Artinian exactly when it has finite length as a module over itself Theorem
- A module has a composition series if and only if it is Noetherian and Artinian, the converse using dependent choice Theorem
- Choice-free semisimple characterizations for finite-length modules Theorem
- Jordan–Hölder theorem for modules Theorem
- Length and valuation in a DVR Theorem
Dependency tree · two levels
6 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
- Arvind Nair, Algebra I, Lecture 5 (standard reference, not scraped)