TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28

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.

The canonical morphism from the coimage to the image exists and is unique

Statement

Let $f : A \to B$ be a morphism in a category with kernels and cokernels. Write $q_{f} : A \to coim (f)$ for the coimage projection and $i_{f} : im (f) \to B$ for the image inclusion. Then there exists a unique morphism

$\overline{f} : coim (f) \to im (f)$

such that

$i_{f} \circ \overline{f} \circ q_{f} = f .$

Facts & Assumptions

Given: A morphism $f : A \to B$ , its coimage projection $q_{f}$ , and its image inclusion $i_{f}$ .

[L1]

The morphism $f$ factors uniquely through its coimage (A morphism factors uniquely through its coimage).

[L2]

The morphism $f$ factors uniquely through its image (A morphism factors uniquely through its image).

[L3]

Every coequalizer is epic (Every equalizer is a monomorphism, and every coequalizer is an epimorphism).

Proof

technique · direct

1.1

By [L1], there is a unique morphism $\tilde{f} : coim (f) \to B$ with $\tilde{f} q_{f} = f$ . Let $c_{f} : B \to C_{f}$ be a cokernel of $f$ . Then $c_{f} \tilde{f} q_{f} = c_{f} f = 0$ , and [L3] makes $q_{f}$ epic, so $c_{f} \tilde{f} = 0$ . Because $i_{f} : im (f) \to B$ is a kernel of $c_{f}$ , there is a unique map $\overline{f} : coim (f) \to im (f)$ with $i_{f} \overline{f} = \tilde{f}$ .

L1L2L3

2.1

Composing the identity of step 1.1 with $q_{f}$ gives $i_{f} \overline{f} q_{f} = \tilde{f} q_{f} = f$ , so $\overline{f}$ has the required property. If another map $u : coim (f) \to im (f)$ also satisfies $i_{f} u q_{f} = f$ , then $i_{f} u = \tilde{f}$ by the epicity of $q_{f}$ from [L3], and the uniqueness of the kernel factorization in step 1.1 gives $u = \overline{f}$ .

L1L2L3step 1.1∎

Depends on

Used by

Dependency tree · two levels

6 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

Gautam Tamme, Algebra II Lecture 9, §9.1 (standard reference, not scraped)