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 chain map carries cycles to cycles and boundaries to boundaries
Statement
Let be a chain map. For every there are induced morphisms compatible with the canonical inclusions into and .
Facts & Assumptions
Given: A chain map and an integer .
A chain map satisfies (Chain map).
Kernels are universal among arrows killed by the given morphism (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).
Write and as epic-monic factorizations, where and are the boundary inclusions (Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism).
In an abelian category, every monomorphism is the kernel of its cokernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).
Proof
Let and be the cycle inclusions. Using [L1], so [L2] yields a unique map with .
By [L3], Let be a cokernel of . Then Since is epic, this implies . By [L4], the monomorphism is a kernel of , so [L2] gives a unique morphism with This is the required boundary map.
Depends on
- Chain map
- Cycle and boundary subobjects of a complex
- Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers
- Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism
- Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel
Used by
Dependency tree · two levels
17 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
- Charles A. Weibel, Chapter 1 of An Introduction to Homological Algebra (standard reference, not scraped)
- Romyar Sharifi, Homological Algebra, Lemma 2.7.10 (standard reference, not scraped)