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.
Depends on
Used by
- Gaussian cancellation preserves homotopy type and abelian-category homology Corollary
- The coimage projection is epic and the image inclusion is monic Proposition
- A complete locally small category with a jointly weakly initial set has an initial object, without class-indexed choice Theorem
- A complete locally small category with a small coseparating set and intersections of all subobject collections has an initial object Theorem
- A short exact sequence is a kernel-cokernel pair Theorem
- Degenerate exactness criteria Theorem
- Exactness of kernel and cokernel sequences under endpoint hypotheses Theorem
- Freyd's axioms force the additive structure and recover the AB2 definition Theorem
- The canonical morphism from the coimage to the image exists and is unique Theorem
- The kernel row and cokernel row of a morphism of short exact sequences are exact at two nodes each Theorem
- The kernel-cokernel sequence of a composite Theorem
- Third isomorphism theorem in an abelian category Theorem
Dependency tree · two levels
5 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
- E. Riehl, Category Theory in Context, Exercise 3.1.iv (standard reference, not scraped)