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 generator detects comparison of subobjects
Statement
Let be a generator of an abelian category, and let be subobjects. Then
Facts & Assumptions
Given: A generator and subobjects , represented by monomorphisms and .
A generator separates distinct morphisms by precomposition (Generator and cogenerator of a category).
The meet is represented by the pullback of and (The meet of two subobjects is their pullback).
In an abelian category, a morphism that is both monic and epic is an isomorphism (An abelian category is balanced).
In a preadditive category with a zero object, a morphism is epic exactly when its cokernel is zero (In a preadditive category with a zero object, a morphism is epic exactly when its cokernel is zero).
Abelian categories have cokernels (Abelian category).
Proof
If , then any map factoring through also factors through by composition.
To prove the converse, assume . By [L2], let be the pullback subobject of and . If were epic, then [L3] would make it an isomorphism, forcing to factor through . So is not epic.
Let be a cokernel of , which exists by [L5]. Since is not epic, [L4] implies .
The morphisms and are therefore distinct, so [L1] gives some with . If factored through , the pullback property in [L2] would force to factor through , hence , impossible. Thus factors through but not through .
Step 1.1 proves the forward implication, and steps 1.2, 2.1, and 3.1 prove the contrapositive of the reverse implication. Therefore exactly when every morphism factoring through also factors through .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
15 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, Proposition 3.35 (standard reference, not scraped)