Alphabeta Math
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→fB→gC be composable morphisms in an abelian category. Choose an epi-mono factorization A→eim⁡(f)→mB of f, and choose a kernel K→kB of g.

Then:

  1. [ ⁣m ⁣]≤[ ⁣k ⁣] if and only if gf=0.
  2. [ ⁣k ⁣]≤[ ⁣m ⁣] if and only if every morphism u:U→B with gu=0 factors through m.

Facts & Assumptions

Given: The composable pair A→fB→gC, the factorization f=me with e epic and m monic, and the kernel k:K→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 gk=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.1L2L3algebra

If [ ⁣m ⁣]≤[ ⁣k ⁣], then m=kt for some t:im⁡(f)→K by [L2], so gf=gme=gkte=0 by [L3].

1.2L1L2L3algebra

If gf=0, then gme=0, and the epicity of e from [L1] gives gm=0. So [L3] gives t:im⁡(f)→K with kt=m, hence [ ⁣m ⁣]≤[ ⁣k ⁣] by [L2].

1.3L2L3

If [ ⁣k ⁣]≤[ ⁣m ⁣], then k=ms for some s:K→im⁡(f) by [L2]. For any u:U→B with gu=0, [L3] gives v:U→K with u=kv=msv, so u factors through m.

1.4L2L3

Conversely, if every u:U→B with gu=0 factors through m, then in particular the kernel arrow k does, because gk=0 by [L3]. Thus k=ms for some s, so [ ⁣k ⁣]≤[ ⁣m ⁣] by [L2].

2.1step 1.1step 1.2

Steps 1.1 and 1.2 prove the first biconditional.

3.1step 1.3step 1.4∎

Steps 1.3 and 1.4 prove the second biconditional.

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

Exactness at a node

Definition

Let A→fB→gC 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→fB→gC be composable morphisms in an abelian category, let K→kB be a kernel of g, and let B→qQ be a cokernel of f.

Then the pair is exact at B if and only if both gf=0andqk=0.

Facts & Assumptions

Given: The composable pair A→fB→gC, a kernel k:K→B of g, and a cokernel q:B→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=me, one has [ ⁣m ⁣]≤[ ⁣k ⁣] if and only if gf=0, and [ ⁣k ⁣]≤[ ⁣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.1L1L2

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

1.2L1L2L3algebra

Write f=me for an image factorization. Exactness gives k=mu for some u:K→im⁡(f), and qf=qme=0 implies qm=0 because e is epic. Hence qk=qmu=0.

1.3L2

Assume now that gf=0 and qk=0. Writing again f=me, the equality gf=0 gives [ ⁣m ⁣]≤[ ⁣k ⁣] by [L2].

2.1L3step 1.3algebra

Since qf=qme=0 and e is epic, one has qm=0. Together with the hypothesis qk=0, the cokernel property in [L3] yields u:K→im⁡(f) with mu=k, hence [ ⁣k ⁣]≤[ ⁣m ⁣].

3.1L1step 1.1step 1.2step 1.3step 2.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.

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→A→iB→pC→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→A→iB→pC→0 in an abelian category, the following are equivalent:

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

Facts & Assumptions

Given: Morphisms i:A→B and p:B→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 gf=0 and qk=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→A, and dually the identity of C is a kernel of C→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).

Proof

technique · direct
1.1L1L2L3L4

Assume the displayed sequence is short exact. Exactness at A and [L4] make the arrow criterion [L2] read 1Ak=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.

1.2L2L3L7

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 pi=0, and if k is a kernel of p while q is a cokernel of i, then k factors through i, hence qk=0 because qi=0. Thus [L2] gives exactness at B, so the sequence is short exact.

2.1L2step 1.1

Exactness at B gives pi=0 by [L2]. Since i is monic by step 1.1, the factorization i=i1A is an epi-mono factorization of i, so every u:U→B with pu=0 factors through i. Thus i is a kernel of p.

2.2L5L6step 1.1

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.

3.1step 1.1step 2.1

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

4.1step 2.2step 1.2∎

Steps 2.2 and 1.2 complete the equivalence.

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

Degenerate exactness criteria

Statement

In an abelian category:

  1. 0→K→uA is exact if and only if u is monic.
  2. 0→K→uA→vB is exact if and only if u is a kernel of v.
  3. A→vB→wC→0 is exact if and only if w is a cokernel of v.
  4. 0→A→uB→vC→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.1L1L2L3

Exactness of 0→K→uA says that the kernel of u is the zero subobject, and [L3] identifies that with u being monic. This proves claim 1.

1.2L2L3L4L5

For claim 3, first assume A→vB→wC→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.

2.1L2L4step 1.1

For claim 2, first assume 0→K→uA→vB 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.

2.2step 1.1step 1.2

If u is monic and v is a cokernel of u, then step 1.1 gives exactness of 0→A→uB, and claim 3 gives exactness of A→uB→vC→0. Hence the full sequence is short exact.

3.1step 2.1step 1.2

If 0→A→uB→vC→0 is short exact, then claims 2 and 3 give that u is a kernel of v and v is a cokernel of u.

3.2L3step 2.1

If u is a kernel of v and v is epic, then claim 2 gives exactness of 0→A→uB→vC, and [L3] turns the epicity of v into exactness at C. Hence the full sequence is short exact.

4.1step 3.1step 2.2step 3.2∎

Steps 3.1, 2.2, and 3.2 prove claim 4.

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→fB→gC is exact at B in an abelian category A if and only if the opposite pair C→gopB→fopA is exact at B in Aop.

Facts & Assumptions

Given: A composable pair A→fB→gC 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.1L1L2

By [L1], the opposite category Aop is again abelian, so the definition [L2] applies there. Passing to the opposite exchanges kernels with cokernels and images with coimages.

2.1L2step 1.1∎

Therefore the equality [im⁡(f)]=[ker⁡(g)] in A is exactly the equality [im⁡(gop)]=[ker⁡(fop)] in Aop. By [L2], those are the two exactness assertions.

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→A→iB→pC→0 in an abelian category is split when there exist morphisms s:C→B,π:B→A such that ps=1C,πi=1A,iπ+sp=1B.

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⊕C.

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

Splitting lemma in an abelian category

Statement

Let 0→A→iB→pC→0 be a short exact sequence in an abelian category.

  1. If s:C→B satisfies ps=1C, then there is a unique morphism π:B→A such that πi=1A,iπ+sp=1B.
  2. If π:B→A satisfies πi=1A, then there is a unique morphism s:C→B such that ps=1C,iπ+sp=1B.

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 ps=1C, πi=1A, and iπ+sp=1B (Split short exact sequence in an abelian category).

Proof

technique · constructive
1.1L1givenconstructalgebra

Assume ps=1C and put t:=1B−sp. Then pt=0, so because i is a kernel of p by [L1], there is a unique π:B→A with iπ=t=1B−sp.

1.2L1givenconstructalgebra

Conversely assume πi=1A and put u:=1B−iπ. Then ui=0, so because p is a cokernel of i by [L1], there is a unique s:C→B with sp=u=1B−iπ.

2.1L1step 1.1algebra

Composing iπ=1B−sp with i gives iπi=i−spi=i, because pi=0 by [L1]. Since i is monic, πi=1A, and the defining equation also yields iπ+sp=1B.

2.2L1step 1.2algebra

Composing sp=1B−iπ with p gives psp=p, and epicity of p forces ps=1C. The same equation already gives iπ+sp=1B.

3.1L1L2step 1.1step 2.1

If π′ satisfies the same two identities, then iπ′=1B−sp=iπ, so monicity of i gives π′=π. Hence the map is unique, and [L2] says the sequence is split.

3.2L1L2step 1.2step 2.2

If s′ satisfies the same two identities, then s′p=1B−iπ=sp, so epicity of p gives s′=s. Hence the map is unique, and [L2] again says the sequence is split.

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

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

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→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→A and y:Y→A be members of the same object A.

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

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 ≡ is reflexive and symmetric.

Facts & Assumptions

Given: Members x:X→A and y:Y→A.

[L1]

By definition, x≡y means there are epimorphisms u:W→X and v:W→Y with xu=yv (Equivalence of members).

Proof

technique · direct
1.1L1algebra

Reflexivity uses W=X with u=v=1X. The identity is epic and x1X=x1X, so x≡x by [L1].

1.2L1

If x≡y, choose W,u,v as in [L1] with xu=yv. Reading the same equality backwards gives yv=xu, so y≡x.

2.1step 1.1step 1.2∎

Therefore the member relation is reflexive and symmetric.

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

Member equivalence is transitive

Statement

For members of one object in an abelian category, the relation ≡ is transitive.

Facts & Assumptions

Given: An abelian category and members x:X→A, y:Y→A, and z:Z→A with x≡y and y≡z.

[L1]

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

[L2]
[L3]

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

Proof

technique · direct
1.1L1choose

Choose epimorphisms u:W1→X, v:W1→Y, w:W2→Y, and r:W2→Z with xu=yv and yw=zr, using [L1].

1.2L2L3construct

Form the pullback of v and w, with projections v′:P→W1 and w′:P→W2. By [L3], both v′ and w′ are epic.

2.1L1step 1.1step 1.2algebra

The pullback equation gives vv′=ww′, so xuv′=yvv′=yww′=zrw′. Hence the epimorphisms uv′:P→X and rw′:P→Z witness x≡z.

3.1step 2.1∎

Therefore member equivalence is transitive.

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

Members modulo equivalence correspond to subobjects

Statement

Let A be an object of an abelian category. Sending a member x:X→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→A and, when needed, a second member y:Y→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).

[L4]

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

Proof

technique · direct
1.1L1L2construct

Factor x as X→exIx→mxA with ex epic and mx monic, using [L1], and assign to the class of x the subobject [ ⁣mx ⁣] 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→1SS→mA shows that its image class is [ ⁣m ⁣].

2.1L1L2L4step 1.1

This assignment is well defined on equivalence classes. The equality x1X=mxex with epic maps on the right shows x≡mx, and similarly y≡my. If x≡y, then transitivity from [L4] gives mx≡my, 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 [ ⁣mx ⁣]=[ ⁣my ⁣] by [L2]. Step 2.1 gives x≡mx and y≡my, while equality of subobjects makes mx and my equivalent as members. Another use of [L4] yields x≡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.

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

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

Statement

For every object A of an abelian category:

  1. there is a zero member of A;
  2. every member x:X→A has a negative member −x:X→A;
  3. for every member x, one has x≡0 if and only if x=0 as a morphism.

Facts & Assumptions

Given: An abelian category and a member x:X→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.1L1L2

By [L1], there is a zero morphism 0X,A:X→A, so A has a zero member. By [L2], the additive inverse −x:X→A exists, so every member has a negative.

1.2L3assume-hypalgebra

Conversely, if x≡0, choose epimorphisms u:W→X and v:W→Y witnessing that equivalence. Then xu=0, and epicity of u forces x=0.

2.1L3step 1.1

If x=0, then x≡0 is witnessed by the identity epic 1X:X→X, since x1X=01X.

3.1step 1.1step 2.1step 1.2∎

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

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→B be a morphism.

  1. If x:X→A is a member of A, then fx:X→B is a member of B.
  2. If x≡y as members of A, then fx≡fy as members of B.

Facts & Assumptions

Given: A morphism f:A→B and members x:X→A, y:Y→A.

[L1]

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

Proof

technique · direct
1.1given

The composite fx:X→B is again a morphism into B, so it is a member of B.

1.2L1algebra

If x≡y, choose epimorphisms u:W→X and v:W→Y with xu=yv by [L1]. Postcomposing with f gives fxu=fyv, and the same epimorphisms witness fx≡fy.

2.1step 1.1step 1.2∎

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

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

Monicity is detected by members

Statement

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

  1. f is monic.
  2. For every member x:X→A, the implication fx≡0⟹x≡0 holds.

Facts & Assumptions

Given: A morphism f:A→B.

[L1]
[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.1L1L2assume-hypalgebra

Assume f is monic, and let x:X→A satisfy fx≡0. Choose an epic u:W→X witnessing this, so fxu=0. Since f is monic, xu=0, and the same epic u witnesses x≡0.

1.2L1L2L3assume-hypalgebra

Assume condition 2. If u,v:U→A satisfy fu=fv, then for the member x:=u−v one has fx=fu−fv=0, hence fx≡0 by [L2] and [L3]. Condition 2 gives x≡0, so [L2] makes x=0, namely u=v. Thus f is monic by [L1].

2.1step 1.1step 1.2∎

Therefore the two conditions are equivalent.

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

Monicity by member cancellation

Statement

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

  1. f is monic.
  2. For all members x and y of A, fx≡fy⟹x≡y.

Facts & Assumptions

Given: A morphism f:A→B.

[L1]

Monicity is equivalent to the rule fz≡0⇒z≡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.1L1L2assume-hypalgebra

Assume f is monic, and suppose fx≡fy. Choose a common witness u:W→X, v:W→Y with fxu=fyv. Then f(xu−yv)=0, so [L1] gives xu−yv≡0. By [L2], this means xu=yv, hence x≡y.

1.2L1L2assume-hyp

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

2.1step 1.1step 1.2∎

Therefore conditions 1 and 2 are equivalent.

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

Epimorphy is detected by members

Statement

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

  1. g is epic.
  2. For every member z:Z→C, there exists a member y:Y→B with gy≡z.

Facts & Assumptions

Given: A morphism g:B→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).

Proof

technique · direct
1.1L4assume-hypconstruct

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

1.2L1L3assume-hypalgebra

Assume condition 2, and write g as an epi-mono factorization B→eI→mC. Apply condition 2 to the identity member 1C:C→C. Then there is y:Y→B with gy≡1C, so [L1] says that gy and 1C determine the same whole subobject of C. Since gy factors through g, [L3] gives [im⁡(gy)]≤[im⁡(g)]=[ ⁣m ⁣], hence [1C]≤[ ⁣m ⁣], which forces [ ⁣m ⁣]=[1C]. Thus g is epic.

2.1step 1.1step 1.2∎

Therefore conditions 1 and 2 are equivalent.

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

A zero arrow is detected by members

Statement

A morphism h:R→S in an abelian category is the zero morphism if and only if hx≡0 for every member x of R.

Facts & Assumptions

Given: A morphism h:R→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.1L1algebra

If h=0, then for every member x one has hx=0, hence hx≡0 by [L1].

1.2L1assume-hyp

Conversely, assume hx≡0 for every member x of R. Apply this to the identity member 1R:R→R. Then h=h1R≡0, so [L1] forces h=0.

2.1step 1.1step 1.2∎

Therefore the displayed member criterion detects exactly the zero morphism.

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

Exactness is detected by members

Statement

For a composable pair A→fB→gC in an abelian category, the following are equivalent:

  1. the pair is exact at B;
  2. gf=0, and for every member y:Y→B with gy≡0 there exists a member x:X→A with fx≡y.

Facts & Assumptions

Given: The composable pair A→fB→gC.

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

Proof

technique · direct
1.1L1L2L5assume-hypchoose

Assume the pair is exact at B, and let y:Y→B satisfy gy≡0. Choose an epic u:W→Y with gyu=0. If A→eI→mB is an image factorization of f, then exactness and [L2] give a map w:W→I with mw=yu.

1.2L2L3L5assume-hyp

Assume condition 2. For any u:U→B with gu=0, we have gu≡0, so condition 2 gives a member x:X→A with fx≡u. By [L3], the members fx and u determine the same subobject of B, and since fx 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 gf=0, [L2] yields exactness at B.

2.1L4L5step 1.1constructalgebra

Pull back the epic e:A→I along w, obtaining x:P→A and an epic α:P→W by [L4]. Then fx=mex=mwα=yuα, so fx≡y.

3.1step 2.1step 1.2∎

Thus conditions 1 and 2 are equivalent.

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

The subtraction surrogate

Statement

Let g:B→C be a morphism and let x:X→B, y:Y→B be members with gx≡gy. Then there exists a member z:Z→B such that gz≡0.

Moreover:

  1. if f:B→D and fx≡0, then fy≡fz;
  2. if h:B→A and hy≡0, then hx≡−hz.

Facts & Assumptions

Given: Morphisms g:B→C, f:B→D, and h:B→A, and members x:X→B, y:Y→B with gx≡gy.

[L1]

The relation gx≡gy 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→X and v:W→Y with gxu=gyv, using [L1], and define z:=yv−xu:W→B. Then gz=gyv−gxu=0 by [L2], so gz≡0 by [L3].

2.1L1L2L3step 1.1constructalgebra

Suppose fx≡0. After replacing W by a common epic refinement of the witnesses for gx≡gy and fx≡0, we may assume fxu=0. Then fyv=f(yv−xu)=fz, so the epic v witnesses fy≡fz.

2.2L1L2L3step 1.1constructalgebra

Suppose hy≡0. After the same common-refinement step, we may assume hyv=0. Then hxu=−h(yv−xu)=−hz, so the epic u witnesses hx≡−hz.

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.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open 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→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-29Open 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

PYXZ¯®gf

Then the square is cartesian if and only if the sequence 0→P→(αβ)X⊕Y→(f,−g)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⊕Y is determined by its two projections, and iXpX+iYpY=1X⊕Y (Biproduct, On a biproduct, the injections and projections satisfy the identity-sum relation).

[L3]

Exactness of 0→P→X⊕Y→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.1L1L2L3assume-hypalgebra

Assume the square is cartesian. Then (f,−g)(αβ)=fα−gβ=0. If u:U→X⊕Y satisfies (f,−g)u=0, write x:=pXu and y:=pYu. Then fx=gy, so the pullback property [L1] gives a unique t:U→P with αt=x and βt=y. By [L2], this implies (αβ)t=u, so (αβ) is a kernel of (f,−g) and the sequence is exact by [L3].

1.2L1L2L3assume-hypconstructalgebra

Assume the sequence is exact. Then [L3] says (αβ) is a kernel of (f,−g), so the square commutes. Given x:U→X and y:U→Y with fx=gy, define u:=iXx+iYy. By [L2], (f,−g)u=fx−gy=0, so the kernel property gives a unique t:U→P with (αβ)t=u. Applying pX and pY yields αt=x and βt=y, proving the pullback property.

2.1step 1.1step 1.2∎

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

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

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

Statement

In a cartesian square in an abelian category

PYXZ¯®gf

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

Facts & Assumptions

Given: The displayed cartesian square.

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

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

2.1L2step 1.1∎

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

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

PYXZ¯®ef

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→P→(αβ)X⊕Y→(f,−e)Z is exact (A square is cartesian exactly when a short sequence is exact).

[L2]

In an abelian category, an exact sequence A→B→C→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⊕Y carries the usual injections from X and Y (Biproduct).

Proof

technique · direct
1.1L1givenL4algebra

By [L1], the cartesian hypothesis makes 0→P→(αβ)X⊕Y→vZ exact, where v:=(f,−e). If r,s:Z→T satisfy rv=sv, then re=−rv iY=−sv iY=se, so the epicity of e gives r=s. Thus v is epic, and the sequence P→(αβ)X⊕Y→vZ→0 is exact.

2.1L2L3L4step 1.1constructalgebra

By [L2], the map v is a cokernel of (αβ). Now let x:X→T and y:Y→T satisfy xα=yβ. By the coproduct side of [L4], there is a unique morphism w:X⊕Y→T with wiX=x and wiY=−y. Then w(αβ)=xα−yβ=0, so the cokernel property gives a unique u:Z→T with uv=w. Composing with iX and iY yields uf=uviX=wiX=x,ue=−uviY=−wiY=y. This is exactly the pushout universal property from [L3].

3.1step 2.1∎

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

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open 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.1given

Take any epimorphism and any pullback of it.

2.1L1step 1.1∎

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

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

The covering criterion for exactness

Statement

For a composable pair X→fY→gZ in an abelian category, the following are equivalent:

  1. the pair is exact at Y;
  2. gf=0, and for every morphism h:W→Y with gh=0, there exist an object V, an epimorphism k:V→W, and a morphism l:V→X such that hk=fl.

Facts & Assumptions

Given: The composable pair X→fY→gZ.

[L1]

Exactness at Y is equivalent to the member criterion gy≡0⇒∃x,  fx≡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.1L1L2assume-hypchooseconstruct

Assume the pair is exact. Then [L1] gives gf=0. Now let h:W→Y satisfy gh=0. Then gh≡0, so [L1] gives a member x:U→X with fx≡h. By [L2], there exist an object V and epimorphisms a:V→U and k:V→W such that fxa=hk. Putting l:=xa proves the covering condition.

1.2L1L2assume-hypconstruct

Assume gf=0 and the covering condition. Let y:W→Y be a member with gy≡0. Choose an epic u:W′→W with gyu=0, and apply the covering condition to h:=yu. This gives an epic k:V→W′ and a map l:V→X with yuk=fl. Since uk is epic, [L2] says exactly that fl≡y. Therefore [L1] gives exactness at Y.

2.1step 1.1step 1.2∎

Thus the covering condition is equivalent to exactness.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-29Open 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 gf=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 fx≡y in Exactness is detected by members is the same lifting assertion as the existence of an epic cover k:V→W and a morphism l:V→X with yk=fl in The covering criterion for exactness.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-29Open 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

0ABC00A0B0C00iapbci0p0

the induced kernel sequence 0→ker⁡(a)→ker⁡(b)→ker⁡(c) is exact at ker⁡(a) and at ker⁡(b).

Dually, the induced cokernel sequence coker⁡(a)→coker⁡(b)→coker⁡(c)→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).

[L4]

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

Proof

technique · direct
1.1L1L2

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)→ker⁡(b)→ker⁡(c) at ker⁡(b).

1.2L1L3algebra

Let u:ker⁡(a)→ker⁡(b) be the induced map and choose kernel arrows ka:ker⁡(a)→A and kb:ker⁡(b)→B. If us=ut, then ikas=kbus=kbut=ikat. The map i is monic by [L1], and ka is monic by [L3], so s=t. Hence u is monic, which is exactly exactness of 0→ker⁡(a)→ker⁡(b) at ker⁡(a).

2.1L4step 1.1step 1.2

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

3.1step 1.1step 1.2step 2.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).

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

Exactness of kernel and cokernel sequences under endpoint hypotheses

Statement

Consider a commutative diagram in an abelian category

XYZUVWf®g¯°kl

Then:

  1. if the top row is exact and k is monic, the induced sequence ker⁡(α)→ker⁡(β)→ker⁡(γ) is exact;
  2. if the bottom row is exact and g is epic, the induced sequence coker⁡(α)→coker⁡(β)→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).

Proof

technique · direct
1.1L3assume-hypconstruct

Assume the top row is exact and k is monic. Choose kernels h:ker⁡(α)→X, i:ker⁡(β)→Y, and j:ker⁡(γ)→Z. By [L3], the commutative diagram induces morphisms a:ker⁡(α)→ker⁡(β),b:ker⁡(β)→ker⁡(γ) with ia=fh,jb=gi.

2.1L1L3step 1.1construct

To prove exactness of ker⁡(α)→aker⁡(β)→bker⁡(γ), apply the covering criterion [L1] to the pair (a,b). Let u:T→ker⁡(β) satisfy bu=0. Then giu=jbu=0, so exactness of the top row gives an object P, an epimorphism e:P→T, and a morphism x:P→X with iue=fx.

3.1L1L3L4step 1.1step 2.1algebra

Applying β to the displayed equality gives 0=βiue=kαx. Since k is monic, αx=0. The kernel property of h therefore gives x′:P→ker⁡(α) with hx′=x. Now iue=fhx′=iax′, so monicity of i from [L4] yields ue=ax′. Also jba=gia=gfh=0, so monicity of j from [L4] gives ba=0. Thus the pair (a,b) satisfies both parts of the covering criterion [L1], and the kernel sequence is exact.

4.1L2step 1.1step 2.1step 3.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 gop, kernels become cokernels, and [L2] transports the resulting exact sequence back to the original category.

5.1step 3.1step 4.1∎

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

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

The kernel-cokernel sequence of a composite

Statement

For composable morphisms A→fB→gC in an abelian category, there is an exact sequence 0→ker⁡(f)→ker⁡(gf)→ker⁡(g)→qfkgcoker⁡(f)→coker⁡(gf)→coker⁡(g)→0, where kg:ker⁡(g)→B is a kernel of g, qf:B→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→fB→gC.

[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→A (The cokernel of the zero map out of the zero object is the target, and dually for kernels).

Proof

technique · direct
1.1L3construct

Choose kernels kf:Kf→A,kgf:Kgf→A,kg:Kg→B and cokernels qf:B→Qf,qgf:C→Qgf,qg:C→Qg. Because gfkf=0, [L3] gives a canonical map u:Kf→Kgf with kgfu=kf. Likewise gfkgf=0 gives a canonical map v:Kgf→Kg with kgv=fkgf. Put δ:=qfkg:Kg→Qf. Since qgfgf=0 and qgg=0, [L3] also gives canonical maps w:Qf→Qgf and x:Qgf→Qg.

2.1L5step 1.1algebra

The map u is monic: if us=ut, then kfs=kgfus=kgfut=kft, and monicity of kf from [L5] forces s=t. So the sequence is exact at ker⁡(f).

2.2L1L4step 1.1construct

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→C is monic. Hence the induced sequence ker⁡(0)→ker⁡(gf)→ker⁡(g) is exact. By [L4], ker⁡(0) is represented by 1ker⁡(f), so this is exactly the sequence ker⁡(f)→uker⁡(gf)→vker⁡(g) at ker⁡(gf).

2.3L1L4step 1.1construct

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 1C is monic. Therefore the induced sequence ker⁡(gf)→ker⁡(g)→ker⁡(0coker⁡(f),0) is exact. By [L4], the last kernel is represented by 1coker⁡(f), and the induced map is qfkg=δ. Hence ker⁡(gf)→vker⁡(g)→δcoker⁡(f) is exact at ker⁡(g).

3.1L2step 1.1step 2.1step 2.2step 2.3

Apply steps 2.1 to 2.3 in the opposite category to the composable pair C→gopB→fopA. Using [L2], the resulting exactness statements transport back to exactness of ker⁡(g)→δcoker⁡(f)→wcoker⁡(gf)→xcoker⁡(g)→0 at coker⁡(f), at coker⁡(gf), and at coker⁡(g).

4.1step 2.1step 2.2step 2.3step 3.1∎

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

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→X, and two comembers x:A→X and y:A→Y are equivalent when there exist one object W and monomorphisms u:X↣W,v:Y↣W with ux=vy.

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

RemarkRemark: AI-adaptedProof: Not applicableaudited 2026-08-29Open 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-29Open item page →

Hom is left exact in each variable

Statement

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

  1. If 0→A→B→C is exact, then 0→A(X,A)→A(X,B)→A(X,C) is exact in Ab.
  2. If A→B→C→0 is exact, then 0→A(C,X)→A(B,X)→A(A,X) is exact in Ab.

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 Aop(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 Ab, which is abelian (Abelian groups form an abelian category).

Proof

technique · direct
1.1L1L2L3L4assume-hyp

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

2.1L2L3L4step 1.1

Passing to the opposite category, the exact sequence A→B→C→0 becomes a left-exact sequence in Aop. Applying step 1.1 there to the representable functor Aop(X,−)=A(−,X) gives 0→A(C,X)→A(B,X)→A(A,X) exact in Ab.

3.1step 1.1step 2.1∎

Hence Hom is left exact in each variable.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open 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 Ab, the short exact sequence 0→Z→×2Z→Z/2→0.

[L1]

The category Ab 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.1L1L2given

Apply Ab(−,Z) to the given short exact sequence. This yields 0→Hom⁡(Z/2,Z)→Hom⁡(Z,Z)→(×2)∗Hom⁡(Z,Z), which is left exact by [L2].

2.1step 1.1algebra

The group Hom⁡(Z,Z) is Z, and precomposition with ×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.

3.1step 2.1∎

Therefore the contravariant Hom functor need not be exact.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open 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.

  1. P is projective if and only if the functor A(P,−) is exact.
  2. 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.1L1L2L4

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.

2.1L1L3L4∎

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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29Open 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:AJ→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).

[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 (⋁iBi)∧C=⋁i(Bi∧C).

Proof

technique · direct
1.1L1L3L5assume-hyp

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.

1.2L2L3L4assume-hypconstruct

Conversely, assume every filtered colimit functor is exact. Let I be a small directed poset indexing a family of monomorphisms bi:Bi↣A, and let c:C↣A represent a fixed subobject of A. For each i∈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 Bi∧C. These pullback squares assemble into a diagram in AI. 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.

2.1L4step 1.2algebra

The image of b:B→A is the join ⋁iBi: each bi factors through b, so every Bi 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→C is ⋁i(Bi∧C).

3.1L1L4step 1.2step 2.1

Because the square of step 1.2 is a pullback, [L4] identifies the image of P→C with the meet of the subobject represented by im⁡(b) and the fixed subobject C. Using step 2.1, this gives (⋁iBi)∧C=⋁i(Bi∧C), which is exactly AB5 by [L1].

4.1step 1.1step 3.1∎

Therefore AB5 is equivalent to exactness of filtered colimits.

5 · Examples, counterexamples and false statements

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

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

Statement

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

Facts & Assumptions

Given: The ring R=k[ε]/(ε2), the quotient q:R→k=R/(ε), and the inclusion i:k→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.1L1givenalgebra

In R-Mod, the sequence 0→k→iR→qk→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.

2.1L2step 1.1assume-hypalgebra

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

3.1L2step 2.1constructalgebra

Let T:=R(N)⊕k(N). Direct-summing step 1.1 with 0→T→1TT→0→0 gives 0→k⊕T→R⊕T→q⊕0k→0. Any section of q⊕0 would project to a section of q, so this stabilized sequence is still nonsplit by step 2.1.

4.1step 3.1algebra

Countable shifts give R⊕T≅T, k⊕T≅T, and (k⊕T)⊕k≅T, because adding finitely many R- or k-summands does not change R(N)⊕k(N). Hence R⊕T≅(k⊕T)⊕k.

5.1step 3.1step 4.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.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open 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 Ab and the identity member 1Z:Z→Z.

[L1]

The category Ab 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.1L1L2algebra

In Ab, the identity member satisfies 1Z≡−1Z because 1Z(−1Z)=(−1Z)1Z and the automorphism −1Z is epic.

1.2L2assume-hypalgebra

If member classes carried a group law induced from arrow addition, then [1Z]+[1Z]=[1Z]+[−1Z]=[0]. But the left-hand class is represented by 2⋅1Z:Z→Z, and [L2] says 2⋅1Z≡0 would force 2⋅1Z=0, which is false in Ab.

2.1step 1.1step 1.2∎

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

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

Two morphisms agreeing on every member need not be equal

Statement refuted

If two morphisms f,g:A→B satisfy fx≡gx for every member x of A, then f=g.

Facts & Assumptions

Given: The abelian category Ab and the two endomorphisms 1Z,−1Z:Z→Z.

[L1]

The category Ab 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.1L1L2algebra

Let x:X→Z be any member. Then (−1Z)x=x(−1X), and the automorphism −1X is epic. Therefore 1Zx≡(−1Z)x.

1.2L1algebra

Nevertheless 1Z≠−1Z, since they send 1∈Z to different integers. So memberwise equivalence of composites does not force equality of the morphisms themselves.

2.1step 1.1step 1.2∎

This refutes the statement.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open 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

0ZZZ=200ZZZ=20£2£2£20£2

Facts & Assumptions

Given: In Ab, the commutative diagram above.

[L1]

The category Ab 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).

Proof

technique · direct
1.1L1givenalgebra

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

2.1L2step 1.1algebra

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

3.1step 2.1algebra

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

4.1step 3.1∎

This refutes the statement.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

FALSE: two morphisms that agree on every member are equal

Statement

If f,g:A→B satisfy fx≡gx 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.1L2

The witness in [L2] gives distinct morphisms f and g with fx≡gx for every member x. So the stated implication fails.

2.1L1step 1.1∎

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

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open 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.1L2

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

2.1L1step 1.1∎

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

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

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

Statement

In any pointed category with pullbacks, the member relation ≡ is transitive.

Facts & Assumptions

Given: The weakened hypothesis of the statement.

Refutation

technique · direct
1.1constructalgebra

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:=1A:A→A,z:C[t−1]↪A be the two localization inclusions and the identity member. The map x is epic: if φ,ψ:A→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 eR, so they are equal; hence φ=ψ. The same argument shows that z is epic. Therefore x≡y and y≡z.

1.2constructalgebra

The pullback of x and z is the constant subring C, because inside C[t,t−1] one has C[t]∩C[t−1]=C. Its two projections are the constant-term inclusions p1:C→C[t],p2:C→C[t−1].

2.1step 1.2assume-hypalgebra

Suppose x≡z. Then there would exist a ring T and epimorphisms q:T→C[t] and r:T→C[t−1] with xq=zr. By the pullback property from step 1.2, there would be a map m:T→C with q=p1m and r=p2m. Since q is epic, p1 would also be epic. But p1 is not epic: the evaluation maps ev⁡0,ev⁡1:C[t]→C are distinct and satisfy ev⁡0p1=ev⁡1p1=1C. This contradiction shows that x≢z.

3.1step 1.1step 2.1∎

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

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open 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.1L2

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

2.1L1step 1.1∎

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

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

FALSE: the subtraction rule produces a unique member

Statement

In the subtraction surrogate, the member z with gz≡0 is unique.

Facts & Assumptions

Given: The category Ab.

[L1]

The category Ab is abelian (Abelian groups form an abelian category).

[L2]

The subtraction surrogate applies whenever gx≡gy (The subtraction surrogate).

Refutation

technique · direct
1.1L1L2

In Ab, take B=Z, C=0, g=0:Z→0, and x=y=0Z,Z:Z→Z. Then gx=gy=0, so the hypotheses of [L2] are satisfied.

2.1L1step 1.1algebra

Both z0:=0Z,Z and z1:=1Z satisfy gzi=0, hence gzi≡0. Since z0≠z1, the asserted uniqueness fails in this instance.

3.1step 2.1∎

Therefore the statement is false.

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→fB→gC 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.1L1L2

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.

2.1step 1.1∎

Therefore the statement is false.

Sources