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.
Exactness of kernel and cokernel sequences under endpoint hypotheses
Statement
Consider a commutative diagram in an abelian category
Then:
- if the top row is exact and is monic, the induced sequence is exact;
- if the bottom row is exact and is epic, the induced sequence is exact.
Facts & Assumptions
Given: The commutative diagram in the statement.
Exactness can be tested by the covering criterion (The covering criterion for exactness).
Exactness is self-dual (Exactness is self-dual).
Kernels are universal for morphisms annihilated by the given map, and cokernels are dual (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).
Every kernel is monic (Every equalizer is a monomorphism, and every coequalizer is an epimorphism).
Proof
Assume the top row is exact and is monic. Choose kernels , , and . By [L3], the commutative diagram induces morphisms with
To prove exactness of apply the covering criterion [L1] to the pair . Let satisfy . Then so exactness of the top row gives an object , an epimorphism , and a morphism with
Applying to the displayed equality gives Since is monic, . The kernel property of therefore gives with . Now so monicity of from [L4] yields . Also so monicity of from [L4] gives . Thus the pair satisfies both parts of the covering criterion [L1], and the kernel sequence is exact.
The cokernel statement is the formal dual of steps 1.1 to 3.1 in the opposite abelian category: bottom-row exactness becomes top-row exactness, the epicity of becomes monicity of , kernels become cokernels, and [L2] transports the resulting exact sequence back to the original category.
Therefore both displayed induced sequences are exact under the stated endpoint hypotheses.
Depends on
Used by
Dependency tree · two levels
14 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
- The Stacks Project, Section 12.5, Lemma 12.5.16 (standard reference, not scraped)