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.
Every equalizer is a monomorphism, and every coequalizer is an epimorphism
Statement
Every equalizer morphism is monic, and every coequalizer morphism is epic.
Facts & Assumptions
Given: An equalizer and a coequalizer .
An equalizer is the single nonidentity leg of a limiting cone, and a coequalizer is the single nonidentity leg of a colimiting cocone (Equalizers and coequalizers as limits and colimits of a parallel pair).
Limit legs are jointly monic and colimit legs are jointly epic (The legs of a limiting cone are jointly monic, and the legs of a colimiting cocone are jointly epic).
Proof
If , [F1] and the limiting clause of [L1] give ; hence is monic.
If , [F1] and the colimiting clause of [L1] give ; hence is epic.