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 be a category with specified zero morphisms (Category with zero morphisms), and let .
The kernel of is an equalizer
The cokernel of is a coequalizer
in the sense of Equalizers and coequalizers as limits and colimits of a parallel pair. Thus and every with factors uniquely through ; dually, and every with factors uniquely through .
Depends on
Used by
- Gaussian cancellation preserves homotopy type and abelian-category homology Corollary
- Cohomology object of a cochain complex Definition
- Cycle and boundary subobjects of a complex Definition
- Homology object of a chain complex Definition
- Image and coimage in a category with kernels and cokernels Definition
- Normal monomorphisms and conormal epimorphisms Definition
- A chain map carries cycles to cycles and boundaries to boundaries Lemma
- The boundary subobject factors through the cycle subobject Lemma
- The cokernel of a chain map is computed degreewise Lemma
- The differential descends to a quotient complex Lemma
- The kernel of a chain map is computed degreewise Lemma
- The cokernel of the zero map out of the zero object is the target, and dually for kernels Proposition
- The kernel of a monomorphism is zero and the cokernel of an epimorphism is zero Proposition
- A chain map induces a well-defined map on homology Theorem
- Chain-homotopic maps induce the same map on homology Theorem
- Exactness of kernel and cokernel sequences under endpoint hypotheses Theorem
- Homology is an additive functor Theorem
- In a preadditive category with a zero object, a morphism is monic exactly when its kernel is zero Theorem
- In a preadditive category, the equalizer of a parallel pair is the kernel of their difference Theorem
- Snake lemma under the weaker Stacks hypotheses Theorem
- The arrow-theoretic criterion for exactness Theorem
- The connecting morphism exists and is unique Theorem
- The kernel-cokernel sequence of a composite Theorem
- The subobject inequalities underlying exactness Theorem
Dependency tree · two levels
4 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, Example 3.1.26 (standard reference, not scraped)