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.

The subtraction surrogate

Statement

Let $g : B \to C$ be a morphism and let $x : X \to B$ , $y : Y \to B$ be members with $g x \equiv g y .$ Then there exists a member $z : Z \to B$ such that $g z \equiv 0.$

Moreover:

if $f : B \to D$ and $f x \equiv 0$ , then $f y \equiv f z$ ;
if $h : B \to A$ and $h y \equiv 0$ , then $h x \equiv - h z$ .

Facts & Assumptions

Given: Morphisms $g : B \to C$ , $f : B \to D$ , and $h : B \to A$ , and members $x : X \to B$ , $y : Y \to B$ with $g x \equiv g y$ .

[L1]

The relation $g x \equiv g y$ is witnessed by one common pair of epimorphisms (Equivalence of members).

[L2]

Every hom-set in an abelian category is an abelian group, so members with one common domain may be added and subtracted (Abelian category).

[L3]

Zero members and negatives behave literally under equivalence (Each object has a zero member and each member has a negative).

Proof

technique · constructive

1.1L1L2L3chooseconstructalgebra

Choose epimorphisms $u : W \to X$ and $v : W \to Y$ with $g x u = g y v$ , using [L1], and define $z : = y v - x u : W \to B$ . Then $g z = g y v - g x u = 0$ by [L2], so $g z \equiv 0$ by [L3].

2.1L1L2L3step 1.1constructalgebra

Suppose $f x \equiv 0$ . After replacing $W$ by a common epic refinement of the witnesses for $g x \equiv g y$ and $f x \equiv 0$ , we may assume $f x u = 0$ . Then $f y v = f (y v - x u) = f z$ , so the epic $v$ witnesses $f y \equiv f z$ .

2.2L1L2L3step 1.1constructalgebra

Suppose $h y \equiv 0$ . After the same common-refinement step, we may assume $h y v = 0$ . Then $h x u = - h (y v - x u) = - h z$ , so the epic $u$ witnesses $h x \equiv - h z$ .

3.1step 1.1step 2.1step 2.2discharge-construct∎

Step 1.1 gives the required member $z$ , while steps 2.1 and 2.2 prove the two moreover clauses.

Depends on

Used by

FALSE: the members of an object form an abelian group False statement
FALSE: the subtraction rule produces a unique member False statement
The cost of the member calculus Remark
Two routes to every dual statement Remark
What the subtraction rule does not say Remark

Dependency tree · two levels

12 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, Theorem VIII.4.3(vi) (standard reference, not scraped)