TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29

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.

Members modulo equivalence correspond to subobjects

Statement

Let $A$ be an object of an abelian category. Sending a member $x : X \to A$ to the subobject of $A$ represented by its image inclusion induces a bijection between equivalence classes of members of $A$ and subobjects of $A$ .

Facts & Assumptions

Given: A member $x : X \to A$ and, when needed, a second member $y : Y \to A$ .

[L1]

Every morphism factors as an epimorphism followed by a monomorphism (Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism).

[L2]

Subobjects are mutual-factorization classes of monomorphisms (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms, Mutual factorisation is an equivalence relation on monomorphisms into an object and dually on epimorphisms out of it).

[L4]

Member equivalence is transitive (Equivalence of members, Member equivalence is transitive).

Proof

technique · direct

1.1L1L2construct

Factor $x$ as $X \overset{e_{x}}{\to} I_{x} \overset{m_{x}}{\to} A$ with $e_{x}$ epic and $m_{x}$ monic, using [L1], and assign to the class of $x$ the subobject $[⁣ m_{x} ⁣]$ of $A$ .

1.2L1L2

Every subobject is represented. If $m : S ↣ A$ is monic, then $m$ itself is a member of $A$ , and the factorization $S \overset{1_{S}}{\to} S \overset{m}{\to} A$ shows that its image class is $[⁣ m ⁣]$ .

2.1L1L2L4step 1.1

This assignment is well defined on equivalence classes. The equality $x 1_{X} = m_{x} e_{x}$ with epic maps on the right shows $x \equiv m_{x}$ , and similarly $y \equiv m_{y}$ . If $x \equiv y$ , then transitivity from [L4] gives $m_{x} \equiv m_{y}$ , which for monomorphisms into $A$ is exactly equality of subobject classes by [L2].

3.1L2L4step 2.1

The assignment is injective. If $x$ and $y$ determine the same subobject, then $[⁣ m_{x} ⁣] = [⁣ m_{y} ⁣]$ by [L2]. Step 2.1 gives $x \equiv m_{x}$ and $y \equiv m_{y}$ , while equality of subobjects makes $m_{x}$ and $m_{y}$ equivalent as members. Another use of [L4] yields $x \equiv y$ .

4.1step 1.2step 3.1∎

Therefore the assignment of step 1.1 is a bijection from member-equivalence classes to subobjects of $A$ .

Depends on

Dependency tree · 2 levels

Sources

Saunders Mac Lane, Categories for the Working Mathematician, VIII.4