DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)audited 2026-08-13

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.

Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers

Definition

Let $C$ be a category with specified zero morphisms (Category with zero morphisms), and let $f : A \to B$ .

The kernel of $f$ is an equalizer

$\ker (f) \overset{k}{\to} A \begin{array}{c} \overset{f}{\to} \\ \to_{0_{A, B}}^{} \end{array} B .$

The cokernel of $f$ is a coequalizer

$A \begin{array}{c} \overset{f}{\to} \\ \to_{0_{A, B}}^{} \end{array} B \overset{q}{\to} coker (f) .$

in the sense of Equalizers and coequalizers as limits and colimits of a parallel pair. Thus $f k = 0$ and every $h$ with $f h = 0$ factors uniquely through $k$ ; dually, $q f = 0$ and every $h$ with $h f = 0$ factors uniquely through $q$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 8 results over 5 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

E. Riehl, Category Theory in Context, Example 3.1.26 (standard reference, not scraped)