Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13
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 0AiBpC0, the following are equivalent:

  1. p has a section s:CB;
  2. i has a retraction r:BA;
  3. there is an isomorphism Φ:ACB with Φ(a,0)=i(a) and p(Φ(a,c))=c.

Given a section, Φ(a,c)=i(a)+s(c) and B=i(A)s(C).

Facts & Assumptions

Given: A short exact sequence 0AiBpC0.

[F1]

A section satisfies ps=idC, and a retraction satisfies ri=idA (Split short exact sequences, sections, and retractions).

[L1]

Short exactness means that i is injective, p is surjective, and imi=kerp (The endpoints of a short exact sequence encode injectivity and surjectivity).

[L2]

Homomorphisms from AC are uniquely determined by their restrictions to the two summands (Universal property of a direct sum of modules).

Proof

technique · direct
1.1

Suppose s is a section and define Φ:ACB by Φ(a,c)=i(a)+s(c); [L2] makes this a homomorphism.

assume-hypF1L2
1.2

Suppose assertion 3 holds. Define r:BA as the first coordinate of Φ1; then Φ(a,0)=i(a) gives r(i(a))=a, so r is a retraction.

assume-hypF1construct
1.3

Suppose instead that r is a retraction. For each cC, choose any b with p(b)=c using surjectivity and put k=bi(r(b)). Then r(k)=0 and p(k)=c.

assume-hypF1L1choose
2.1

For bB, the element bs(p(b)) lies in kerp=imi, so by injectivity of i there is a unique aA with i(a)=bs(p(b)); hence b=Φ(a,p(b)) and Φ is surjective.

step 1.1F1L1
2.2

If Φ(a,c)=0, applying p gives c=0, and then injectivity of i gives a=0; thus Φ is injective and satisfies the compatibility conditions in assertion 3.

step 1.1F1L1
2.3

The element k of step 1.3 is unique in kerr with image c: if kkerr and p(k)=c, then kkkerp=imi, say kk=i(a), and applying r gives a=0. Therefore the rule s(c)=k is independent of the temporary lift b, is linear by uniqueness, and satisfies ps=idC.

step 1.3F1L1
3.1

Steps 1.1, 2.1, and 2.2 prove 13, step 1.2 proves 32, and steps 1.3 and 2.3 prove 21. The formula for Φ also yields the internal direct sum B=i(A)s(C).

step 1.1step 2.1step 2.2step 1.2step 1.3step 2.3

Depends on

Used by

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