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.

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).

Proof

technique · direct

1.1

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.2

The composite $q_{C} b : B \to A / C$ kills $C$ , since $q_{C} b c = q_{C} (b c) = 0$ . Conversely, if $h : X \to B$ satisfies $q_{C} b h = 0$ , then $b h$ is killed by $q_{C}$ , so the cokernel property of $q_{C}$ makes $b h$ factor through $b c$ . Because $b$ is monic, $h$ factors through $c$ . Thus $c : C \to B$ is a kernel of $q_{C} b$ , and [L2] identifies the image of $q_{C} b$ with $B / C$ . Let $\tilde{b} : B / C \to A / C$ be the corresponding monic image inclusion. Then $\overline{q} \tilde{b} = 0$ , because $\overline{q} q_{C} b = q_{B} b = 0$ .

L1L2

2.1

If $r : A / C \to Y$ satisfies $r \tilde{b} = 0$ , then $r q_{C} b = 0$ , so $r q_{C}$ kills $B$ . Since $q_{B}$ is the cokernel of $B \to A$ , there is a unique $s : A / B \to Y$ with $s q_{B} = r q_{C}$ . Using $q_{B} = \overline{q} q_{C}$ and the epicity of $q_{C}$ from [L3], one gets $s \overline{q} = r$ . Thus $\overline{q}$ is the cokernel of $\tilde{b}$ , so by [L1] the quotient $(A / C) / (B / C)$ is canonically $A / B$ .

L1L3step 1.1step 1.2∎

Depends on

Used by

The third isomorphism theorem in abelian groups matches the categorical statement Example

Dependency tree · two levels

13 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)