Session-authored (Fable 5 assisted)

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.

✓ 39 results · all verified · 14 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 25 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Exactness and the Member Calculus

1 · Prerequisites

2 · Summary

This page is the arrow-theoretic bridge between abstract abelian-category structure and the diagram chases that follow. It first pins down exactness as a precise comparison of image and kernel subobjects, then packages the same data into the member calculus and the covering criterion, and finally records the kernel/cokernel exactness lemmas and Hom exactness facts that later diagram lemmas spend directly.

The page also keeps its own guard rails visible. Members are weaker than elements, the subtraction rule is weaker than actual subtraction, and short exactness depends on compatible structure rather than an abstract isomorphism of the middle object.

3 · Logical flowchart

4 · Definitions, theorems and proofs

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

The subobject inequalities underlying exactness

Statement

Let $A \overset{f}{\to} B \overset{g}{\to} C$ be composable morphisms in an abelian category. Choose an epi-mono factorization $A \overset{e}{\to} im (f) \overset{m}{\to} B$ of $f$ , and choose a kernel $K \overset{k}{\to} B$ of $g$ .

Then:

$[⁣ m ⁣] \leq [⁣ k ⁣]$ if and only if $g f = 0$ .
$[⁣ k ⁣] \leq [⁣ m ⁣]$ if and only if every morphism $u : U \to B$ with $g u = 0$ factors through $m$ .

Facts & Assumptions

Given: The composable pair $A \overset{f}{\to} B \overset{g}{\to} C$ , the factorization $f = m e$ with $e$ epic and $m$ monic, and the kernel $k : K \to B$ of $g$ .

[L1]

Every morphism in an abelian category admits an epimorphism-monomorphism factorization, unique up to unique isomorphism (Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism).

[L2]

Subobjects are ordered by factorization of monomorphisms, and the image is the least subobject through which the morphism factors (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms, The image is the least subobject through which a morphism factors).

[L3]

The kernel $k$ satisfies $g k = 0$ , and every morphism killed by $g$ factors uniquely through $k$ (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

Proof

technique · direct

1.1

If $[⁣ m ⁣] \leq [⁣ k ⁣]$ , then $m = k t$ for some $t : im (f) \to K$ by [L2], so $g f = g m e = g k t e = 0$ by [L3].

L2L3algebra

1.2

If $g f = 0$ , then $g m e = 0$ , and the epicity of $e$ from [L1] gives $g m = 0$ . So [L3] gives $t : im (f) \to K$ with $k t = m$ , hence $[⁣ m ⁣] \leq [⁣ k ⁣]$ by [L2].

L1L2L3algebra

1.3

If $[⁣ k ⁣] \leq [⁣ m ⁣]$ , then $k = m s$ for some $s : K \to im (f)$ by [L2]. For any $u : U \to B$ with $g u = 0$ , [L3] gives $v : U \to K$ with $u = k v = m s v$ , so $u$ factors through $m$ .

L2L3

1.4

Conversely, if every $u : U \to B$ with $g u = 0$ factors through $m$ , then in particular the kernel arrow $k$ does, because $g k = 0$ by [L3]. Thus $k = m s$ for some $s$ , so $[⁣ k ⁣] \leq [⁣ m ⁣]$ by [L2].

L2L3

2.1

Steps 1.1 and 1.2 prove the first biconditional.

step 1.1step 1.2

3.1

Steps 1.3 and 1.4 prove the second biconditional.

step 1.3step 1.4∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-29Open item page →

Exactness at a node

Definition

Let $A \overset{f}{\to} B \overset{g}{\to} C$ be composable morphisms in an abelian category.

The pair is exact at $B$ when the image of $f$ and the kernel of $g$ represent the same subobject of $B$ : $[im (f)] = [\ker (g)] .$

Equivalently, by the dual description in the opposite abelian category (The opposite of an abelian category is abelian) together with the definitions of image and coimage (Image and coimage in a category with kernels and cokernels), the pair is exact at $B$ exactly when the cokernel of $f$ and the coimage of $g$ represent the same quotient of $B$ : $[coker (f)] = [coim (g)] .$

The well-definedness of the first equality as a comparison of subobjects is exactly the content of The subobject inequalities underlying exactness ↗.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

The arrow-theoretic criterion for exactness

Statement

Let $A \overset{f}{\to} B \overset{g}{\to} C$ be composable morphisms in an abelian category, let $K \overset{k}{\to} B$ be a kernel of $g$ , and let $B \overset{q}{\to} Q$ be a cokernel of $f$ .

Then the pair is exact at $B$ if and only if both $g f = 0 and q k = 0.$

Facts & Assumptions

Given: The composable pair $A \overset{f}{\to} B \overset{g}{\to} C$ , a kernel $k : K \to B$ of $g$ , and a cokernel $q : B \to Q$ of $f$ .

[L1]

Exactness at $B$ means $[im (f)] = [\ker (g)]$ , equivalently $[coker (f)] = [coim (g)]$ (Exactness at a node, Image and coimage in a category with kernels and cokernels).

[L2]

For the image factorization $f = m e$ , one has $[⁣ m ⁣] \leq [⁣ k ⁣]$ if and only if $g f = 0$ , and $[⁣ k ⁣] \leq [⁣ m ⁣]$ if and only if every morphism killed by $g$ factors through $m$ (The subobject inequalities underlying exactness).

[L3]

Kernels and cokernels are characterized by the usual vanishing and universal factorization properties (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

Proof

technique · direct

1.1

Assume the pair is exact at $B$ . Then $[im (f)] = [\ker (g)]$ , so [L2] gives $g f = 0$ .

L1L2

1.2

Write $f = m e$ for an image factorization. Exactness gives $k = m u$ for some $u : K \to im (f)$ , and $q f = q m e = 0$ implies $q m = 0$ because $e$ is epic. Hence $q k = q m u = 0$ .

L1L2L3algebra

1.3

Assume now that $g f = 0$ and $q k = 0$ . Writing again $f = m e$ , the equality $g f = 0$ gives $[⁣ m ⁣] \leq [⁣ k ⁣]$ by [L2].

2.1

Since $q f = q m e = 0$ and $e$ is epic, one has $q m = 0$ . Together with the hypothesis $q k = 0$ , the cokernel property in [L3] yields $u : K \to im (f)$ with $m u = k$ , hence $[⁣ k ⁣] \leq [⁣ m ⁣]$ .

L3step 1.3algebra

3.1

Steps 1.3 and 2.1 give $[im (f)] = [\ker (g)]$ , so the pair is exact at $B$ by [L1]. With steps 1.1 and 1.2, this proves the equivalence.

L1step 1.1step 1.2step 1.3step 2.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Exact sequence and short exact sequence in an abelian category

Definition

A sequence of morphisms in an abelian category is exact when it is exact at every interior object in the sense of Exactness at a node.

In particular, a composable triple $0 \to A \overset{i}{\to} B \overset{p}{\to} C \to 0$ is a short exact sequence when it is exact at $A$ , at $B$ , and at $C$ .

This page uses the sequence language literally: the definition names exactness of displayed chains of morphisms, not chain complexes as objects.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

A short exact sequence is a kernel-cokernel pair

Statement

For morphisms $0 \to A \overset{i}{\to} B \overset{p}{\to} C \to 0$ in an abelian category, the following are equivalent:

the sequence is short exact;
$i$ is a kernel of $p$ and $p$ is a cokernel of $i$ .

Facts & Assumptions

Given: Morphisms $i : A \to B$ and $p : B \to C$ in an abelian category.

[L1]

A short exact sequence is exact at $A$ , $B$ , and $C$ (Exact sequence and short exact sequence in an abelian category).

[L2]

Exactness at a node can be tested by the two arrow equalities $g f = 0$ and $q k = 0$ (The arrow-theoretic criterion for exactness).

[L3]

In an abelian category, a morphism is monic exactly when its kernel is zero, and epic exactly when its cokernel is zero (In an abelian category, monic means zero kernel and epic means zero cokernel).

[L4]

The identity of $A$ is a cokernel of $0 \to A$ , and dually the identity of $C$ is a kernel of $C \to 0$ (The cokernel of the zero map out of the zero object is the target, and dually for kernels).

[L5]

Exactness at $B$ gives both $[im (i)] = [\ker (p)]$ and $[coker (i)] = [coim (p)]$ (Exactness at a node).

[L6]

Every epimorphism is the cokernel of its kernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

[L7]

Kernels are monic and cokernels are epic (Every equalizer is a monomorphism, and every coequalizer is an epimorphism).

Proof

technique · direct

1.1

Assume the displayed sequence is short exact. Exactness at $A$ and [L4] make the arrow criterion [L2] read $1_{A} k = 0$ for a kernel $k$ of $i$ , so $\ker (i) = 0$ and [L3] makes $i$ monic. Dually, exactness at $C$ gives $coker (p) = 0$ , so $p$ is epic.

L1L2L3L4

1.2

Conversely, assume $i$ is a kernel of $p$ and $p$ is a cokernel of $i$ . Then [L7] makes $i$ monic and $p$ epic, so [L3] gives endpoint exactness. Also $p i = 0$ , and if $k$ is a kernel of $p$ while $q$ is a cokernel of $i$ , then $k$ factors through $i$ , hence $q k = 0$ because $q i = 0$ . Thus [L2] gives exactness at $B$ , so the sequence is short exact.

L2L3L7

2.1

Exactness at $B$ gives $p i = 0$ by [L2]. Since $i$ is monic by step 1.1, the factorization $i = i 1_{A}$ is an epi-mono factorization of $i$ , so every $u : U \to B$ with $p u = 0$ factors through $i$ . Thus $i$ is a kernel of $p$ .

L2step 1.1

2.2

The same exactness at $B$ , read through the second equality in [L5], identifies $coker (i)$ with $coim (p)$ . Because step 1.1 makes $p$ epic, [L6] says that $p$ itself represents $coim (p)$ . Hence $p$ represents the quotient $coker (i)$ , which is exactly to say that $p$ is a cokernel of $i$ .

L5L6step 1.1

3.1

Steps 1.1 and 2.1 show that short exactness forces $i$ to be the kernel of $p$ .

step 1.1step 2.1

4.1

Steps 2.2 and 1.2 complete the equivalence.

step 2.2step 1.2∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Degenerate exactness criteria

Statement

In an abelian category:

$0 \to K \overset{u}{\to} A$ is exact if and only if $u$ is monic.
$0 \to K \overset{u}{\to} A \overset{v}{\to} B$ is exact if and only if $u$ is a kernel of $v$ .
$A \overset{v}{\to} B \overset{w}{\to} C \to 0$ is exact if and only if $w$ is a cokernel of $v$ .
$0 \to A \overset{u}{\to} B \overset{v}{\to} C \to 0$ is exact if and only if $u$ is monic and $v$ is a cokernel of $u$ , equivalently if and only if $u$ is a kernel of $v$ and $v$ is epic.

Facts & Assumptions

Given: Morphisms in an abelian category as displayed in the statement.

[L1]

Exactness of the displayed sequences is the sequence notion of Exact sequence and short exact sequence in an abelian category.

[L2]

Exactness at a node means image equals kernel, equivalently cokernel equals coimage (Exactness at a node).

[L3]

Monomorphisms are exactly the zero-kernel morphisms, and epimorphisms are exactly the zero-cokernel morphisms (In an abelian category, monic means zero kernel and epic means zero cokernel).

[L4]

Equalizers are monic and coequalizers are epic (Every equalizer is a monomorphism, and every coequalizer is an epimorphism).

[L5]

Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

Proof

technique · direct

1.1

Exactness of $0 \to K \overset{u}{\to} A$ says that the kernel of $u$ is the zero subobject, and [L3] identifies that with $u$ being monic. This proves claim 1.

L1L2L3

1.2

For claim 3, first assume $A \overset{v}{\to} B \overset{w}{\to} C \to 0$ is exact. Exactness at $C$ says the cokernel of $w$ is zero, so [L3] makes $w$ epic. Exactness at $B$ gives $[coker (v)] = [coim (w)]$ by [L2]. Because $w$ is epic, [L5] says that $w$ itself represents $coim (w)$ . Hence $w$ is a cokernel of $v$ . Conversely, if $w$ is a cokernel of $v$ , then [L4] makes $w$ epic, so exactness at $C$ follows from [L3]. Also $w$ itself represents $coim (w)$ , so exactness at $B$ is exactly [L2]. This proves claim 3.

L2L3L4L5

2.1

For claim 2, first assume $0 \to K \overset{u}{\to} A \overset{v}{\to} B$ is exact. By step 1.1, $u$ is monic. Exactness at $A$ gives $[im (u)] = [\ker (v)]$ by [L2], and for a monomorphism the image representative is $u$ itself. Hence $u$ represents the same subobject as a kernel of $v$ , so $u$ is a kernel of $v$ . Conversely, if $u$ is a kernel of $v$ , then $u$ is monic by [L4] and therefore exactness at $K$ follows from step 1.1. Since $u$ itself represents $\ker (v)$ , exactness at $A$ is exactly [L2]. This proves claim 2.

L2L4step 1.1

2.2

If $u$ is monic and $v$ is a cokernel of $u$ , then step 1.1 gives exactness of $0 \to A \overset{u}{\to} B$ , and claim 3 gives exactness of $A \overset{u}{\to} B \overset{v}{\to} C \to 0$ . Hence the full sequence is short exact.

step 1.1step 1.2

3.1

If $0 \to A \overset{u}{\to} B \overset{v}{\to} C \to 0$ is short exact, then claims 2 and 3 give that $u$ is a kernel of $v$ and $v$ is a cokernel of $u$ .

step 2.1step 1.2

3.2

If $u$ is a kernel of $v$ and $v$ is epic, then claim 2 gives exactness of $0 \to A \overset{u}{\to} B \overset{v}{\to} C$ , and [L3] turns the epicity of $v$ into exactness at $C$ . Hence the full sequence is short exact.

L3step 2.1

4.1

Steps 3.1, 2.2, and 3.2 prove claim 4.

step 3.1step 2.2step 3.2∎

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Exactness is self-dual

Statement

A composable pair $A \overset{f}{\to} B \overset{g}{\to} C$ is exact at $B$ in an abelian category $A$ if and only if the opposite pair $C \overset{g^{o p}}{\to} B \overset{f^{o p}}{\to} A$ is exact at $B$ in $A^{o p}$ .

Facts & Assumptions

Given: A composable pair $A \overset{f}{\to} B \overset{g}{\to} C$ in an abelian category $A$ .

[L1]

The opposite of an abelian category is abelian (The opposite of an abelian category is abelian).

[L2]

Exactness at $B$ means either $[im (f)] = [\ker (g)]$ or, equivalently, $[coker (f)] = [coim (g)]$ (Exactness at a node, Image and coimage in a category with kernels and cokernels).

Proof

technique · direct

1.1

By [L1], the opposite category $A^{o p}$ is again abelian, so the definition [L2] applies there. Passing to the opposite exchanges kernels with cokernels and images with coimages.

L1L2

2.1

Therefore the equality $[im (f)] = [\ker (g)]$ in $A$ is exactly the equality $[im (g^{o p})] = [\ker (f^{o p})]$ in $A^{o p}$ . By [L2], those are the two exactness assertions.

L2step 1.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Split short exact sequence in an abelian category

Definition

A short exact sequence $0 \to A \overset{i}{\to} B \overset{p}{\to} C \to 0$ in an abelian category is split when there exist morphisms $s : C \to B, π : B \to A$ such that $p s = 1_{C}, π i = 1_{A}, i π + s p = 1_{B} .$

Equivalently, the five-tuple $(B, i, s, π, p)$ is the biproduct diagram of $A$ and $C$ in the sense of Biproduct. The point of the definition is the displayed compatible structure, not merely an abstract isomorphism $B ≅ A \oplus C$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

Splitting lemma in an abelian category

Statement

Let $0 \to A \overset{i}{\to} B \overset{p}{\to} C \to 0$ be a short exact sequence in an abelian category.

If $s : C \to B$ satisfies $p s = 1_{C}$ , then there is a unique morphism $π : B \to A$ such that $π i = 1_{A}, i π + s p = 1_{B} .$
If $π : B \to A$ satisfies $π i = 1_{A}$ , then there is a unique morphism $s : C \to B$ such that $p s = 1_{C}, i π + s p = 1_{B} .$

In either case the sequence is split.

Facts & Assumptions

Given: The short exact sequence in the statement.

[L1]

In a short exact sequence, $i$ is a kernel of $p$ and $p$ is a cokernel of $i$ (A short exact sequence is a kernel-cokernel pair).

[L2]

A split short exact sequence is exactly one equipped with maps $s, π$ satisfying $p s = 1_{C}$ , $π i = 1_{A}$ , and $i π + s p = 1_{B}$ (Split short exact sequence in an abelian category).

Proof

technique · constructive

1.1

Assume $p s = 1_{C}$ and put $t : = 1_{B} - s p$ . Then $p t = 0$ , so because $i$ is a kernel of $p$ by [L1], there is a unique $π : B \to A$ with $i π = t = 1_{B} - s p$ .

L1givenconstructalgebra

1.2

Conversely assume $π i = 1_{A}$ and put $u : = 1_{B} - i π$ . Then $u i = 0$ , so because $p$ is a cokernel of $i$ by [L1], there is a unique $s : C \to B$ with $s p = u = 1_{B} - i π$ .

L1givenconstructalgebra

2.1

Composing $i π = 1_{B} - s p$ with $i$ gives $i π i = i - s p i = i$ , because $p i = 0$ by [L1]. Since $i$ is monic, $π i = 1_{A}$ , and the defining equation also yields $i π + s p = 1_{B}$ .

L1step 1.1algebra

2.2

Composing $s p = 1_{B} - i π$ with $p$ gives $p s p = p$ , and epicity of $p$ forces $p s = 1_{C}$ . The same equation already gives $i π + s p = 1_{B}$ .

L1step 1.2algebra

3.1

If $π^{'}$ satisfies the same two identities, then $i π^{'} = 1_{B} - s p = i π$ , so monicity of $i$ gives $π^{'} = π$ . Hence the map is unique, and [L2] says the sequence is split.

L1L2step 1.1step 2.1

3.2

If $s^{'}$ satisfies the same two identities, then $s^{'} p = 1_{B} - i π = s p$ , so epicity of $p$ gives $s^{'} = s$ . Hence the map is unique, and [L2] again says the sequence is split.

L1L2step 1.2step 2.2

4.1

Steps 1.1 to 3.1 prove claim 1, and steps 1.2 to 3.2 prove claim 2.

step 1.1step 2.1step 3.1step 1.2step 2.2step 3.2discharge-construct∎

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Member of an object

Definition

Let $A$ be an object of a category. A member of $A$ is simply a morphism with codomain $A$ .

Thus a member is written $x : X \to A,$ and one may read this as " $x$ is a member of $A$ with domain $X$ ". The point of the terminology is that an abelian category need not have honest elements, but it always has arrows into an object.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Equivalence of members

Definition

Let $x : X \to A$ and $y : Y \to A$ be members of the same object $A$ .

They are equivalent, written $x \equiv y,$ when there exist an object $W$ and epimorphisms $u : W ↠ X, v : W ↠ Y$ such that $x u = y v .$

So equivalence of members is equality after comparison on one common epimorphic cover of the two domains.

PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Member equivalence is reflexive and symmetric

Statement

For members of one object, the relation $\equiv$ is reflexive and symmetric.

Facts & Assumptions

Given: Members $x : X \to A$ and $y : Y \to A$ .

[L1]

By definition, $x \equiv y$ means there are epimorphisms $u : W \to X$ and $v : W \to Y$ with $x u = y v$ (Equivalence of members).

Proof

technique · direct

1.1

Reflexivity uses $W = X$ with $u = v = 1_{X}$ . The identity is epic and $x 1_{X} = x 1_{X}$ , so $x \equiv x$ by [L1].

L1algebra

1.2

If $x \equiv y$ , choose $W, u, v$ as in [L1] with $x u = y v$ . Reading the same equality backwards gives $y v = x u$ , so $y \equiv x$ .

2.1

Therefore the member relation is reflexive and symmetric.

step 1.1step 1.2∎

TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Member equivalence is transitive

Statement

For members of one object in an abelian category, the relation $\equiv$ is transitive.

Facts & Assumptions

Given: An abelian category and members $x : X \to A$ , $y : Y \to A$ , and $z : Z \to A$ with $x \equiv y$ and $y \equiv z$ .

[L1]

The relation $x \equiv y$ is witnessed by epimorphisms from one common domain as in Equivalence of members.

[L2]

Pullbacks exist in an abelian category (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L3]

The pullback of an epimorphism is an epimorphism (The pullback of an epimorphism is an epimorphism).

Proof

technique · direct

1.1

Choose epimorphisms $u : W_{1} \to X$ , $v : W_{1} \to Y$ , $w : W_{2} \to Y$ , and $r : W_{2} \to Z$ with $x u = y v$ and $y w = z r$ , using [L1].

L1choose

1.2

Form the pullback of $v$ and $w$ , with projections $v^{'} : P \to W_{1}$ and $w^{'} : P \to W_{2}$ . By [L3], both $v^{'}$ and $w^{'}$ are epic.

L2L3construct

2.1

The pullback equation gives $v v^{'} = w w^{'}$ , so $x u v^{'} = y v v^{'} = y w w^{'} = z r w^{'}$ . Hence the epimorphisms $u v^{'} : P \to X$ and $r w^{'} : P \to Z$ witness $x \equiv z$ .

L1step 1.1step 1.2algebra

3.1

Therefore member equivalence is transitive.

step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

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

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

L1L2construct

1.2

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 ⁣]$ .

L1L2

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

L1L2L4step 1.1

3.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$ .

L2L4step 2.1

4.1

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

step 1.2step 3.1∎

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Each object has a zero member and each member has a negative

Statement

For every object $A$ of an abelian category:

there is a zero member of $A$ ;
every member $x : X \to A$ has a negative member $- x : X \to A$ ;
for every member $x$ , one has $x \equiv 0$ if and only if $x = 0$ as a morphism.

Facts & Assumptions

Given: An abelian category and a member $x : X \to A$ .

[L1]

A zero object supplies zero morphisms between any two objects (A zero object supplies a unique compatible system of zero morphisms).

[L2]

An abelian category is additive, so every hom-set has negatives (Abelian category).

[L3]

Member equivalence is defined by comparison after epimorphisms (Equivalence of members).

Proof

technique · direct

1.1

By [L1], there is a zero morphism $0_{X, A} : X \to A$ , so $A$ has a zero member. By [L2], the additive inverse $- x : X \to A$ exists, so every member has a negative.

L1L2

1.2

Conversely, if $x \equiv 0$ , choose epimorphisms $u : W \to X$ and $v : W \to Y$ witnessing that equivalence. Then $x u = 0$ , and epicity of $u$ forces $x = 0$ .

L3assume-hypalgebra

2.1

If $x = 0$ , then $x \equiv 0$ is witnessed by the identity epic $1_{X} : X \to X$ , since $x 1_{X} = 01_{X}$ .

L3step 1.1

3.1

Step 1.1 proves claims 1 and 2, while steps 2.1 and 1.2 prove claim 3.

step 1.1step 2.1step 1.2∎

PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A morphism carries members to members and preserves equivalence

Statement

Let $f : A \to B$ be a morphism.

If $x : X \to A$ is a member of $A$ , then $f x : X \to B$ is a member of $B$ .
If $x \equiv y$ as members of $A$ , then $f x \equiv f y$ as members of $B$ .

Facts & Assumptions

Given: A morphism $f : A \to B$ and members $x : X \to A$ , $y : Y \to A$ .

[L1]

Member equivalence means equality after precomposition by one common pair of epimorphisms (Equivalence of members).

Proof

technique · direct

1.1

The composite $f x : X \to B$ is again a morphism into $B$ , so it is a member of $B$ .

given

1.2

If $x \equiv y$ , choose epimorphisms $u : W \to X$ and $v : W \to Y$ with $x u = y v$ by [L1]. Postcomposing with $f$ gives $f x u = f y v$ , and the same epimorphisms witness $f x \equiv f y$ .

L1algebra

2.1

Therefore every morphism carries members to members and preserves their equivalence.

step 1.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Monicity is detected by members

Statement

For a morphism $f : A \to B$ in an abelian category, the following are equivalent:

$f$ is monic.
For every member $x : X \to A$ , the implication $f x \equiv 0 ⟹ x \equiv 0$ holds.

Facts & Assumptions

Given: A morphism $f : A \to B$ .

[L1]

Monomorphisms are left-cancellable (Monomorphism and epimorphism by left and right cancellation).

[L2]

A member equivalent to zero is literally the zero morphism, and every member has a zero comparison member (Each object has a zero member and each member has a negative).

[L3]

Postcomposition preserves member equivalence (A morphism carries members to members and preserves equivalence).

Proof

technique · direct

1.1

Assume $f$ is monic, and let $x : X \to A$ satisfy $f x \equiv 0$ . Choose an epic $u : W \to X$ witnessing this, so $f x u = 0$ . Since $f$ is monic, $x u = 0$ , and the same epic $u$ witnesses $x \equiv 0$ .

L1L2assume-hypalgebra

1.2

Assume condition 2. If $u, v : U \to A$ satisfy $f u = f v$ , then for the member $x : = u - v$ one has $f x = f u - f v = 0$ , hence $f x \equiv 0$ by [L2] and [L3]. Condition 2 gives $x \equiv 0$ , so [L2] makes $x = 0$ , namely $u = v$ . Thus $f$ is monic by [L1].

L1L2L3assume-hypalgebra

2.1

Therefore the two conditions are equivalent.

step 1.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Monicity by member cancellation

Statement

For a morphism $f : A \to B$ in an abelian category, the following are equivalent:

$f$ is monic.
For all members $x$ and $y$ of $A$ , $f x \equiv f y ⟹ x \equiv y .$

Facts & Assumptions

Given: A morphism $f : A \to B$ .

[L1]

Monicity is equivalent to the rule $f z \equiv 0 \Rightarrow z \equiv 0$ (Monicity is detected by members).

[L2]

Members have negatives, and equivalence to zero means literal zero after a common epic comparison (Each object has a zero member and each member has a negative).

Proof

technique · direct

1.1

Assume $f$ is monic, and suppose $f x \equiv f y$ . Choose a common witness $u : W \to X$ , $v : W \to Y$ with $f x u = f y v$ . Then $f (x u - y v) = 0$ , so [L1] gives $x u - y v \equiv 0$ . By [L2], this means $x u = y v$ , hence $x \equiv y$ .

L1L2assume-hypalgebra

1.2

Conversely, assume condition 2. Apply it with $y$ equal to the zero member on the same domain as $x$ . Then $f x \equiv 0$ implies $x \equiv 0$ , so [L1] makes $f$ monic.

L1L2assume-hyp

2.1

Therefore conditions 1 and 2 are equivalent.

step 1.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Epimorphy is detected by members

Statement

For a morphism $g : B \to C$ in an abelian category, the following are equivalent:

$g$ is epic.
For every member $z : Z \to C$ , there exists a member $y : Y \to B$ with $g y \equiv z .$

Facts & Assumptions

Given: A morphism $g : B \to C$ .

[L1]

Members modulo equivalence correspond exactly to subobjects (Members modulo equivalence correspond to subobjects).

[L3]

The image is the least subobject through which a morphism factors (The image is the least subobject through which a morphism factors).

[L4]

Pullbacks exist, and pullbacks of epimorphisms are epimorphisms (Pullbacks and pushouts as limits and colimits of cospans and spans, The pullback of an epimorphism is an epimorphism).

Proof

technique · direct

1.1

Assume $g$ is epic. For a member $z : Z \to C$ , form the pullback of $z$ along $g$ with projections $y : P \to B$ and $α : P \to Z$ . By [L4], $α$ is epic, and the pullback equation $g y = z α$ shows $g y \equiv z$ .

L4assume-hypconstruct

1.2

Assume condition 2, and write $g$ as an epi-mono factorization $B \overset{e}{\to} I \overset{m}{\to} C$ . Apply condition 2 to the identity member $1_{C} : C \to C$ . Then there is $y : Y \to B$ with $g y \equiv 1_{C}$ , so [L1] says that $g y$ and $1_{C}$ determine the same whole subobject of $C$ . Since $g y$ factors through $g$ , [L3] gives $[im (g y)] \leq [im (g)] = [⁣ m ⁣]$ , hence $[1_{C}] \leq [⁣ m ⁣]$ , which forces $[⁣ m ⁣] = [1_{C}]$ . Thus $g$ is epic.

L1L3assume-hypalgebra

2.1

Therefore conditions 1 and 2 are equivalent.

step 1.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

A zero arrow is detected by members

Statement

A morphism $h : R \to S$ in an abelian category is the zero morphism if and only if $h x \equiv 0$ for every member $x$ of $R$ .

Facts & Assumptions

Given: A morphism $h : R \to S$ .

[L1]

The zero member exists, and a member equivalent to zero is literally zero (Each object has a zero member and each member has a negative).

Proof

technique · direct

1.1

If $h = 0$ , then for every member $x$ one has $h x = 0$ , hence $h x \equiv 0$ by [L1].

L1algebra

1.2

Conversely, assume $h x \equiv 0$ for every member $x$ of $R$ . Apply this to the identity member $1_{R} : R \to R$ . Then $h = h 1_{R} \equiv 0$ , so [L1] forces $h = 0$ .

L1assume-hyp

2.1

Therefore the displayed member criterion detects exactly the zero morphism.

step 1.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Exactness is detected by members

Statement

For a composable pair $A \overset{f}{\to} B \overset{g}{\to} C$ in an abelian category, the following are equivalent:

the pair is exact at $B$ ;
$g f = 0$ , and for every member $y : Y \to B$ with $g y \equiv 0$ there exists a member $x : X \to A$ with $f x \equiv y .$

Facts & Assumptions

Given: The composable pair $A \overset{f}{\to} B \overset{g}{\to} C$ .

[L1]

Exactness at $B$ is the equality $[im (f)] = [\ker (g)]$ (Exactness at a node).

[L2]

The subobject inequalities underlying exactness are exactly the two factorization statements for morphisms killed by $g$ (The subobject inequalities underlying exactness).

[L3]

Members modulo equivalence correspond to subobjects (Members modulo equivalence correspond to subobjects).

[L4]

Pullbacks of epimorphisms are epimorphisms (Pullbacks and pushouts as limits and colimits of cospans and spans, The pullback of an epimorphism is an epimorphism).

[L5]

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

Proof

technique · direct

1.1

Assume the pair is exact at $B$ , and let $y : Y \to B$ satisfy $g y \equiv 0$ . Choose an epic $u : W \to Y$ with $g y u = 0$ . If $A \overset{e}{\to} I \overset{m}{\to} B$ is an image factorization of $f$ , then exactness and [L2] give a map $w : W \to I$ with $m w = y u$ .

L1L2L5assume-hypchoose

1.2

Assume condition 2. For any $u : U \to B$ with $g u = 0$ , we have $g u \equiv 0$ , so condition 2 gives a member $x : X \to A$ with $f x \equiv u$ . By [L3], the members $f x$ and $u$ determine the same subobject of $B$ , and since $f x$ factors through $f$ , that subobject lies below the image of $f$ . Thus every morphism killed by $g$ factors through the image of $f$ . Together with $g f = 0$ , [L2] yields exactness at $B$ .

L2L3L5assume-hyp

2.1

Pull back the epic $e : A \to I$ along $w$ , obtaining $x : P \to A$ and an epic $α : P \to W$ by [L4]. Then $f x = m e x = m w α = y u α$ , so $f x \equiv y$ .

L4L5step 1.1constructalgebra

3.1

Thus conditions 1 and 2 are equivalent.

step 2.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

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

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

L1L2L3chooseconstructalgebra

2.1

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

L1L2L3step 1.1constructalgebra

2.2

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

L1L2L3step 1.1constructalgebra

3.1

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

step 1.1step 2.1step 2.2discharge-construct∎

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

What the subtraction rule does not say

Remark

The member $z$ in The subtraction surrogate is an existence statement, not a canonical difference. The theorem does not assert uniqueness of $z$ , does not endow member classes with a binary subtraction law, and does not say anything about an arbitrary morphism $k : B \to E$ applied to $z$ .

What it does control is narrower and exactly sufficient for diagram chasing: $z$ is killed by $g$ , and it is related to $x$ and $y$ only through morphisms that already kill one of them.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

The cost of the member calculus

The member calculus uses only the abelian-category primitives already on the page: finite limits and finite colimits, additivity on hom-sets, and one genuinely nonformal stability statement, The pullback of an epimorphism is an epimorphism, which is exactly what makes member equivalence transitive.

What it does not use is equally important: no choice principle, no generator, no projectives, and no smallness assumption. This remark records only those supported proof costs. It does not claim a stronger constructive metatheorem that this run did not source.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A square is cartesian exactly when a short sequence is exact

Statement

Consider a commutative square in an abelian category

Then the square is cartesian if and only if the sequence $0 \to P \overset{(\binom{α}{β})}{\to} X \oplus Y \overset{(f, - g)}{\to} Z$ is exact.

Facts & Assumptions

Given: The displayed commutative square.

[L1]

Pullbacks are defined by the usual universal property (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L2]

In a biproduct, a morphism into $X \oplus Y$ is determined by its two projections, and $i_{X} p_{X} + i_{Y} p_{Y} = 1_{X \oplus Y}$ (Biproduct, On a biproduct, the injections and projections satisfy the identity-sum relation).

[L3]

Exactness of $0 \to P \to X \oplus Y \to Z$ is equivalent to the first map being a kernel of the second (Degenerate exactness criteria, Exact sequence and short exact sequence in an abelian category).

Proof

technique · direct

1.1

Assume the square is cartesian. Then $(f, - g) (\binom{α}{β}) = f α - g β = 0$ . If $u : U \to X \oplus Y$ satisfies $(f, - g) u = 0$ , write $x : = p_{X} u$ and $y : = p_{Y} u$ . Then $f x = g y$ , so the pullback property [L1] gives a unique $t : U \to P$ with $α t = x$ and $β t = y$ . By [L2], this implies $(\binom{α}{β}) t = u$ , so $(\binom{α}{β})$ is a kernel of $(f, - g)$ and the sequence is exact by [L3].

L1L2L3assume-hypalgebra

1.2

Assume the sequence is exact. Then [L3] says $(\binom{α}{β})$ is a kernel of $(f, - g)$ , so the square commutes. Given $x : U \to X$ and $y : U \to Y$ with $f x = g y$ , define $u : = i_{X} x + i_{Y} y$ . By [L2], $(f, - g) u = f x - g y = 0$ , so the kernel property gives a unique $t : U \to P$ with $(\binom{α}{β}) t = u$ . Applying $p_{X}$ and $p_{Y}$ yields $α t = x$ and $β t = y$ , proving the pullback property.

L1L2L3assume-hypconstructalgebra

2.1

Therefore the square is cartesian exactly when the displayed sequence is exact.

step 1.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

A cartesian square induces an isomorphism on the kernels of its parallel legs

Statement

In a cartesian square in an abelian category

the induced morphism $\ker (β) ⟶ \ker (f)$ is an isomorphism.

Facts & Assumptions

Given: The displayed cartesian square.

[L1]

The square is a pullback (A square is cartesian exactly when a short sequence is exact).

[L2]

In a pullback square, the induced map on the kernels of the parallel legs is an isomorphism (In a pullback square, the induced map on the kernels of the two parallel arrows is an isomorphism).

Proof

technique · direct

1.1

Since the square is cartesian, [L1] identifies it as a pullback square.

2.1

Applying [L2] to that pullback gives the claimed isomorphism $\ker (β) ≅ \ker (f)$ .

L2step 1.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open item page →

A cartesian square over an epimorphism is also cocartesian

Statement

In an abelian category, if

is a cartesian square and $e$ is epic, then the square is also cocartesian.

Facts & Assumptions

Given: The displayed cartesian square, with $e$ epic.

[L1]

The square is a pullback exactly when $0 \to P \overset{(\binom{α}{β})}{\to} X \oplus Y \overset{(f, - e)}{\to} Z$ is exact (A square is cartesian exactly when a short sequence is exact).

[L2]

In an abelian category, an exact sequence $A \to B \to C \to 0$ is exactly one in which the last map is a cokernel of the first (Degenerate exactness criteria).

[L3]

Pushouts are defined by the usual colimit universal property (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L4]

The biproduct $X \oplus Y$ carries the usual injections from $X$ and $Y$ (Biproduct).

Proof

technique · direct

1.1

By [L1], the cartesian hypothesis makes $0 \to P \overset{(\binom{α}{β})}{\to} X \oplus Y \overset{v}{\to} Z$ exact, where $v : = (f, - e)$ . If $r, s : Z \to T$ satisfy $r v = s v$ , then $r e = - r v i_{Y} = - s v i_{Y} = s e$ , so the epicity of $e$ gives $r = s$ . Thus $v$ is epic, and the sequence $P \overset{(\binom{α}{β})}{\to} X \oplus Y \overset{v}{\to} Z \to 0$ is exact.

L1givenL4algebra

2.1

By [L2], the map $v$ is a cokernel of $(\binom{α}{β})$ . Now let $x : X \to T$ and $y : Y \to T$ satisfy $x α = y β$ . By the coproduct side of [L4], there is a unique morphism $w : X \oplus Y \to T$ with $w i_{X} = x$ and $w i_{Y} = - y$ . Then $w (\binom{α}{β}) = x α - y β = 0,$ so the cokernel property gives a unique $u : Z \to T$ with $u v = w$ . Composing with $i_{X}$ and $i_{Y}$ yields $u f = u v i_{X} = w i_{X} = x, u e = - u v i_{Y} = - w i_{Y} = y .$ This is exactly the pushout universal property from [L3].

L2L3L4step 1.1constructalgebra

3.1

Therefore every pullback square over an epimorphism is also a pushout square.

step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Epimorphisms in an abelian category are universal

Statement

Every epimorphism in an abelian category is universal: every pullback of it is again an epimorphism.

Facts & Assumptions

Given: An epimorphism in an abelian category and any pullback of it.

[L1]

The pullback of an epimorphism is an epimorphism (The pullback of an epimorphism is an epimorphism).

Proof

technique · direct

1.1

Take any epimorphism and any pullback of it.

given

2.1

The pullback leg is epic by [L1], which is exactly the universality claim.

L1step 1.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

The covering criterion for exactness

Statement

For a composable pair $X \overset{f}{\to} Y \overset{g}{\to} Z$ in an abelian category, the following are equivalent:

the pair is exact at $Y$ ;
$g f = 0$ , and for every morphism $h : W \to Y$ with $g h = 0$ , there exist an object $V$ , an epimorphism $k : V \to W$ , and a morphism $l : V \to X$ such that $h k = f l .$

Facts & Assumptions

Given: The composable pair $X \overset{f}{\to} Y \overset{g}{\to} Z$ .

[L1]

Exactness at $Y$ is equivalent to the member criterion $g y \equiv 0 \Rightarrow \exists x, f x \equiv y$ (Exactness is detected by members).

[L2]

Member equivalence means equality after precomposition by one common pair of epimorphisms (Equivalence of members).

Proof

technique · direct

1.1

Assume the pair is exact. Then [L1] gives $g f = 0$ . Now let $h : W \to Y$ satisfy $g h = 0$ . Then $g h \equiv 0$ , so [L1] gives a member $x : U \to X$ with $f x \equiv h$ . By [L2], there exist an object $V$ and epimorphisms $a : V \to U$ and $k : V \to W$ such that $f x a = h k$ . Putting $l : = x a$ proves the covering condition.

L1L2assume-hypchooseconstruct

1.2

Assume $g f = 0$ and the covering condition. Let $y : W \to Y$ be a member with $g y \equiv 0$ . Choose an epic $u : W^{'} \to W$ with $g y u = 0$ , and apply the covering condition to $h : = y u$ . This gives an epic $k : V \to W^{'}$ and a map $l : V \to X$ with $y u k = f l$ . Since $u k$ is epic, [L2] says exactly that $f l \equiv y$ . Therefore [L1] gives exactness at $Y$ .

L1L2assume-hypconstruct

2.1

Thus the covering condition is equivalent to exactness.

step 1.1step 1.2∎

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

The covering criterion and the member calculus are the same tool

The two formulations carry the same data. Both begin with the composite-zero condition $g f = 0$ . A member of $Y$ is an arrow into $Y$ , and equivalence of members in Equivalence of members is exactly agreement after precomposition with one common pair of epimorphic covers. Thus the existence of $x$ with $f x \equiv y$ in Exactness is detected by members is the same lifting assertion as the existence of an epic cover $k : V \to W$ and a morphism $l : V \to X$ with $y k = f l$ in The covering criterion for exactness.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

The kernel row and cokernel row of a morphism of short exact sequences are exact at two nodes each

Statement

Given a morphism of short exact sequences in an abelian category

the induced kernel sequence $0 \to \ker (a) \to \ker (b) \to \ker (c)$ is exact at $\ker (a)$ and at $\ker (b)$ .

Dually, the induced cokernel sequence $coker (a) \to coker (b) \to coker (c) \to 0$ is exact at $coker (b)$ and at $coker (c)$ .

Facts & Assumptions

Given: The morphism of short exact sequences in the statement.

[L1]

In a short exact sequence, the left map is a kernel and the right map is a cokernel (Degenerate exactness criteria).

[L2]

Under the stated endpoint hypotheses, the induced kernel or cokernel sequence is exact at its middle node (Exactness of kernel and cokernel sequences under endpoint hypotheses).

[L3]

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

[L4]

Exactness is self-dual (Exactness is self-dual).

Proof

technique · direct

1.1

Because both rows are short exact, [L1] says that the left square is a morphism between exact pairs and that $i^{'}$ is monic. Therefore [L2] applies and gives exactness of the induced kernel sequence $\ker (a) \to \ker (b) \to \ker (c)$ at $\ker (b)$ .

L1L2

1.2

Let $u : \ker (a) \to \ker (b)$ be the induced map and choose kernel arrows $k_{a} : \ker (a) \to A$ and $k_{b} : \ker (b) \to B$ . If $u s = u t$ , then $i k_{a} s = k_{b} u s = k_{b} u t = i k_{a} t .$ The map $i$ is monic by [L1], and $k_{a}$ is monic by [L3], so $s = t$ . Hence $u$ is monic, which is exactly exactness of $0 \to \ker (a) \to \ker (b)$ at $\ker (a)$ .

L1L3algebra

2.1

Passing to the opposite category turns the diagram into a morphism of short exact sequences again. Applying steps 1.1 and 1.2 there and transporting the result back with [L4] yields exactness of the induced cokernel sequence at $coker (b)$ and at $coker (c)$ .

L4step 1.1step 1.2

3.1

Hence the kernel row is exact at $\ker (a)$ and $\ker (b)$ , and the cokernel row is exact at $coker (b)$ and $coker (c)$ .

step 1.1step 1.2step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Exactness of kernel and cokernel sequences under endpoint hypotheses

Statement

Consider a commutative diagram in an abelian category

Then:

if the top row is exact and $k$ is monic, the induced sequence $\ker (α) \to \ker (β) \to \ker (γ)$ is exact;
if the bottom row is exact and $g$ is epic, the induced sequence $coker (α) \to coker (β) \to coker (γ)$ is exact.

Facts & Assumptions

Given: The commutative diagram in the statement.

[L1]

Exactness can be tested by the covering criterion (The covering criterion for exactness).

[L2]

Exactness is self-dual (Exactness is self-dual).

[L3]

Kernels are universal for morphisms annihilated by the given map, and cokernels are dual (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

[L4]

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

Proof

technique · direct

1.1

Assume the top row is exact and $k$ is monic. Choose kernels $h : \ker (α) \to X$ , $i : \ker (β) \to Y$ , and $j : \ker (γ) \to Z$ . By [L3], the commutative diagram induces morphisms $a : \ker (α) \to \ker (β), b : \ker (β) \to \ker (γ)$ with $i a = f h, j b = g i .$

L3assume-hypconstruct

2.1

To prove exactness of $\ker (α) \overset{a}{\to} \ker (β) \overset{b}{\to} \ker (γ),$ apply the covering criterion [L1] to the pair $(a, b)$ . Let $u : T \to \ker (β)$ satisfy $b u = 0$ . Then $g i u = j b u = 0,$ so exactness of the top row gives an object $P$ , an epimorphism $e : P \to T$ , and a morphism $x : P \to X$ with $i u e = f x .$

L1L3step 1.1construct

3.1

Applying $β$ to the displayed equality gives $0 = β i u e = k α x .$ Since $k$ is monic, $α x = 0$ . The kernel property of $h$ therefore gives $x^{'} : P \to \ker (α)$ with $h x^{'} = x$ . Now $i u e = f h x^{'} = i a x^{'},$ so monicity of $i$ from [L4] yields $u e = a x^{'}$ . Also $j b a = g i a = g f h = 0,$ so monicity of $j$ from [L4] gives $b a = 0$ . Thus the pair $(a, b)$ satisfies both parts of the covering criterion [L1], and the kernel sequence is exact.

L1L3L4step 1.1step 2.1algebra

4.1

The cokernel statement is the formal dual of steps 1.1 to 3.1 in the opposite abelian category: bottom-row exactness becomes top-row exactness, the epicity of $g$ becomes monicity of $g^{o p}$ , kernels become cokernels, and [L2] transports the resulting exact sequence back to the original category.

L2step 1.1step 2.1step 3.1

5.1

Therefore both displayed induced sequences are exact under the stated endpoint hypotheses.

step 3.1step 4.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

The kernel-cokernel sequence of a composite

Statement

For composable morphisms $A \overset{f}{\to} B \overset{g}{\to} C$ in an abelian category, there is an exact sequence $0 \to \ker (f) \to \ker (g f) \to \ker (g) \overset{q_{f} k_{g}}{\to} coker (f) \to coker (g f) \to coker (g) \to 0,$ where $k_{g} : \ker (g) \to B$ is a kernel of $g$ , $q_{f} : B \to coker (f)$ is a cokernel of $f$ , and the unlabeled arrows are the canonical comparison maps induced by the chosen kernels and cokernels.

Facts & Assumptions

Given: Composable morphisms $A \overset{f}{\to} B \overset{g}{\to} C$ .

[L1]

Under the stated endpoint hypotheses, the induced kernel and cokernel sequences are exact (Exactness of kernel and cokernel sequences under endpoint hypotheses).

[L2]

Exactness is self-dual (Exactness is self-dual).

[L3]

Kernels and cokernels are universal for the morphisms they annihilate (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

[L4]

The identity of an object is a kernel of its map to $0$ , and dually a cokernel of the map $0 \to A$ (The cokernel of the zero map out of the zero object is the target, and dually for kernels).

[L5]

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

Proof

technique · direct

1.1

Choose kernels $k_{f} : K_{f} \to A, k_{g f} : K_{g f} \to A, k_{g} : K_{g} \to B$ and cokernels $q_{f} : B \to Q_{f}, q_{g f} : C \to Q_{g f}, q_{g} : C \to Q_{g} .$ Because $g f k_{f} = 0$ , [L3] gives a canonical map $u : K_{f} \to K_{g f}$ with $k_{g f} u = k_{f}$ . Likewise $g f k_{g f} = 0$ gives a canonical map $v : K_{g f} \to K_{g}$ with $k_{g} v = f k_{g f}$ . Put $δ : = q_{f} k_{g} : K_{g} \to Q_{f} .$ Since $q_{g f} g f = 0$ and $q_{g} g = 0$ , [L3] also gives canonical maps $w : Q_{f} \to Q_{g f}$ and $x : Q_{g f} \to Q_{g}$ .

L3construct

2.1

The map $u$ is monic: if $u s = u t$ , then $k_{f} s = k_{g f} u s = k_{g f} u t = k_{f} t$ , and monicity of $k_{f}$ from [L5] forces $s = t$ . So the sequence is exact at $\ker (f)$ .

L5step 1.1algebra

2.2

Apply [L1] to the commutative diagram tikzcd \ker(f) \arrow[r, "k_f"] \arrow[d, "0"'] & A \arrow[r, "f"] \arrow[d, "g f"'] & B \arrow[d, "g"'] \\ 0 \arrow[r] & C \arrow[r, "1_C"'] & C. The top row is exact, and $0 \to C$ is monic. Hence the induced sequence $\ker (0) \to \ker (g f) \to \ker (g)$ is exact. By [L4], $\ker (0)$ is represented by $1_{\ker (f)}$ , so this is exactly the sequence $\ker (f) \overset{u}{\to} \ker (g f) \overset{v}{\to} \ker (g)$ at $\ker (g f)$ .

L1L4step 1.1construct

2.3

Apply [L1] again to tikzcd A \arrow[r, "f"] \arrow[d, "g f"'] & B \arrow[r, "q_f"] \arrow[d, "g"'] & \operatorname{coker}(f) \arrow[d, "0"'] \\ C \arrow[r, "1_C"'] & C \arrow[r] & 0. The top row is exact, and $1_{C}$ is monic. Therefore the induced sequence $\ker (g f) \to \ker (g) \to \ker (0_{coker (f), 0})$ is exact. By [L4], the last kernel is represented by $1_{coker (f)}$ , and the induced map is $q_{f} k_{g} = δ$ . Hence $\ker (g f) \overset{v}{\to} \ker (g) \overset{δ}{\to} coker (f)$ is exact at $\ker (g)$ .

L1L4step 1.1construct

3.1

Apply steps 2.1 to 2.3 in the opposite category to the composable pair $C \overset{g^{o p}}{\to} B \overset{f^{o p}}{\to} A .$ Using [L2], the resulting exactness statements transport back to exactness of $\ker (g) \overset{δ}{\to} coker (f) \overset{w}{\to} coker (g f) \overset{x}{\to} coker (g) \to 0$ at $coker (f)$ , at $coker (g f)$ , and at $coker (g)$ .

L2step 1.1step 2.1step 2.2step 2.3

4.1

Steps 2.1 to 2.3 and 3.1 give the full exact sequence displayed in the statement.

step 2.1step 2.2step 2.3step 3.1∎

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Comember and the dual calculus

Definition

The dual member calculus in an abelian category is the member calculus of the opposite category, transported back along Exactness is self-dual.

Concretely, a comember of $A$ is a morphism with domain $A$ , $x : A \to X,$ and two comembers $x : A \to X$ and $y : A \to Y$ are equivalent when there exist one object $W$ and monomorphisms $u : X ↣ W, v : Y ↣ W$ with $u x = v y .$

So comembers compare after one common monomorphic enlargement, just as members compare after one common epimorphic cover.

RemarkRemark: AI-adaptedProof: Not applicableaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Two routes to every dual statement

Every dual statement on the next page may be reached in two honest ways. One may dualize a member argument through Exactness is self-dual, or one may run the comember calculus directly via Comember and the dual calculus. The page keeps both routes visible because Mac Lane's subtraction surrogate The subtraction surrogate is used directly in some member arguments while other proofs are cleaner after formal dualization.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Hom is left exact in each variable

Statement

Let $A$ be an abelian category and $X$ an object of $A$ .

If $0 \to A \to B \to C$ is exact, then $0 \to A (X, A) \to A (X, B) \to A (X, C)$ is exact in $A b$ .
If $A \to B \to C \to 0$ is exact, then $0 \to A (C, X) \to A (B, X) \to A (A, X)$ is exact in $A b$ .

Thus Hom is left exact in each variable.

Facts & Assumptions

Given: An abelian category $A$ and an object $X$ of $A$ .

[L1]

In an abelian category, exactness at the left end means that the first displayed map is a kernel of the second (Degenerate exactness criteria).

[L2]

Abelian categories have all finite limits, and representable functors preserve existing small limits (An abelian category has all finite limits and all finite colimits, Every covariantly representable functor to Set preserves all existing small limits).

[L3]

The covariant and contravariant Hom assignments are the representable functors $A (X, -)$ and $A^{o p} (X, -)$ (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category, The opposite of an abelian category is abelian).

[L4]

The target category of these Hom functors is $A b$ , which is abelian (Abelian groups form an abelian category).

Proof

technique · direct

1.1

Assume $0 \to A \to B \to C$ is exact. By [L1], the map $A \to B$ is a kernel of $B \to C$ . By [L2] and [L3], the representable functor $A (X, -)$ preserves that kernel. Therefore $0 \to A (X, A) \to A (X, B) \to A (X, C)$ is exact in $A b$ by [L1] applied inside the abelian category [L4].

L1L2L3L4assume-hyp

2.1

Passing to the opposite category, the exact sequence $A \to B \to C \to 0$ becomes a left-exact sequence in $A^{o p}$ . Applying step 1.1 there to the representable functor $A^{o p} (X, -) = A (-, X)$ gives $0 \to A (C, X) \to A (B, X) \to A (A, X)$ exact in $A b$ .

L2L3L4step 1.1

3.1

Hence Hom is left exact in each variable.

step 1.1step 2.1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Hom is not exact

Statement refuted

For every object $X$ in an abelian category, the functor $A (-, X)$ is exact.

Facts & Assumptions

Given: In $A b$ , the short exact sequence $0 \to Z \overset{\times 2}{\to} Z \to Z / 2 \to 0.$

[L1]

The category $A b$ is abelian (Abelian groups form an abelian category).

[L2]

Hom is left exact, but no right exactness was asserted (Hom is left exact in each variable).

Counterexample

technique · direct

1.1

Apply $A b (-, Z)$ to the given short exact sequence. This yields $0 \to Hom (Z / 2, Z) \to Hom (Z, Z) \overset{(\times 2)^{*}}{\to} Hom (Z, Z)$ , which is left exact by [L2].

L1L2given

2.1

The group $Hom (Z, Z)$ is $Z$ , and precomposition with $\times 2$ is multiplication by $2$ on that copy of $Z$ . This map is not surjective, so the Hom sequence is not exact at the right-hand term.

step 1.1algebra

3.1

Therefore the contravariant Hom functor need not be exact.

step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

An object is projective exactly when Hom out of it is exact

Statement

Let $P$ and $I$ be objects of an abelian category.

$P$ is projective if and only if the functor $A (P, -)$ is exact.
$I$ is injective if and only if the functor $A (-, I)$ is exact.

Facts & Assumptions

Given: An abelian category and objects $P$ and $I$ in it.

[L1]

Hom is left exact in each variable (Hom is left exact in each variable).

[L2]

Projective objects are exactly those for which Hom out of them sends every short exact sequence to a short exact sequence (Projective object, Projective object characterisations).

[L3]

Injective objects are exactly those for which Hom into them sends every short exact sequence to a short exact sequence (Injective object, Injective object characterisations).

[L4]

An exact functor is one that is both left exact and right exact (Exact functor between abelian categories).

Proof

technique · direct

1.1

By [L1], the functor $A (P, -)$ is always left exact. Therefore, by [L4], it is exact exactly when it is also right exact on every short exact sequence. But [L2] says that extra right-end surjectivity is exactly the projective lifting property.

L1L2L4

2.1

The same argument for the contravariant Hom functor uses [L1], [L3], and [L4]: $A (-, I)$ is always left exact, and exactness is equivalent to the additional surjectivity that characterizes injectivity.

L1L3L4∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

AB5 is equivalent to exactness of filtered colimits

Statement

Let $A$ be a cocomplete abelian category. Then $A$ satisfies AB5 if and only if for every small filtered category $J$ , the filtered colimit functor ${colim}_{J} : A^{J} \to A$ is exact.

Facts & Assumptions

Given: A cocomplete abelian category $A$ .

[L1]

AB5 is the directed-family lattice identity of The axioms AB5 and AB5*.

[L2]

An exact functor preserves the finite limits and finite colimits of its source, and in particular preserves short exact sequences (Exact functor between abelian categories, Exact sequence and short exact sequence in an abelian category, Degenerate exactness criteria).

[L3]

A filtered colimit is a colimit indexed by a small filtered category (Filtered categories and filtered colimits, Finite, small, and large limits and colimits; complete and cocomplete categories).

[L4]

The meet of two subobjects is represented by their pullback, and the image of a morphism is the least subobject through which that morphism factors (The meet of two subobjects is their pullback, The image is the least subobject through which a morphism factors).

[L5]

Weibel, Appendix A.4.6, states for a cocomplete abelian category that exactness of filtered colimits is equivalent to the directed-subobject identity $(⋁_{i} B_{i}) \land C = ⋁_{i} (B_{i} \land C) .$

Proof

technique · direct

1.1

Assume AB5. Its defining identity [L1] is exactly the directed-subobject identity in [L5]. The forward implication of the cited equivalence therefore says that every filtered colimit functor is exact.

L1L3L5assume-hyp

1.2

Conversely, assume every filtered colimit functor is exact. Let $I$ be a small directed poset indexing a family of monomorphisms $b_{i} : B_{i} ↣ A$ , and let $c : C ↣ A$ represent a fixed subobject of $A$ . For each $i \in I$ , form the pullback square tikzcd P_i \arrow[r] \arrow[d] & C \arrow[d, "c"] \\ B_i \arrow[r, "b_i"'] & A. By [L4], the top-left leg represents $B_{i} \land C$ . These pullback squares assemble into a diagram in $A^{I}$ . Because the filtered colimit functor ${colim}_{I}$ is exact, [L2] and [L3] say that it preserves finite limits, so its colimit square tikzcd P \arrow[r] \arrow[d] & C \arrow[d, "c"] \\ B \arrow[r, "b"'] & A is again a pullback.

L2L3L4assume-hypconstruct

2.1

The image of $b : B \to A$ is the join $⋁_{i} B_{i}$ : each $b_{i}$ factors through $b$ , so every $B_{i}$ lies below $im (b)$ , and any common upper bound of the family receives $b$ by the colimit universal property, so [L4] makes $im (b)$ the least such upper bound. The same argument inside $C$ shows that the image of $P \to C$ is $⋁_{i} (B_{i} \land C)$ .

L4step 1.2algebra

3.1

Because the square of step 1.2 is a pullback, [L4] identifies the image of $P \to C$ with the meet of the subobject represented by $im (b)$ and the fixed subobject $C$ . Using step 2.1, this gives $(⋁_{i} B_{i}) \land C = ⋁_{i} (B_{i} \land C),$ which is exactly AB5 by [L1].

L1L4step 1.2step 2.1

4.1

Therefore AB5 is equivalent to exactness of filtered colimits.

step 1.1step 3.1∎

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

FALSE: a short exact sequence splits whenever its middle object is isomorphic to the biproduct of the outer two

Statement

If $0 \to A \to B \to C \to 0$ is a short exact sequence in an abelian category and $B$ is merely isomorphic as an object to $A \oplus C$ , then the sequence splits.

Facts & Assumptions

Given: The ring $R = k [ε] / (ε^{2})$ , the quotient $q : R \to k = R / (ε)$ , and the inclusion $i : k \to R$ with image $(ε)$ .

[L1]

Module categories are abelian (Modules over a ring form an abelian category).

[L2]

A short exact sequence splits exactly when the epimorphism has a section (Splitting lemma in an abelian category, Split short exact sequence in an abelian category).

Refutation

technique · direct

1.1

In $R - M o d$ , the sequence $0 \to k \overset{i}{\to} R \overset{q}{\to} k \to 0$ is short exact: $q$ is the quotient by $(ε)$ and $i$ identifies $k$ with that ideal. By [L1], this is a short exact sequence in an abelian category.

L1givenalgebra

2.1

If this sequence split, a section $s : k \to R$ of $q$ would satisfy $q (s (1)) = 1$ while $R$ -linearity would force $ε s (1) = s (ε \cdot 1) = 0$ , so $s (1)$ would lie in $(ε)$ , contradiction. Hence [L2] says the sequence is nonsplit.

L2step 1.1assume-hypalgebra

3.1

Let $T : = R^{(N)} \oplus k^{(N)}$ . Direct-summing step 1.1 with $0 \to T \overset{1_{T}}{\to} T \to 0 \to 0$ gives $0 \to k \oplus T \to R \oplus T \overset{q \oplus 0}{\to} k \to 0$ . Any section of $q \oplus 0$ would project to a section of $q$ , so this stabilized sequence is still nonsplit by step 2.1.

L2step 2.1constructalgebra

4.1

Countable shifts give $R \oplus T ≅ T$ , $k \oplus T ≅ T$ , and $(k \oplus T) \oplus k ≅ T$ , because adding finitely many $R$ - or $k$ -summands does not change $R^{(N)} \oplus k^{(N)}$ . Hence $R \oplus T ≅ (k \oplus T) \oplus k$ .

step 3.1algebra

5.1

Step 3.1 gives a nonsplit short exact sequence, while step 4.1 shows that its middle object is abstractly isomorphic to the biproduct of its outer objects. Therefore the statement is false.

step 3.1step 4.1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

The members of an object do not form a group

Statement refuted

For every object in an abelian category, its members modulo equivalence form an group under the ambient addition of arrows.

Facts & Assumptions

Given: The abelian category $A b$ and the identity member $1_{Z} : Z \to Z$ .

[L1]

The category $A b$ is abelian (Abelian groups form an abelian category).

[L2]

Every member has a negative, and equivalence to zero is literal equality to the zero morphism (Each object has a zero member and each member has a negative).

Counterexample

technique · direct

1.1

In $A b$ , the identity member satisfies $1_{Z} \equiv - 1_{Z}$ because $1_{Z} (- 1_{Z}) = (- 1_{Z}) 1_{Z}$ and the automorphism $- 1_{Z}$ is epic.

L1L2algebra

1.2

If member classes carried a group law induced from arrow addition, then $[1_{Z}] + [1_{Z}] = [1_{Z}] + [- 1_{Z}] = [0]$ . But the left-hand class is represented by $2 \cdot 1_{Z} : Z \to Z$ , and [L2] says $2 \cdot 1_{Z} \equiv 0$ would force $2 \cdot 1_{Z} = 0$ , which is false in $A b$ .

L2assume-hypalgebra

2.1

Therefore the member classes of an object need not carry an induced group law.

step 1.1step 1.2∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

Two morphisms agreeing on every member need not be equal

Statement refuted

If two morphisms $f, g : A \to B$ satisfy $f x \equiv g x$ for every member $x$ of $A$ , then $f = g$ .

Facts & Assumptions

Given: The abelian category $A b$ and the two endomorphisms $1_{Z}, - 1_{Z} : Z \to Z$ .

[L1]

The category $A b$ is abelian (Abelian groups form an abelian category).

[L2]

Every member has a negative, and equivalence to zero is literal equality (Each object has a zero member and each member has a negative).

Counterexample

technique · direct

1.1

Let $x : X \to Z$ be any member. Then $(- 1_{Z}) x = x (- 1_{X})$ , and the automorphism $- 1_{X}$ is epic. Therefore $1_{Z} x \equiv (- 1_{Z}) x$ .

L1L2algebra

1.2

Nevertheless $1_{Z} \neq - 1_{Z}$ , since they send $1 \in Z$ to different integers. So memberwise equivalence of composites does not force equality of the morphisms themselves.

L1algebra

2.1

This refutes the statement.

step 1.1step 1.2∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

The kernel row of a morphism of short exact sequences need not be short exact

Statement refuted

For every morphism of short exact sequences in an abelian category, the induced kernel row is itself short exact.

Diagram

diagram failed to render:
0 \arrow[r] & \mathbb Z \arrow[r, "\times 2"] \arrow[d, "\times 2"'] & \mathbb Z \arrow[r] \arrow[d, "\times 2"'] & \mathbb Z/2 \arrow[r] \arrow[d, "0"'] & 0 \\
0 \arrow[r] & \mathbb Z \arrow[r, "\times 2"'] & \mathbb Z \arrow[r] & \mathbb Z/2 \arrow[r] & 0.

Facts & Assumptions

Given: In $A b$ , the commutative diagram above.

[L1]

The category $A b$ is abelian (Abelian groups form an abelian category).

[L2]

For such a diagram, the kernel row is exact at its first two nodes (The kernel row and cokernel row of a morphism of short exact sequences are exact at two nodes each).

Counterexample

technique · direct

1.1

Each row is short exact, and the vertical maps make a morphism of short exact sequences in the abelian category $A b$ by [L1].

L1givenalgebra

1.2

The kernels of the three vertical maps are $\ker (\times 2) = 0, \ker (\times 2) = 0, \ker (0) = Z / 2.$ So the kernel row is $0 \to 0 \to 0 \to Z / 2.$ By [L2], it is exact at the first two nodes.

L2step 1.1algebra

2.1

The last map in that row is the zero map $0 \to Z / 2$ , hence not epic. Therefore the kernel row is not short exact.

step 1.2algebra

3.1

This refutes the statement.

step 2.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

FALSE: two morphisms that agree on every member are equal

Statement

If $f, g : A \to B$ satisfy $f x \equiv g x$ for every member $x$ of $A$ , then $f = g$ .

Facts & Assumptions

Given: The memberwise equality claim of the statement.

[L1]

The only general member test for equality of morphisms is the zero-arrow criterion (A zero arrow is detected by members).

[L2]

There are distinct morphisms that agree on every member (Two morphisms agreeing on every member need not be equal).

Refutation

technique · direct

1.1

The witness in [L2] gives distinct morphisms $f$ and $g$ with $f x \equiv g x$ for every member $x$ . So the stated implication fails.

2.1

Item [L1] explains the precise replacement: member tests can detect equality with zero, not arbitrary equality of morphisms.

L1step 1.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

FALSE: the members of an object form an abelian group

Statement

For every object of an abelian category, addition of representatives induces an abelian-group operation on its members modulo equivalence.

Facts & Assumptions

Given: The group-law claim of the statement.

[L1]

The subtraction surrogate gives only an existence statement for a witness $z$ , not a binary operation on all member classes (The subtraction surrogate).

[L2]

There is an explicit object whose members do not support such a group law (The members of an object do not form a group).

Refutation

technique · direct

1.1

The counterexample [L2] shows that the claimed group structure fails even in $A b$ . So the statement is false.

2.1

This does not contradict [L1]: the subtraction surrogate is weaker than an additive law on member classes.

L1step 1.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

FALSE: member equivalence is transitive in any pointed category with pullbacks

Statement

In any pointed category with pullbacks, the member relation $\equiv$ is transitive.

Facts & Assumptions

Given: The weakened hypothesis of the statement.

Refutation

technique · direct

1.1

Work in the category of commutative rings not required to have an identity, with arbitrary ring homomorphisms. The zero ring is a zero object, and pullbacks are the usual fibre-product rings, so this category is pointed and has pullbacks. Let $A : = C [t, t^{- 1}], x : C [t] ↪ A, y : = 1_{A} : A \to A, z : C [t^{- 1}] ↪ A$ be the two localization inclusions and the identity member. The map $x$ is epic: if $φ, ψ : A \to R$ agree on $C [t]$ , then they agree on $e : = φ (1) = ψ (1)$ and $a : = φ (t) = ψ (t)$ . Both $φ (t^{- 1})$ and $ψ (t^{- 1})$ are inverses of $a$ in the commutative corner ring $e R$ , so they are equal; hence $φ = ψ$ . The same argument shows that $z$ is epic. Therefore $x \equiv y$ and $y \equiv z$ .

constructalgebra

1.2

The pullback of $x$ and $z$ is the constant subring $C$ , because inside $C [t, t^{- 1}]$ one has $C [t] \cap C [t^{- 1}] = C .$ Its two projections are the constant-term inclusions $p_{1} : C \to C [t], p_{2} : C \to C [t^{- 1}] .$

constructalgebra

2.1

Suppose $x \equiv z$ . Then there would exist a ring $T$ and epimorphisms $q : T \to C [t]$ and $r : T \to C [t^{- 1}]$ with $x q = z r$ . By the pullback property from step 1.2, there would be a map $m : T \to C$ with $q = p_{1} m$ and $r = p_{2} m$ . Since $q$ is epic, $p_{1}$ would also be epic. But $p_{1}$ is not epic: the evaluation maps ${ev}_{0}, {ev}_{1} : C [t] \to C$ are distinct and satisfy ${ev}_{0} p_{1} = {ev}_{1} p_{1} = 1_{C} .$ This contradiction shows that $x \equiv̸ z$ .

step 1.2assume-hypalgebra

3.1

Thus $\equiv$ is not transitive in this pointed category with pullbacks, and the statement is false.

step 1.1step 2.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29‡ rests on unproved material (inherited)Open item page →

FALSE: the kernel row of a morphism of short exact sequences is short exact

Statement

For every morphism of short exact sequences in an abelian category, the induced kernel row is short exact.

Facts & Assumptions

Given: The universal short-exactness claim of the statement.

[L1]

The general positive theorem gives exactness only at the first two nodes (The kernel row and cokernel row of a morphism of short exact sequences are exact at two nodes each).

[L2]

The multiplication-by-two diagram gives a failure of short exactness (The kernel row of a morphism of short exact sequences need not be short exact).

Refutation

technique · direct

1.1

The witness in [L2] is a morphism of short exact sequences whose kernel row is not short exact. Therefore the universal statement fails.

2.1

Item [L1] records the correct surviving assertion: two exact nodes, not a short exact row.

L1step 1.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29‡ rests on unproved material (inherited)Open item page →

FALSE: the subtraction rule produces a unique member

Statement

In the subtraction surrogate, the member $z$ with $g z \equiv 0$ is unique.

Facts & Assumptions

Given: The category $A b$ .

[L1]

The category $A b$ is abelian (Abelian groups form an abelian category).

[L2]

The subtraction surrogate applies whenever $g x \equiv g y$ (The subtraction surrogate).

Refutation

technique · direct

1.1

In $A b$ , take $B = Z$ , $C = 0$ , $g = 0 : Z \to 0$ , and $x = y = 0_{Z, Z} : Z \to Z$ . Then $g x = g y = 0$ , so the hypotheses of [L2] are satisfied.

L1L2

2.1

Both $z_{0} : = 0_{Z, Z}$ and $z_{1} : = 1_{Z}$ satisfy $g z_{i} = 0$ , hence $g z_{i} \equiv 0$ . Since $z_{0} \neq z_{1}$ , the asserted uniqueness fails in this instance.

L1step 1.1algebra

3.1

Therefore the statement is false.

step 2.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

FALSE: the subobject-side definition of exactness needs no canonical image monomorphism

Statement

One may define exactness of $A \overset{f}{\to} B \overset{g}{\to} C$ by treating $im (f)$ merely as an object, without specifying its canonical monomorphism into $B$ , and writing the purported subobject equality $[im (f)] = [\ker (g)]$ anyway.

Facts & Assumptions

Given: The claim of the statement.

[L1]

Exactness at a node is stated as equality of the image subobject of $f$ with the kernel subobject of $g$ (Exactness at a node).

[L2]

A subobject of $B$ is represented by a monomorphism into $B$ (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms), and the image of $f$ includes its defining kernel arrow into $B$ (Image and coimage in a category with kernels and cokernels).

Refutation

technique · direct

1.1

By [L2], an object alone does not represent a subobject of $B$ : the structure monomorphism into $B$ is essential data. Thus the proposed equality is not a typed equality of subobjects until the canonical image monomorphism has been specified.

L1L2

2.1

Therefore the statement is false.

step 1.1∎