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.
Half nine lemma
Statement
Consider a commutative diagram in an abelian category whose three columns are short exact:
If the bottom two rows are short exact, then the top row is exact at and at .
Facts & Assumptions
Given: The commutative diagram in the statement.
In a short exact sequence, the left map is monic and the middle node is exact (Degenerate exactness criteria).
Monicity is equivalent to cancellation on members (Monicity by member cancellation).
Exactness at a node is equivalent to the member-lifting condition (Exactness is detected by members).
Proof
Let and be members of with the same image in . Commutativity gives the same image of and in . Because the second row is short exact, its left map is monic by [L1], so [L2] gives . The first column is also short exact, so its left map is monic; applying [L2] again yields . Hence the top-row map is monic, so the top row is exact at .
Let be a member of with image in . Commutativity gives that maps to in . Exactness of the second row at therefore yields a member of with by [L3]. Applying the right map of the first column gives Because the bottom row is short exact, its left map is monic by [L1], so [L2] shows . Exactness of the first column at now gives a member of with by [L3]. Then Since the second column is short exact, is monic, so [L2] gives . Thus every member of killed by lifts from , and the top row is exact at by [L3].
Therefore the top row is left exact whenever the bottom two rows and all three columns are short exact.
Depends on
Used by
Dependency tree · two levels
16 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
- Peter Freyd, Abelian Categories, Section 2.6 (standard reference, not scraped)
- Saunders Mac Lane, Homology, Chapter XII, Section 3 (standard reference, not scraped)