Alphabeta MathHow 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.
An abelian category is balanced
Statement
If in an abelian category is both monic and epic, then is an isomorphism.
Facts & Assumptions
Given: An abelian category and a morphism that is both monic and epic.
The kernel of a monomorphism is zero, and the cokernel of an epimorphism is zero (The kernel of a monomorphism is zero and the cokernel of an epimorphism is zero).
The cokernel of is , and the kernel of is (The cokernel of the zero map out of the zero object is the target, and dually for kernels).
Every morphism has a canonical factorization (The canonical morphism from the coimage to the image exists and is unique).
In an abelian category the canonical map is an isomorphism (Abelian category).
Proof
Because is monic and epic, [L1] identifies and with zero objects. Hence [L2] gives isomorphisms and for the coimage projection and image inclusion of .
By [L4], the middle map is an isomorphism. Since , step 1.1 shows that is a composite of three isomorphisms, so itself is an isomorphism.
Depends on
Used by
- A morphism of short exact sequences with invertible outer maps is invertible Corollary
- An abelian category that is a preorder is trivial Corollary
- Torsion-free abelian groups do not form an abelian category Counterexample
- FALSE: in an abelian category a morphism can be monic and epic without being an isomorphism False statement
- A chain map is a quasi-isomorphism exactly when its cone is acyclic Theorem
- A complex is exact at n exactly when its nth homology is zero Theorem
- A generator detects comparison of subobjects Theorem
- Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism Theorem
- Five lemma for a morphism of long exact sequences Theorem
- Five lemma in an abelian category Theorem
- Module reconstruction from a small projective generator with supplied copowers and cokernels Theorem
- Short five lemma by pullback without members Theorem
- Short five lemma in an abelian category Theorem
- The subobject lattice of an abelian category is modular Theorem
Dependency tree · two levels
11 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
- Junhan Tan, The Freyd-Mitchell Embedding Theorem, Theorem 2.4 (standard reference, not scraped)
- The Stacks Project, Section 12.5, Lemma 12.5.2 (standard reference, not scraped)