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.
The splitting lemma for short exact sequences of modules
Statement
For a short exact sequence the following are equivalent:
- has a section ;
- has a retraction ;
- there is an isomorphism with and .
Given a section, and .
Facts & Assumptions
Given: A short exact sequence .
A section satisfies , and a retraction satisfies (Split short exact sequences, sections, and retractions).
Short exactness means that is injective, is surjective, and (The endpoints of a short exact sequence encode injectivity and surjectivity).
Homomorphisms from are uniquely determined by their restrictions to the two summands (Universal property of a direct sum of modules).
Proof
Suppose is a section and define by ; [L2] makes this a homomorphism.
Suppose assertion 3 holds. Define as the first coordinate of ; then gives , so is a retraction.
Suppose instead that is a retraction. For each , choose any with using surjectivity and put . Then and .
For , the element lies in , so by injectivity of there is a unique with ; hence and is surjective.
If , applying gives , and then injectivity of gives ; thus is injective and satisfies the compatibility conditions in assertion 3.
The element of step 1.3 is unique in with image : if and , then , say , and applying gives . Therefore the rule is independent of the temporary lift , is linear by uniqueness, and satisfies .
Steps 1.1, 2.1, and 2.2 prove , step 1.2 proves , and steps 1.3 and 2.3 prove . The formula for also yields the internal direct sum .
Depends on
Used by
- 0→ℤxrightarrow×2ℤ→ℤ/2ℤ→0 does not split Counterexample
- 0→ A→ A⊕ C→ C→0 is canonically split Example
- Equivalent characterizations of injective modules Theorem
- Equivalent characterizations of projective modules Theorem
Cited to discharge well-definedness by Split short exact sequences, sections, and retractions.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 17 results over 7 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
- A. Kleshchev, Lectures on Abstract Algebra for Graduate Students, sections 3.6, 3.14, and 3.15 (standard reference, not scraped)
- The Stacks Project, Algebra (standard reference, not scraped)
- P. Hekmati, Homological Algebra, section 3.1 (standard reference, not scraped)