TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01

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.

Schanuel's lemma in an abelian category

Statement

If $0 \to K \to P \to A \to 0 and 0 \to K^{'} \to P^{'} \to A \to 0$ are short exact sequences with $P$ and $P^{'}$ projective, then $K \oplus P^{'} ≅ K^{'} \oplus P .$

Facts & Assumptions

Given: Two projective presentations of the same object $A$ as displayed.

[L1]

Pullbacks and pushouts provide the comparison object used in the proof (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L2]

The pullback of an epimorphism is an epimorphism (The pullback of an epimorphism is an epimorphism).

[L3]

For a projective object, every epimorphism onto it splits (Projective object characterisations).

Proof

technique · direct

1.1L1L2construct

Form the pullback $X = P \times_{A} P^{'}$ of the two epimorphisms onto $A$ as in [L1]. By [L2], the projections $X ↠ P$ and $X ↠ P^{'}$ are epimorphisms. Their kernels are $K^{'}$ and $K$ respectively, so there are short exact sequences $0 \to K^{'} \to X \to P \to 0, 0 \to K \to X \to P^{'} \to 0.$

2.1L3step 1.1∎

Since $P$ and $P^{'}$ are projective, [L3] splits both short exact sequences. Therefore $X ≅ K^{'} \oplus P ≅ K \oplus P^{'},$ which yields the claimed isomorphism $K \oplus P^{'} ≅ K^{'} \oplus P .$

Depends on

Used by

Dependency tree · two levels

10 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

Charles A. Weibel, An Introduction to Homological Algebra (standard reference, not scraped)
The Stacks Project, Section 10.109: Rings of finite global dimension (standard reference, not scraped)