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.
A nonzero abelian category cannot satisfy both AB5 and AB5*
Statement
If an abelian category satisfies both AB5 and AB5*, then it is the zero category. Equivalently, no nonzero abelian category satisfies both axioms.
Facts & Assumptions
Given: An abelian category satisfying both AB5 and AB5*.
AB5 and AB5* are the directed-join and decreasing-meet distributivity laws of The axioms AB5 and AB5*.
An abelian category has zero objects, kernels, cokernels, and finite biproducts (Abelian category).
Proof
Suppose is a nonzero object. Let and , which exist by the AB3 and AB3* parts of [L1]. Let be the canonical map. For each , let be the tail subobject . Then is decreasing, because the product projections jointly detect morphisms, and because the finite head together with the tail generates all of . Applying AB5* to the family and the subobject gives .
For each , let be the finite partial sum . The family is directed and has join . Transport the product diagonal across the isomorphism from step 1.1, and let be its image. The diagonal is monic because each product projection composed with it is , so . But for every one has : a map factoring through both and has zero -st coproduct projection because it factors through , while through that same projection is the factor map itself, so the map is zero.
Applying AB5 to the directed family and the fixed subobject gives contradicting step 2.1. Therefore no nonzero object exists, so is the zero category.
Step 3.1 proves that satisfying both AB5 and AB5* forces the category to be zero, which is the contrapositive form of the theorem's second sentence.
Depends on
Used by
Nothing in the library uses this result yet.
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, Exercise A.4.7 (standard reference, not scraped)