TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Third isomorphism theorem in an abelian category

Statement

Let $C \leq B \leq A$ be subobjects in an abelian category. Then there is a canonical isomorphism

$(A / C) / (B / C) ≅ A / B .$

Facts & Assumptions

Given: Subobjects $C \leq B \leq A$ represented by monomorphisms $c : C \to B$ and $b : B \to A$ .

[L1]

Quotients by subobjects are well defined (The quotient of an object by a subobject, The quotient by a subobject is independent of the chosen representing monomorphism).

[L2]

The first isomorphism theorem identifies a quotient by a kernel with the image (First isomorphism theorem in an abelian category).

[L3]

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

[L4]

Every monomorphism in an abelian category is a kernel of its cokernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

Proof

technique · direct

1.1L1

Let $q_{C} : A \to A / C$ and $q_{B} : A \to A / B$ be the quotient maps from [L1]. Since $q_{B} b c = 0$ , the morphism $q_{B}$ kills $C$ , so the universal property of $q_{C}$ gives a unique map $\overline{q} : A / C \to A / B$ with $\overline{q} q_{C} = q_{B}$ .

1.2givenL1L4

The composite $b c$ is monic: equality $b c u = b c v$ implies $c u = c v$ and then $u = v$ . By [L4], $b c$ is therefore a kernel of its cokernel $q_{C}$ . If $h : X \to B$ satisfies $q_{C} b h = 0$ , there is a unique $t : X \to C$ with $b c t = b h$ . Monicity of $b$ gives $c t = h$ , and monicity of $c$ gives uniqueness. Since $q_{C} b c = 0$ , this proves that $c$ is a kernel of $q_{C} b$ .

2.1L1L2L3step 1.1step 1.2

Let $p : B \to B / C$ be the cokernel of $c$ . By [L2], the canonical image factorization of $q_{C} b$ gives a monomorphism $\tilde{b} : B / C \to A / C$ satisfying $\tilde{b} p = q_{C} b$ . Since $p$ is epic by [L3] and $\overline{q} \tilde{b} p = q_{B} b = 0$ , we have $\overline{q} \tilde{b} = 0$ .

3.1L1L3step 1.1step 2.1∎

If $r : A / C \to Y$ satisfies $r \tilde{b} = 0$ , then $r q_{C} b = r \tilde{b} p = 0$ . The cokernel property of $q_{B}$ gives a unique $s : A / B \to Y$ with $s q_{B} = r q_{C}$ . Since $q_{B} = \overline{q} q_{C}$ and $q_{C}$ is epic, $s \overline{q} = r$ . Conversely, any $s$ satisfying this last equality satisfies $s q_{B} = r q_{C}$ , proving uniqueness. Thus $\overline{q}$ is a cokernel of $\tilde{b}$ , and [L1] identifies $(A / C) / (B / C)$ canonically with $A / B$ .

Depends on

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

Saunders Mac Lane, Categories for the Working Mathematician, VIII.3 (standard reference, not scraped)