Alphabeta MathHow 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-Holder theorem in an abelian category
Statement
If an object in an abelian category has two composition series, then the two series have the same length and the same composition factors up to permutation and isomorphism.
Facts & Assumptions
Given: Two composition series of the same object .
A composition series is a finite strict subobject chain with simple successive quotients (Composition series and composition factors of an object, Simple object).
Any two finite subobject chains admit equivalent refinements (Schreier refinement theorem in an abelian category).
Proof
By [L2], the two composition series admit equivalent refinements.
A composition series has no proper refinement. Indeed, if , then the quotient map carries to a nonzero proper subobject of the simple object , contradicting [L1]. So any refinement of a composition series differs from it only by repeated adjacent terms.
Delete repeated adjacent terms from the equivalent refinements of step 1.1. By step 1.2 this recovers the original two composition series, and the quotient pairing survives. Therefore the original series have the same number of factors, and a permutation matches their factors up to isomorphism.