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 connecting morphism exists and is unique
Statement
Let
be snake data in the Mac Lane shape. Let be a kernel of and a cokernel of .
Form the pullback with projections and the pushout of and with coprojections
Then there exists a unique morphism such that
Facts & Assumptions
Given: The snake-data diagram in the statement, together with and .
In a short exact sequence, the left map is a kernel and the right map is a cokernel (A short exact sequence is a kernel-cokernel pair).
Pullbacks and pushouts exist, pullbacks of epimorphisms are epimorphisms, and the induced map on kernels in a pullback square is an isomorphism (Pullbacks and pushouts as limits and colimits of cospans and spans, The pullback of an epimorphism is an epimorphism, In a pullback square, the induced map on the kernels of the two parallel arrows is an isomorphism).
A pushout of a monomorphism is again a monomorphism (The pushout of a monomorphism is a monomorphism).
A complex is short exact exactly when is a kernel of and is epic (Degenerate exactness criteria).
Kernels and cokernels are characterized by their universal properties (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).
Proof
Because the top row is short exact, [L1] says that is epic and . Form the pullback of along :
tikzcd P \arrow[r, "\pi'"] \arrow[d, "\pi"'] & B \arrow[d, "p"] \\ K \arrow[r, "k_h"'] & C.
By [L2], the map is epic. The induced map on kernels identifies with , so after transporting along we obtain a kernel of satisfying . [L1, L2, construct]
Form the pushout of and :
tikzcd A' \arrow[r, "i'"] \arrow[d, "q_f"'] & B' \arrow[d, "\iota'"] \\ Q \arrow[r, "\iota"'] & R.
Since is monic by [L1], [L3] makes monic. [L1, L3, construct]
Step 1.1 gives and makes epic. By [L4], the sequence is therefore short exact. Applying [L1] to this new short exact sequence shows that is also a cokernel of .
The pullback relation gives so the snake-data square yields Because by [L1], [L5] gives a unique map with
Since and the left square commutes, we have The map is monic, so . Therefore Because is a cokernel of by step 2.1, [L5] yields a unique morphism with
Composing with the pushout coprojection gives which is the required relation. If and both satisfy that relation, then Since is epic by step 1.1 and is monic by step 1.2, this forces .
Hence the connecting morphism exists and is unique.
Depends on
- Snake data
- Pullbacks and pushouts as limits and colimits of cospans and spans
- Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers
- A short exact sequence is a kernel-cokernel pair
- Degenerate exactness criteria
- The pullback of an epimorphism is an epimorphism
- In a pullback square, the induced map on the kernels of the two parallel arrows is an isomorphism
- The pushout of a monomorphism is a monomorphism
Used by
- The connecting morphism computed for a short exact sequence of abelian groups Example
- FALSE: the connecting morphism depends on the choices made in its construction False statement
- FALSE: the diagram lemmas in an abelian category follow from the module case by the embedding theorem False statement
- The connecting morphism depends on no choices Remark
- An exact functor transports every diagram lemma Theorem
- Naturality of the connecting morphism Theorem
- Snake lemma in an abelian category Theorem
Dependency tree · two levels
23 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
- Saunders Mac Lane, Categories for the Working Mathematician, Lemma VIII.4.5 (standard reference, not scraped)
- The Stacks Project, Section 12.5, Lemma 12.5.17(1) (standard reference, not scraped)