Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck 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 0→A→iB→pC→0, the following are equivalent:

  1. p has a section s:C→B;
  2. i has a retraction r:B→A;
  3. there is an isomorphism Φ:A⊕C→B 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 0→A→iB→pC→0.

[F1]

A section satisfies p∘s=id⁡C, and a retraction satisfies r∘i=id⁡A (Split short exact sequences, sections, and retractions).

[L1]

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

[L2]

Homomorphisms from A⊕C 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 Φ:A⊕C→B by Φ(a,c)=i(a)+s(c); [L2] makes this a homomorphism.

assume-hypF1L2
1.2

Suppose assertion 3 holds. Define r:B→A 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 c∈C, choose any b with p(b)=c using surjectivity and put k=b−i(r(b)). Then r(k)=0 and p(k)=c.

assume-hypF1L1choose
2.1

For b∈B, the element b−s(p(b)) lies in ker⁡p=im⁡i, so by injectivity of i there is a unique a∈A with i(a)=b−s(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 ker⁡r with image c: if k′∈ker⁡r and p(k′)=c, then k−k′∈ker⁡p=im⁡i, say k−k′=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 p∘s=id⁡C.

step 1.3F1L1
3.1

Steps 1.1, 2.1, and 2.2 prove 1⇒3, step 1.2 proves 3⇒2, and steps 1.3 and 2.3 prove 2⇒1. 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 · two levels

8 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