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.

✓ 44 results · all verified · 19 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.

Abelian Categories

1 · Prerequisites

2 · Summary

This page builds the image and coimage of a morphism before it ever says that the two agree. That ordering is the point: the canonical map coim⁡(f)→im⁡(f) is constructed first, and only then made invertible in the definition of an abelian category.

The page then develops the standard structural consequences. The basic ones are balancedness, normality of monomorphisms and epimorphisms, epi-mono factorization, pullbacks of epimorphisms, the quotient and isomorphism theorems, and the exact-functor criteria. It also proves the equivalence with Freyd's alternative axiomatisation. The later diagram arguments use intrinsic kernel, cokernel and pullback constructions.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Normal monomorphisms and conormal epimorphisms

Definition

Let m:A→B be a monomorphism and let e:A→B be an epimorphism (Monomorphism and epimorphism by left and right cancellation) in a category with zero morphisms and the relevant kernels or cokernels (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

The monomorphism m is normal when it is a kernel of some morphism out of B. Dually, the epimorphism e is conormal when it is a cokernel of some morphism into A.

So a normal monomorphism is not merely left-cancellable: it is the inclusion of the part of the codomain killed by a specified morphism. A conormal epimorphism is the dual quotient map.

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

The kernel of a monomorphism is zero and the cokernel of an epimorphism is zero

Statement

Let C be a category with a zero object and the needed kernels and cokernels. If m:A→B is monic and k:K→A is a kernel of m, then K is a zero object and k is the zero morphism into A.

Dually, if e:A→B is epic and q:B→Q is a cokernel of e, then Q is a zero object and q is the zero morphism out of B.

Facts & Assumptions

Given: A zero object 0, a monomorphism m:A→B with kernel k:K→A, and an epimorphism e:A→B with cokernel q:B→Q.

[L1]

A zero object is both initial and terminal, so there are unique morphisms 0→X and X→0 for every object X (Initial object, terminal object, and zero object).

[L2]

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

[L3]

A kernel of m is a morphism k with mk=0 through which every morphism h with mh=0 factors uniquely; a cokernel is dual (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

Proof

technique · direct
1.1L1L2L3

If h:X→A satisfies mh=0, then also m0X,A=0, so [L2] gives h=0X,A. Therefore the unique map 0→A from [L1] has the kernel universal property for m, because every morphism killed by m factors uniquely through 0.

2.1L1L2L3step 1.1∎

Kernels are unique up to a unique compatible isomorphism, so the displayed kernel k:K→A is isomorphic to the zero morphism 0→A from step 1.1. Hence K is a zero object and k is the zero map into A. The cokernel claim is the formal dual of the same argument with right cancellation in [L2].

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

The cokernel of the zero map out of the zero object is the target, and dually for kernels

Statement

Let 0 be a zero object in a category with zero morphisms and kernels and cokernels. For every object A, the identity 1A:A→A is a cokernel of the zero morphism 0→A. Dually, 1A is a kernel of the zero morphism A→0.

So coker⁡(0→A)≅A and ker⁡(A→0)≅A.

Facts & Assumptions

Given: A zero object 0 and an object A.

[L1]

There is a unique morphism 0→A and a unique morphism A→0 (Initial object, terminal object, and zero object).

[L2]

A cokernel of u is a morphism q with qu=0 through which every morphism annihilating u factors uniquely, and a kernel is dual (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

Proof

technique · direct
1.1L1L2

Let u:0→A be the unique map from [L1]. Since every composite h∘u:0→X equals the unique map 0→X, every morphism h:A→X annihilates u. Each such h factors uniquely through 1A, namely as h=h∘1A. Therefore 1A is a cokernel of u.

2.1L1L2step 1.1∎

The dual argument with the unique map A→0 shows that 1A is also a kernel of A→0. So both displayed identifications hold up to the unique compatible isomorphism of kernels and cokernels.

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

Image and coimage in a category with kernels and cokernels

Definition

Let f:A→B be a morphism in a category with kernels and cokernels (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

The image of f is the kernel of a cokernel of f:

im⁡(f):=ker⁡(coker⁡(f)).

The coimage of f is the cokernel of a kernel of f:

coim⁡(f):=coker⁡(ker⁡(f)).

This page uses the object notation im⁡(f) and coim⁡(f). Their defining arrows are the corresponding kernel and cokernel maps.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

A morphism factors uniquely through its coimage

Statement

Let f:A→B be a morphism in a category with kernels and cokernels. If k:K→A is a kernel of f and q:A→coim⁡(f) is a cokernel of k, then there exists a unique morphism f~:coim⁡(f)→B with

f~∘q=f.

Facts & Assumptions

Given: A morphism f:A→B, a kernel k:K→A of f, and a cokernel q:A→coim⁡(f) of k.

[L1]

The coimage of f is the cokernel of a kernel of f (Image and coimage in a category with kernels and cokernels).

Proof

technique · direct
1.1L1given

Because k is a kernel of f, one has f∘k=0.

2.1L1step 1.1∎

The morphism q is a cokernel of k, so step 1.1 gives a unique f~:coim⁡(f)→B with f~q=f. That is exactly the claimed factorization through the coimage.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

A morphism factors uniquely through its image

Statement

Let f:A→B be a morphism in a category with kernels and cokernels. If c:B→C is a cokernel of f and i:im⁡(f)→B is a kernel of c, then there exists a unique morphism f^:A→im⁡(f) with

i∘f^=f.

Facts & Assumptions

Given: A morphism f:A→B, a cokernel c:B→C of f, and a kernel i:im⁡(f)→B of c.

[L1]

The image of f is the kernel of a cokernel of f (Image and coimage in a category with kernels and cokernels).

Proof

technique · direct
1.1L1given

Because c is a cokernel of f, one has c∘f=0.

2.1L1step 1.1∎

The morphism i is a kernel of c, so step 1.1 gives a unique f^:A→im⁡(f) with if^=f. That is the claimed factorization through the image.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The canonical morphism from the coimage to the image exists and is unique

Statement

Let f:A→B be a morphism in a category with kernels and cokernels. Write qf:A→coim⁡(f) for the coimage projection and if:im⁡(f)→B for the image inclusion. Then there exists a unique morphism

f‾:coim⁡(f)→im⁡(f)

such that

if∘f‾∘qf=f.

Facts & Assumptions

Given: A morphism f:A→B, its coimage projection qf, and its image inclusion if.

[L1]

The morphism f factors uniquely through its coimage (A morphism factors uniquely through its coimage).

[L2]

The morphism f factors uniquely through its image (A morphism factors uniquely through its image).

Proof

technique · direct
1.1L1L2L3

By [L1], there is a unique morphism f~:coim⁡(f)→B with f~qf=f. Let cf:B→Cf be a cokernel of f. Then cff~qf=cff=0, and [L3] makes qf epic, so cff~=0. Because if:im⁡(f)→B is a kernel of cf, there is a unique map f‾:coim⁡(f)→im⁡(f) with iff‾=f~.

2.1L1L2L3step 1.1∎

Composing the identity of step 1.1 with qf gives iff‾qf=f~qf=f, so f‾ has the required property. If another map u:coim⁡(f)→im⁡(f) also satisfies ifuqf=f, then ifu=f~ by the epicity of qf from [L3], and the uniqueness of the kernel factorization in step 1.1 gives u=f‾.

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

The coimage projection is epic and the image inclusion is monic

Statement

For every morphism f in a category with kernels and cokernels, the defining map qf:A→coim⁡(f) is epic and the defining map if:im⁡(f)→B is monic.

Facts & Assumptions

Given: A morphism f:A→B with coimage projection qf and image inclusion if.

[L1]

The coimage is defined as a cokernel and the image as a kernel (Image and coimage in a category with kernels and cokernels).

[L2]

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

Proof

technique · direct
1.1L1L2

By [L1], the map qf is a cokernel of a kernel of f. Therefore [L2] makes qf epic.

2.1L1L2∎

Again by [L1], the map if is a kernel of a cokernel of f. Therefore [L2] makes if monic.

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

Abelian category

Definition

An abelian category is an additive category (Additive category) in which every morphism has a kernel and a cokernel, and in which for every morphism f the canonical comparison morphism

coim⁡(f)⟶im⁡(f)

constructed in The canonical morphism from the coimage to the image exists and is unique is an isomorphism.

The first two clauses are Grothendieck's AB1, while the invertibility of the canonical map is this page's working form of AB2.

RemarkRemark: Literature-sourcedProof: Not applicableaudited 2026-08-28Open item page →

This page uses Grothendieck's AB1 and AB2 labels, and records the competing conventions

Grothendieck's original Tohoku paper labels the two extra clauses on top of additivity as AB1 and AB2: every morphism has a kernel and a cokernel, and the canonical map Coim⁡(f)→Im⁡(f) is an isomorphism. This page follows that convention.

Two cautions matter because both conventions occur in the modern literature. First, there is no Grothendieck axiom "AB0": additivity is a standing hypothesis, not a numbered clause. Second, Weibel's Appendix A uses the label "AB2" for a different statement, namely that every monomorphism is the kernel of its cokernel. That statement is proved later on this page as Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel.

The Stacks Project avoids the AB labels altogether and writes the same content directly as the definition of an abelian category. That is compatible with this page's choice; it is a notation split, not a mathematical disagreement.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

An abelian category is balanced

Statement

If f:A→B in an abelian category is both monic and epic, then f is an isomorphism.

Facts & Assumptions

Given: An abelian category and a morphism f:A→B that is both monic and epic.

[L1]

The kernel of a monomorphism is zero, and the cokernel of an epimorphism is zero (The kernel of a monomorphism is zero and the cokernel of an epimorphism is zero).

[L2]

The cokernel of 0→A is A, and the kernel of B→0 is B (The cokernel of the zero map out of the zero object is the target, and dually for kernels).

[L3]

Every morphism has a canonical factorization A→coim⁡(f)→im⁡(f)→B (The canonical morphism from the coimage to the image exists and is unique).

[L4]

In an abelian category the canonical map coim⁡(f)→im⁡(f) is an isomorphism (Abelian category).

Proof

technique · direct
1.1L1L2L3

Because f is monic and epic, [L1] identifies ker⁡(f) and coker⁡(f) with zero objects. Hence [L2] gives isomorphisms qf:A⟶∼coim⁡(f) and if:im⁡(f)⟶∼B for the coimage projection and image inclusion of f.

2.1L3L4step 1.1∎

By [L4], the middle map f‾:coim⁡(f)→im⁡(f) is an isomorphism. Since f=iff‾qf, step 1.1 shows that f is a composite of three isomorphisms, so f itself is an isomorphism.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The opposite of an abelian category is abelian

Statement

If A is an abelian category, then the opposite category Aop is also abelian.

Facts & Assumptions

Given: An abelian category A.

[L1]

An abelian category is additive and every morphism in it has a kernel and a cokernel (Abelian category).

[L2]

The opposite of an additive category is additive (Additive categories are closed under passage to the opposite).

[L3]

Passing to the opposite reverses every morphism while keeping the same objects (Opposite category Cop).

Proof

technique · direct
1.1L1L2L3

By [L1] and [L2], the opposite category is additive. Under [L3], a kernel in A becomes a cokernel in Aop, and a cokernel becomes a kernel, so every morphism of Aop also has both.

2.1L1L3step 1.1∎

The image of fop in the opposite category is the opposite of the coimage of f, and the coimage of fop is the opposite of the image of f. Therefore the canonical comparison for fop is the opposite of the canonical comparison for f, which is an isomorphism by [L1]. So Aop satisfies the same AB2 clause and is abelian.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

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

Statement

In an abelian category, every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel.

Facts & Assumptions

Given: An abelian category and a monomorphism m:A→B with cokernel c:B→C.

[L3]

The image and coimage are defined by kernels and cokernels (Image and coimage in a category with kernels and cokernels).

[L4]

A morphism factors through its image, and the canonical coim⁡→im⁡ map exists (A morphism factors uniquely through its image, The canonical morphism from the coimage to the image exists and is unique).

[L5]

In an abelian category the canonical coim⁡(m)→im⁡(m) map is an isomorphism (Abelian category).

[L6]

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

Proof

technique · direct
1.1L1L2L3

By [L1], the kernel of m is zero. Therefore [L2] identifies the coimage projection qm:A→coim⁡(m) with an isomorphism.

2.1L3L4L5step 1.1

By definition, the image inclusion im:im⁡(m)→B is a kernel of the cokernel c. Since m=imm‾qm by [L4], and both qm and m‾ are isomorphisms by step 1.1 and [L5], there is an isomorphism u:A⟶∼im⁡(m) with imu=m. So m is itself a kernel of c up to the unique compatible isomorphism of kernel objects.

3.1L6step 2.1∎

By [L6], the opposite of an abelian category is again abelian. Applying step 2.1 there to the opposite of an epimorphism gives that every epimorphism in the original category is the cokernel of its kernel.

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

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

Statement

Every morphism f:A→B in an abelian category admits a factorization

A⟶efIf⟶mfB

with ef epic and mf monic. If also f=m′e′ with e′ epic and m′ monic, then there is a unique isomorphism u:If→I′ such that

m′=mfu−1,u∘ef=e′.

Facts & Assumptions

Given: An abelian category and a morphism f:A→B.

[L1]
[L2]

The coimage projection is epic and the image inclusion is monic (The coimage projection is epic and the image inclusion is monic).

[L3]

In an abelian category the canonical coimage-to-image map is an isomorphism (Abelian category).

[L4]

Abelian categories are balanced (An abelian category is balanced).

Proof

technique · direct
1.1L1L2L3

Let qf:A→coim⁡(f) and if:im⁡(f)→B be the defining maps. By [L1], f factors as f=iff‾qf, and [L2] makes qf epic and if monic. Since f‾ is an isomorphism by [L3], the composite ef:=f‾qf:A→im⁡(f) is epic, so f=ifef is an epic-monic factorization.

2.1L2L5step 1.1

Suppose also f=m′e′ with e′ epic and m′ monic. Then coker⁡(m′)f=0, so coker⁡(m′)ifef=0, and the epicity of ef gives coker⁡(m′)if=0. Since m′ is a kernel of its cokernel by [L5], if factors uniquely through m′ as if=m′u. Reversing the roles of if and m′ gives m′=ifv for a unique v.

3.1L4step 2.1∎

From step 2.1 one gets m′=m′uv and if=ifvu, so monicity gives uv=1 and vu=1. Thus u is an isomorphism. Finally, m′uef=ifef=f=m′e′, and monicity of m′ gives uef=e′. Any other comparison map with the same property equals u by the uniqueness in step 2.1.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The image is the least subobject through which a morphism factors

Statement

Let f:A→B be a morphism in an abelian category, and let if:im⁡(f)→B be the image inclusion. Then f factors through if, and if f=n∘g with n:N→B monic, then

[im⁡(f)]≤[n]

in the subobject order of B.

Facts & Assumptions

Given: An abelian category, a morphism f:A→B, and a factorization f=n∘g through a monomorphism n:N→B.

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

Proof

technique · direct
1.1L1L2

By [L1], f admits an epic-monic factorization f=if∘ef, so it factors through its image.

2.1L1L3step 1.1

Because f=ng, the composite coker⁡(n)∘f is zero. Using step 1.1, this becomes coker⁡(n) ifef=0. Since ef is epic, coker⁡(n) if=0. Now [L3] says that n is a kernel of coker⁡(n), so if factors uniquely through n.

3.1L2step 2.1∎

The factorization in step 2.1 is exactly the order relation [im⁡(f)]≤[n] from [L2]. Hence the image is the least subobject of B through which f factors.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

In an abelian category, monic means zero kernel and epic means zero cokernel

Statement

For a morphism f in an abelian category:

  1. f is monic if and only if its kernel is zero;
  2. f is epic if and only if its cokernel is zero.

Facts & Assumptions

Given: An abelian category and a morphism f in it.

[L1]

An abelian category is additive, hence preadditive and equipped with a zero object (Abelian category).

[L2]

In a preadditive category with a zero object, a morphism is monic exactly when its kernel is zero (In a preadditive category with a zero object, a morphism is monic exactly when its kernel is zero).

[L3]

In a preadditive category with a zero object, a morphism is epic exactly when its cokernel is zero (In a preadditive category with a zero object, a morphism is epic exactly when its cokernel is zero).

Proof

technique · direct corollary
1.1L1L2

The monomorphism claim is exactly [L2], because [L1] supplies the preadditive and zero-object hypotheses that [L2] needs.

2.1L1L3∎

The epimorphism claim is exactly [L3], for the same reason.

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

Freyd's axioms A0, A1, A1*, A2, A2*, A3, and A3* for abelian categories

Definition

Freyd's axiomatisation of an abelian category asks for the following data and properties.

  1. A0. A zero object exists (Initial object, terminal object, and zero object).
  2. A1. Every pair of objects has a product.
  3. A1*. Every pair of objects has a coproduct.
  4. A2. Every morphism has a kernel (Equalizers and coequalizers as limits and colimits of a parallel pair).
  5. A2*. Every morphism has a cokernel (Equalizers and coequalizers as limits and colimits of a parallel pair).
  6. A3. Every monomorphism is a kernel (Monomorphism and epimorphism by left and right cancellation).
  7. A3*. Every epimorphism is a cokernel.

Unlike the working definition on this page, no additive enrichment is part of the data. Freyd's point is that the additive structure can be recovered from the remaining axioms.

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

Freyd's axioms force the additive structure and recover the AB2 definition

Statement

If a category satisfies Freyd's axioms A0, A1, A1*, A2, A2*, A3, and A3*, then it is additive. Moreover, for every morphism the canonical map from the coimage to the image is an isomorphism, so the category is abelian in the working sense of Abelian category.

Facts & Assumptions

Given: A category A satisfying Freyd's axioms A0, A1, A1*, A2, A2*, A3, and A3*.

[L1]

Freyd's axioms are the zero-object, binary product, binary coproduct, kernel, cokernel, normal-monic, and conormal-epic clauses listed in Freyd's axioms A0, A1, A1*, A2, A2*, A3, and A3* for abelian categories.

[L2]

Once one object carries both the product and coproduct structures with the standard zero equations, the canonical comparison is the identity and the object is a biproduct (Biproduct data characterisation without addition).

[L3]

Finite biproducts give a canonical commutative-monoid enrichment on hom-sets, and [L4] makes that enrichment unique (A category with finite biproducts is enriched in commutative monoids, The commutative-monoid enrichment of a category with finite biproducts is unique).

[L4]

Earlier on this page, image, coimage, their factorization maps, and the canonical coimage-to-image morphism were constructed from kernels and cokernels (Image and coimage in a category with kernels and cokernels, A morphism factors uniquely through its coimage, A morphism factors uniquely through its image, The canonical morphism from the coimage to the image exists and is unique).

Proof

technique · direct
1.1L1

Freyd's axioms already make A balanced: if m:A→B is monic and epic, the normality clause writes m as a kernel of some g:B→C, so gm=0; because m is epic, g=0, and the identity 1B is a kernel of 0B,C, so m is isomorphic to 1B.

2.1L1L2step 1.1

Let S=A⊔B and P=A×B be the coproduct and product supplied by [L1]. The split epics [1A,0]:S→A and [0,1B]:S→B are cokernels of the opposite injections because maps out of a coproduct are determined by the injections; dually the split monics ⟨1A,0⟩:A→P and ⟨0,1B⟩:B→P are kernels of the opposite projections because maps into a product are determined by the projections. Therefore the canonical comparison c:S→P is both monic and epic, so step 1.1 makes it an isomorphism. Thus binary biproducts exist, and together with the zero-object clause this gives finite biproducts.

3.1L3step 1.1step 2.1

By [L3], the finite biproducts from step 2.1 give a canonical commutative-monoid law on each hom-set. On A⊕A, Mitchell's shear θ=(1A1A01A) is monic and epic by the same kernel-cokernel argument used in step 2.1, hence invertible by step 1.1. Writing θ−1=(abcd), the matrix identity θθ−1=1 yields 1A+b=0 in the monoid law of [L3]. For every x:A→B, the morphism xb is therefore an additive inverse of x, so the hom-monoids are abelian groups. Hence A is preadditive, and with finite biproducts it is additive.

4.1L1L4L5step 3.1

Let f:A→B, let k:K→A be its kernel, let p:A→Q=coim⁡(f) be the cokernel of k, let m:I=im⁡(f)→B be the kernel of a cokernel of f, and let u:Q→I be the canonical morphism from [L4]. Put i:=mu:Q→B. To show that i is monic, let x:X→Q satisfy ix=0, let q:Q→Q′ be a cokernel of x, and write i=jq. Since qp is a composite of cokernels, [L5] makes it epic, so the conormality clause gives some h:H→A with qp=coker⁡(h). Now fh=iph=jqph=0, so h factors through k; hence ph=0. Because qp is a cokernel of h, the map p factors through qp as p=p′qp. Since p is epic by [L5], p′q=1Q, so q is monic. Then qx=0 forces x=0, and i is monic.

5.1L1L4L5step 1.1step 4.1

The dual argument shows that the factorization map e:=up:A→I is epic: starting from a kernel of a map out of I, one passes to the opposite category and repeats step 4.1. Since m is monic and p is epic by [L5], the equalities mu=i and up=e imply that u itself is monic and epic. Step 1.1 then makes u an isomorphism.

6.1step 3.1step 5.1∎

Thus every morphism has kernels and cokernels and an invertible canonical coimage-to-image comparison. Together with the additivity from step 3.1, this is exactly the working abelian definition of Abelian category.

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

Freyd and Mitchell's characterisation of abelian categories

Statement

For a category A, the following are equivalent.

  1. A is abelian in the working sense of Abelian category.
  2. A satisfies Freyd's axioms A0, A1, A1*, A2, A2*, A3, and A3*.
  3. A has a zero object, pullbacks, and pushouts, and every monomorphism is a kernel while every epimorphism is a cokernel.

Facts & Assumptions

Given: A category A.

[L1]

An abelian category is additive, has kernels and cokernels, and has invertible coimage-image comparison maps (Abelian category).

[L2]

In an abelian category 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).

[L3]

Freyd's axioms imply the working abelian definition (Freyd's axioms force the additive structure and recover the AB2 definition).

[L4]

An additive category with all kernels and cokernels has all finite limits and finite colimits (An additive category with all kernels and cokernels has all finite limits and colimits).

Proof

technique · direct
1.1L1L2

If clause 1 holds, then [L1] gives additivity, kernels, and cokernels. The zero object and binary biproducts in [L1] supply the zero-object, product, and coproduct clauses, while [L2] supplies the normality and conormality clauses. So clause 1 implies clause 2.

1.2L3

Clause 2 implies clause 1 by [L3].

2.1L1L3L4step 1.2

If clause 2 holds, then step 1.2 and [L4] give all finite limits and finite colimits, hence in particular pullbacks and pushouts. So clause 2 implies clause 3. Conversely, if clause 3 holds, then the pullback of A→0←B is a product of A and B, the pushout of A←0→B is a coproduct, the pullback of A→fB←0 is a kernel of f, and the pushout of 0←A→fB is a cokernel of f. Together with the stated normal and conormal clauses, that is exactly Freyd's list.

3.1step 1.1step 1.2step 2.1∎

Steps 1.1, 1.2, and 2.1 prove the three-way equivalence.

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

Additivity can be derived rather than postulated, depending on the axiomatisation

The working definition on this page starts from additivity because it is the cleanest form for later citations. Freyd's axiomatisation goes the other way: the additive structure is a theorem recovered from normality, conormality, products, coproducts, kernels, and cokernels.

That is why items Abelian category, Freyd's axioms A0, A1, A1*, A2, A2*, A3, and A3* for abelian categories, and Freyd's axioms force the additive structure and recover the AB2 definition coexist rather than compete. The first is the library's working interface; the second and third explain why that interface could have been packaged differently without changing the mathematics.

The uniqueness part of the recovered enrichment is already abstracted in The uniqueness of the enrichment is an Eckmann-Hilton phenomenon: once the finite biproduct law exists, there is no second compatible addition to choose.

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

An abelian category has all finite limits and all finite colimits

Statement

Every abelian category has all finite limits and all finite colimits.

Facts & Assumptions

Given: An abelian category A.

[L1]

An abelian category is additive and every morphism has a kernel and a cokernel (Abelian category).

[L2]

An additive category with all kernels and cokernels has all finite limits and all finite colimits (An additive category with all kernels and cokernels has all finite limits and colimits).

Proof

technique · direct
1.1L1L2

By [L1], an abelian category satisfies the hypotheses of [L2].

2.1L2step 1.1∎

Therefore [L2] applies directly and yields all finite limits and all finite colimits.

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

A pullback is the kernel of the difference of the two legs, and dually for pushouts

Statement

Let f:A→C and g:B→C be morphisms in an abelian category. Then a pullback of the cospan A→fC←gB is a kernel of the difference map

f∘pA−g∘pB:A⊕B→C,

where pA and pB are the biproduct projections. Dually, a pushout of B←sA→tC is a cokernel of iB∘s−iC∘t:A→B⊕C.

Facts & Assumptions

Given: An abelian category and a cospan A→fC←gB.

[L1]

Abelian categories have finite limits and finite colimits (An abelian category has all finite limits and all finite colimits).

[L2]

On a biproduct the injections and projections satisfy the standard identity-sum relations (On a biproduct, the injections and projections satisfy the identity-sum relation).

[L3]

In a preadditive category, equalizers are kernels of differences (In a preadditive category, the equalizer of a parallel pair is the kernel of their difference).

[L4]

An abelian category is additive and therefore preadditive (Abelian category).

Proof

technique · direct
1.1L1L3L4

By [L1] there is a product of A and B, and by [L4] that product is the biproduct A⊕B. In the preadditive structure of [L4], a morphism x:X→A⊕B satisfies (fpA−gpB)x=0 exactly when fpAx=gpBx. So by [L3], a kernel of fpA−gpB is an equalizer of the parallel pair fpA,gpB.

2.1L2step 1.1

Giving x:X→A⊕B is the same as giving its two composites to A and B, and the equality in step 1.1 is exactly the pullback compatibility condition. Therefore the equalizer in step 1.1 is a pullback of f and g.

3.1L1L3L4step 2.1∎

Reversing all arrows gives the pushout statement: in an abelian category a pushout is the cokernel of the corresponding difference map.

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

The pullback of an epimorphism is an epimorphism

Statement

In a pullback square in an abelian category

PBAC¯®ef

if e is epic, then α is epic.

Facts & Assumptions

Given: The displayed pullback square in an abelian category, with e epic.

[L1]

The pullback is the kernel of the difference map on A⊕B (A pullback is the kernel of the difference of the two legs, and dually for pushouts).

[L3]

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

[L4]

In an abelian category every epic morphism 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.1L1L2

By [L1], there is a monomorphism k:P→A⊕B with α=pAk, β=pBk, and k the kernel of d:=fpA−epB. Since d iB=−e, the epicity of e implies that d is epic as well.

2.1L1L2L3L4step 1.1∎

Let q:A→Q be a cokernel of α. Because d is epic by step 1.1, [L4] says that d is a cokernel of its kernel k. Since qα=qpAk=0, the map qpA:A⊕B→Q kills k, so it factors through d as q‾ d=qpA. Composing with iB gives q‾(−e)=0, and since e is epic, q‾=0. Thus qpA=0, and composing with iA yields q=0. So α has zero cokernel and is epic by [L3].

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The pushout of a monomorphism is a monomorphism

Statement

In an abelian category, the pushout of a monomorphism is a monomorphism.

Facts & Assumptions

Given: An abelian category and a pushout square whose left leg is monic.

[L1]

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

[L2]

In an abelian category, pullbacks of epimorphisms are epimorphisms (The pullback of an epimorphism is an epimorphism).

Proof

technique · direct corollary
1.1L1

Passing to the opposite category turns the given pushout square into a pullback square, and the given monomorphism into an epimorphism. By [L1], the opposite category is still abelian.

2.1L1L2step 1.1∎

Apply [L2] in the opposite category. The opposite of the resulting epimorphism is exactly the pushout leg in the original square, so that leg is monic.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

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

Statement

In a pullback square in an abelian category

PBAC¯®gf

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

Facts & Assumptions

Given: The displayed pullback square in an abelian category.

[L1]

Abelian categories have pullbacks, and the square above is one (Abelian category, A pullback is the kernel of the difference of the two legs, and dually for pushouts).

Proof

technique · direct
1.1L1given

Let kβ:Kβ→P be a kernel of β and let kf:Kf→A be a kernel of f. Since gβkβ=fαkβ=0, the kernel property of kf gives a unique map u:Kβ→Kf with kfu=αkβ.

2.1step 1.1L1∎

Because fkf=0=g0, the pullback universal property gives a unique map s:Kf→P with αs=kf and βs=0. Since βs=0, the kernel property of kβ gives a unique map v:Kf→Kβ with kβv=s. Then kfuv=αkβv=αs=kf, so uv=1 by monicity of kf; similarly kβvu=s=kβ, so vu=1 by monicity of kβ. Thus u is an isomorphism.

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

A square with monic legs is a pullback exactly when it identifies the source with the intersection subobject

Statement

Consider a commutative square in an abelian category

XBCDmn

whose right and bottom legs are monomorphisms. Let I→D be the intersection of the subobjects represented by m and n. Then the square is a pullback if and only if the induced morphism X→I is an isomorphism.

Facts & Assumptions

Given: The displayed commutative square with monic right and bottom legs.

[L1]

In an abelian category, pullbacks of cospans exist and are computed by the construction of A pullback is the kernel of the difference of the two legs, and dually for pushouts.

Proof

technique · direct
1.1L1L2

By [L1], the pullback P→D of the two monics m and n exists. Because the square defining P is a common lower bound of [m] and [n], and every other common lower bound factors uniquely through that pullback, [L2] says that P→D represents their intersection subobject.

2.1L2step 1.1

If the displayed square is a pullback, then its source X→D is another representative of the same greatest lower bound from step 1.1. Therefore the induced morphism X→I is an isomorphism.

3.1step 1.1step 2.1∎

Conversely, if the induced map X→I is an isomorphism, then composing the pullback square representing I from step 1.1 with that isomorphism yields the displayed square. Pullbackness is invariant under replacing the corner object by an isomorphic one, so the displayed square is a pullback.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Pullback pasting in an abelian category

Statement

Pullback pasting and pullback cancellation hold in every abelian category.

Facts & Assumptions

Given: A diagram of two adjacent commutative squares in an abelian category.

[L1]

Pullback and pushout pasting hold in every category in which the relevant squares exist (Pullback and pushout pasting, with cancellation of the square adjacent to the outer edge).

Proof

technique · direct
1.1L1

An abelian category is still a category, and the statement only concerns pullback squares that already exist in that ambient category.

2.1L1step 1.1∎

Therefore the general theorem [L1] applies verbatim to the abelian setting.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Kernel and cokernel are mutually inverse order-preserving correspondences between subobjects and quotient objects

Statement

Fix an object A in an abelian category. Sending a subobject representative m:M→A to its cokernel class [coker⁡(m)], and sending a quotient representative q:A→Q to its kernel class [ker⁡(q)], defines mutually inverse order-preserving bijections between the subobjects of A and the quotient objects of A.

Facts & Assumptions

Given: An object A in an abelian category.

[L2]

Mutual factorization is the correct representative-independent equality relation on subobjects and quotient objects (Mutual factorisation is an equivalence relation on monomorphisms into an object and dually on epimorphisms out of it).

[L3]

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

Let m:M→A be monic, let cm:A→Qm be its cokernel, and let km:Km→A be the kernel of cm. Since cmm=0, the monomorphism m factors through km. Conversely, [L3] says that m is itself a kernel of cm, so km factors through m. Thus [km]=[m]. The dual argument shows that for every epic q one has [coker⁡(ker⁡q)]=[q].

1.2L1L3

If [m]≤[n], then m=nu for some u. Since coker⁡(n) n=0, one has coker⁡(n) m=0, so the cokernel universal property of m makes coker⁡(n) factor through coker⁡(m). By the quotient-order convention in [L1], this is exactly [coker⁡(m)]≤[coker⁡(n)]. The kernel assignment preserves the order dually.

2.1step 1.1step 1.2∎

Step 1.1 proves that the two assignments are mutually inverse on classes, and step 1.2 proves that both preserve the stated orders. So kernel and cokernel are mutually inverse order isomorphisms between subobjects and quotient objects.

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

The quotient of an object by a subobject

Definition

Let [m] be a subobject of an object A in an abelian category, represented by a monomorphism m:M→A. The quotient of A by [m] is the quotient object represented by the cokernel of m:

A/[m]:=coker⁡(m).

Because every monomorphism is the kernel of its cokernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel), this quotient is the object paired with the given subobject by the kernel-cokernel correspondence. The next item checks that the definition does not depend on the chosen representative of the class [m].

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The quotient by a subobject is independent of the chosen representing monomorphism

Statement

If two monomorphisms m:M→A and n:N→A represent the same subobject of A, then their cokernels are canonically isomorphic. Hence the notation A/B depends only on the subobject class [B→A].

Facts & Assumptions

Given: Two monomorphisms m:M→A and n:N→A representing the same subobject.

[L1]

The quotient by a subobject is defined as the cokernel of a representing monomorphism (The quotient of an object by a subobject).

[L3]

The cokernel assignment depends only on the subobject class and gives the inverse order-preserving correspondence to the kernel assignment (Kernel and cokernel are mutually inverse order-preserving correspondences between subobjects and quotient objects).

Proof

technique · direct
1.1L2L3

By [L2], the condition that m and n represent the same subobject is exactly [m]=[n]. Applying [L3] gives [coker⁡(m)]=[coker⁡(n)] as quotient-object classes.

2.1L1step 1.1∎

Equality of quotient-object classes means the two cokernels are joined by a unique compatible isomorphism. By [L1], that is exactly the claim that the quotient A/B is independent of the chosen representing monomorphism.

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

First isomorphism theorem in an abelian category

Statement

For every morphism f:A→B in an abelian category, there is a canonical isomorphism

A/ker⁡(f)  ≅  im⁡(f).

Facts & Assumptions

Given: An abelian category and a morphism f:A→B.

[L1]
[L2]

The coimage is the cokernel of the kernel, and the image is the kernel of the cokernel (Image and coimage in a category with kernels and cokernels).

[L3]

The canonical morphism coim⁡(f)→im⁡(f) exists (The canonical morphism from the coimage to the image exists and is unique).

[L4]

In an abelian category that canonical morphism is an isomorphism (Abelian category).

Proof

technique · direct
1.1L1L2

By [L1] and [L2], the quotient A/ker⁡(f) is exactly the coimage of f.

2.1L3L4step 1.1∎

The map from step 1.1 to im⁡(f) is the canonical coimage-to-image morphism of [L3], and [L4] makes it an isomorphism. Therefore A/ker⁡(f)≅im⁡(f) canonically.

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

Third isomorphism theorem in an abelian category

Statement

Let C≤B≤A be subobjects in an abelian category. Then there is a canonical isomorphism

(A/C)/(B/C)  ≅  A/B.

Facts & Assumptions

Given: Subobjects C≤B≤A represented by monomorphisms c:C→B and b:B→A.

[L2]

The first isomorphism theorem identifies a quotient by a kernel with the image (First isomorphism theorem in an abelian category).

[L3]

Every coequalizer, hence every cokernel, is epic (Every equalizer is a monomorphism, and every coequalizer is an epimorphism).

[L4]

Every monomorphism in an abelian category is a kernel of its cokernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

Proof

technique · direct
1.1L1

Let qC:A→A/C and qB:A→A/B be the quotient maps from [L1]. Since qBbc=0, the morphism qB kills C, so the universal property of qC gives a unique map q‾:A/C→A/B with q‾ qC=qB.

1.2givenL1L4

The composite bc is monic: equality bcu=bcv implies cu=cv and then u=v. By [L4], bc is therefore a kernel of its cokernel qC. If h:X→B satisfies qCbh=0, there is a unique t:X→C with bct=bh. Monicity of b gives ct=h, and monicity of c gives uniqueness. Since qCbc=0, this proves that c is a kernel of qCb.

2.1L1L2L3step 1.1step 1.2

Let p:B→B/C be the cokernel of c. By [L2], the canonical image factorization of qCb gives a monomorphism b~:B/C→A/C satisfying b~p=qCb. Since p is epic by [L3] and q‾b~p=qBb=0, we have q‾b~=0.

3.1L1L3step 1.1step 2.1∎

If r:A/C→Y satisfies rb~=0, then rqCb=rb~p=0. The cokernel property of qB gives a unique s:A/B→Y with sqB=rqC. Since qB=q‾qC and qC is epic, sq‾=r. Conversely, any s satisfying this last equality satisfies sqB=rqC, proving uniqueness. Thus q‾ is a cokernel of b~, and [L1] identifies (A/C)/(B/C) canonically with A/B.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The quotient by the kernel followed by the image inclusion is the canonical epi-mono factorization

Statement

For a morphism f:A→B in an abelian category, the factorization

A↠A/ker⁡(f)⟶∼im⁡(f)↣B

is the canonical epimorphism-monomorphism factorization of f.

Facts & Assumptions

Given: An abelian category and a morphism f:A→B.

[L1]

The first isomorphism theorem gives a canonical isomorphism A/ker⁡(f)≅im⁡(f) (First isomorphism theorem in an abelian category).

[L2]

Epic-monic factorizations exist and are unique up to unique isomorphism (Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism).

Proof

technique · direct
1.1L1

By [L1], there is an isomorphism ϕ:A/ker⁡(f)→im⁡(f) such that the composite of the quotient map q:A→A/ker⁡(f), the isomorphism ϕ, and the image inclusion if:im⁡(f)→B equals f.

2.1L2step 1.1∎

The quotient map q is epic and the image inclusion if is monic, so step 1.1 is an epic-monic factorization of f. By the uniqueness clause in [L2], it is the canonical one.

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

Exact functor between abelian categories

Definition

Let A and B be abelian categories. A functor F:A→B is exact when it is additive (Additive functor) and both left exact and right exact (Left exact and right exact functors).

Thus exactness is a two-sided preservation condition: F preserves the finite limits and finite colimits that exist in its source, and it preserves the additive structure carried by the hom-sets.

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

A left or right exact functor between abelian categories is automatically additive

Statement

Let F:A→B be a functor between abelian categories. If F is left exact or right exact, then F is additive.

Facts & Assumptions

Given: A functor F:A→B between abelian categories.

[L1]

Left exact means preserving finite limits, and right exact means preserving finite colimits (Left exact and right exact functors).

[L2]

Abelian categories are additive (Abelian category).

[L3]

A functor between additive categories is additive exactly when it preserves finite biproducts (A functor between additive categories is additive exactly when it preserves finite biproducts).

Proof

technique · direct
1.1L1L2L3

If F is left exact, then by [L1] it preserves the zero object and binary products. In an additive category, products are biproducts by [L2], so F preserves finite biproducts.

1.2L1L2L3

If F is right exact, then by [L1] it preserves the zero object and binary coproducts. Again [L2] identifies those with finite biproducts, so F preserves finite biproducts.

2.1L3step 1.1step 1.2∎

In either case, [L3] applies and shows that F is additive.

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

Left exactness, right exactness, and exactness are characterized by short exact sequences

Statement

Let F:A→B be a functor between abelian categories.

  1. F is left exact if and only if for every short exact sequence 0→A′→A→A′′→0 in A, the sequence 0→F(A′)→F(A)→F(A′′) is exact.
  2. F is right exact if and only if for every short exact sequence 0→A′→A→A′′→0 in A, the sequence F(A′)→F(A)→F(A′′)→0 is exact.
  3. F is exact if and only if it carries every short exact sequence in A to a short exact sequence in B.

Facts & Assumptions

Given: A functor F:A→B between abelian categories.

[L1]

Left exactness or right exactness already forces additivity (A left or right exact functor between abelian categories is automatically additive).

[L2]

A functor between additive categories is additive exactly when it preserves finite biproducts (A functor between additive categories is additive exactly when it preserves finite biproducts).

[L3]

An additive functor is left exact exactly when it preserves kernels (An additive functor is left exact exactly when it preserves kernels).

[L4]

Abelian categories remain abelian after passing to the opposite (The opposite of an abelian category is abelian).

[L5]

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

Proof

technique · direct
1.1L1L3L4

If F is left exact, then [L1] makes it additive, and [L3] says that it preserves kernels. Therefore whenever 0→K→kA→cQ→0 is short exact, the map F(k) is a kernel of F(c), which is exactly the left-exact short-sequence criterion. The right-exact half is the dual statement applied in opposite categories using [L4].

1.2L2L3L4L5

Conversely, assume F carries every short exact sequence to one exact through the middle. Applying that to the two split short exact sequences 0→A→A⊕B→B→0 and 0→B→A⊕B→A→0 shows that F(A⊕B) is a biproduct of F(A) and F(B), so F preserves finite biproducts and is additive by [L2]. Now every kernel k:K→A fits into a short exact sequence 0→K→A→A/K→0 by [L5], so the hypothesis makes F(k) a kernel. Then [L3] gives left exactness. The right-exact converse is the dual argument in opposite categories using [L4].

2.1step 1.1step 1.2∎

Clause 3 is exactly the conjunction of the first two clauses: a short exact sequence stays short exact precisely when the transformed sequence is both left exact and right exact.

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

An additive functor is exact exactly when it preserves kernels and cokernels

Statement

Let F:A→B be an additive functor between abelian categories. Then F is exact if and only if it preserves kernels and cokernels.

Facts & Assumptions

Given: An additive functor F:A→B between abelian categories.

[L1]

An additive functor between additive categories is left exact exactly when it preserves kernels (An additive functor is left exact exactly when it preserves kernels).

[L2]

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

[L3]

Exact means additive, left exact, and right exact (Exact functor between abelian categories).

Proof

technique · direct
1.1L1L2L3

If F is exact, then [L3] says it is left exact and right exact. The left-exact half and [L1] show that F preserves kernels. Applying the same argument to Fop:Aop→Bop and using [L2] shows that F preserves cokernels as well.

2.1L1L2L3∎

Conversely, assume F preserves kernels and cokernels. By [L1], kernel preservation makes F left exact. Passing to opposites and using [L2], cokernel preservation makes F right exact. Since F is additive by hypothesis, [L3] shows that F is exact.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

A left exact functor preserves monomorphisms and a right exact functor preserves epimorphisms

Statement

A left exact functor between abelian categories preserves monomorphisms, and a right exact functor preserves epimorphisms.

Facts & Assumptions

Given: A functor between abelian categories.

[L1]

One-sided exactness is characterized by the corresponding short exact sequence test (Left exactness, right exactness, and exactness are characterized by short exact sequences).

[L2]

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

Proof

technique · direct
1.1L1L2

If f:A→B is monic, then [L2] says 0→A→fB is left exact. A left exact functor carries this to another left exact sequence by [L1], so F(f) again has zero kernel. By [L2], F(f) is monic.

2.1L1L2∎

The epimorphism claim is dual: if f is epic, then [L2] says A→fB→0 is right exact, and a right exact functor carries it to a right exact sequence. Hence the cokernel of F(f) is zero, so [L2] makes F(f) epic.

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

An equivalence between abelian categories is exact

Statement

Every equivalence between abelian categories is exact.

Facts & Assumptions

Given: An equivalence F:A→B between abelian categories.

[L2]

Abelian categories are additive (Abelian category).

[L3]

A functor between additive categories is additive exactly when it preserves finite biproducts (A functor between additive categories is additive exactly when it preserves finite biproducts).

[L4]

Exact means additive, left exact, and right exact (Left exact and right exact functors, Exact functor between abelian categories).

Proof

technique · direct
1.1L1L4

By [L1], the functor F preserves finite limits and finite colimits. So by [L4] it is left exact and right exact. In particular it preserves finite products and finite coproducts.

2.1L2L3L4step 1.1∎

Since the source and target are additive by [L2], those finite products and coproducts are finite biproducts. Therefore step 1.1 lets [L3] conclude that F is additive. Together with step 1.1, that is exactly the definition of exactness in [L4].

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

Abelian subcategory and exact embedding

Definition

Let B be a full subcategory of an abelian category A. The subcategory B is an abelian subcategory when for every morphism of B its kernel and cokernel computed in A again lie in B, and when B is closed under finite biproducts in A.

An exact embedding is a full embedding (Embedding and full embedding of categories) whose essential image is an abelian subcategory and whose underlying functor is additive (Additive functor).

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

Abelian groups form an abelian category

Statement

The category Ab of abelian groups and homomorphisms is an abelian category.

Facts & Assumptions

Given: The category Ab of abelian groups.

[L1]

Abelian groups and Z-modules have the same objects and morphisms (Abelian groups and Z-modules have the same objects and morphisms).

[L3]

For a module homomorphism, the kernel, image, and cokernel are the usual submodule and quotient constructions (Module homomorphism and isomorphism, kernel, image and cokernel).

[L4]

The first isomorphism theorem for modules identifies M/ker⁡f with im⁡(f) (First isomorphism theorem for modules: M/ker⁡f≅im⁡f).

Proof

technique · direct
1.1L1L2

By [L1], Ab is the same category as Z-Mod. The hom-sets are therefore abelian groups under pointwise addition, and by [L2] finite products and coproducts exist and are the usual direct sums. So Ab is additive.

2.1L1L3L4∎

Again by [L1], kernels and cokernels in Ab are the module kernels and cokernels from [L3]. The coimage of a homomorphism is G/ker⁡f, its image is the usual image subgroup, and [L4] identifies them canonically. Hence the AB1 and AB2 clauses of Abelian category hold, so Ab is abelian.

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

Modules over a ring form an abelian category

Statement

For every ring R, the category R-Mod of left R-modules is an abelian category.

Facts & Assumptions

Given: A ring R.

[L2]

The category R-Mod is complete and cocomplete (For every ring R, the category R-Mod is complete and cocomplete).

[L3]

Module kernels, images, and cokernels are the usual ones (Module homomorphism and isomorphism, kernel, image and cokernel).

[L4]

The first isomorphism theorem for modules identifies the coimage with the image (First isomorphism theorem for modules: M/ker⁡f≅im⁡f).

Proof

technique · direct
1.1L1L2

The hom-set of module homomorphisms is an abelian group under pointwise addition, and [L2] gives finite products and coproducts, namely the usual direct sums. So R-Mod is additive.

2.1L3L4∎

Every module homomorphism has the kernel and cokernel from [L3], and [L4] identifies M/ker⁡f with im⁡(f). Thus R-Mod satisfies the defining AB1 and AB2 clauses of Abelian category, so it is abelian.

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

Additive functors from a small preadditive category to an abelian category form an abelian category

Statement

If C is a small preadditive category and A is abelian, then the category of additive functors C→A and natural transformations is abelian.

Facts & Assumptions

Given: A small preadditive category C and an abelian category A.

[L1]

Additive functors and natural transformations form a preadditive category (Additive functors and natural transformations form a preadditive category).

[L2]

The smallness of C makes the relevant functor categories locally small (If C is small and D is locally small then [C,D] is locally small; if both are small it is small).

[L4]

Abelian categories are additive and have pointwise kernels, cokernels, and coimage-image isomorphisms (Abelian category).

Proof

technique · direct
1.1L1L3L4

By [L1], the additive functors already form a preadditive category. The zero functor is additive, and binary biproducts are computed pointwise because [L4] gives biproducts in A and [L3] computes them pointwise. So the additive functor category is additive.

2.1L2L3L4step 1.1∎

Let η:F⇒G be a natural transformation. By [L3], its kernel and cokernel in the ambient functor category are computed pointwise, and the pointwise constructions lie in A. Because C is preadditive and F,G are additive, the induced structure maps on those pointwise kernels and cokernels are again additive by uniqueness in the kernel and cokernel universal properties. The canonical coimage-to-image map is likewise computed pointwise and is an isomorphism at each object by [L4]. Therefore the additive functor category satisfies the axioms of an abelian category.

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

A small product of abelian categories is abelian

Statement

Every set-indexed product of abelian categories is abelian. In particular, the empty product category is abelian.

Facts & Assumptions

Given: A set-indexed family (Ai)i∈I of abelian categories.

[L1]

A small product of preadditive categories is preadditive (A small product of preadditive categories is preadditive).

[L2]

Abelian categories are additive and compute kernels, cokernels, and coimage-image comparison maps internally (Abelian category).

Proof

technique · direct
1.1L1L2

By [L1], the product category ∏i∈IAi is preadditive. If I=∅, this product has one object and one morphism, which is simultaneously zero and identity, so it is already an abelian zero category. For nonempty I, the zero object, finite biproducts, kernels, cokernels, and canonical coimage-image maps are all computed coordinatewise from the corresponding structures in each factor from [L2].

2.1L2step 1.1∎

Therefore the product category is additive and satisfies the AB1 and AB2 clauses coordinatewise. So every small product of abelian categories is abelian.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

An abelian category that is a preorder is trivial

Statement

If an abelian category is a preorder, then every object is isomorphic to the zero object. In particular it is equivalent to the terminal one-object category.

Facts & Assumptions

Given: An abelian category A that is also a preorder.

[L1]

In a preorder there is at most one morphism between any two fixed objects (Preorder and monotone map).

[L2]

Abelian categories have a zero object and are balanced (Abelian category, An abelian category is balanced).

Proof

technique · direct corollary
1.1L1

By [L1], any two parallel morphisms in A are automatically equal. So every morphism is monic and epic.

2.1L2step 1.1∎

Let 0 be the zero object from [L2]. The unique morphisms X→0 and 0→X are both monic and epic by step 1.1, hence isomorphisms by [L2]. Therefore every object is isomorphic to 0, and the category is equivalent to the terminal one-object category.

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

The library does not use Freyd-Mitchell to prove the diagram lemmas

Freyd-Mitchell is not the proof device for this library's later diagram lemmas. It applies only to small abelian categories, it is not proved in this batch, and it would make the later exactness pages depend on a metatheorem rather than on the intrinsic abelian arguments built from pullbacks, pushouts, images, and cokernels.

That trade is the wrong one for the library. The member calculus and the diagram-lemma pages stay internal to an arbitrary abelian category, with no smallness side condition and no appeal to an ambient module category.

5 · Examples, counterexamples and false statements

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

An exact functor need not be faithful

Statement refuted

Every exact functor between abelian categories is faithful.

Facts & Assumptions

Given: Two nonzero abelian categories A and B, and an object Y of B with 1Y≠0Y,Y.

[L1]

A finite product of preadditive categories is preadditive (A small product of preadditive categories is preadditive).

[L2]

Abelian categories are additive and have kernels, cokernels, and coimage-image isomorphisms (Abelian category).

[L3]

Exact means additive, left exact, and right exact (Exact functor between abelian categories).

Counterexample

1.1L1L2L3

The product category A×B is preadditive by [L1], and its zero object, kernels, cokernels, finite biproducts, and canonical coimage-image maps are all computed componentwise from the corresponding structures in the two factors. Since both factors satisfy [L2], the product does too. The projection π1:A×B→A preserves those componentwise constructions, so it is exact in the sense of [L3].

2.1givenstep 1.1∎

The endomorphism (0,1Y):(0,Y)→(0,Y) is nonzero in A×B, but π1(0,1Y)=0. So π1 is not faithful. Therefore the refuted claim is false.

CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Filtered vector spaces can be additive with kernels and cokernels without being abelian

Statement refuted

Every additive category with all kernels and cokernels is abelian.

Facts & Assumptions

Given: A field k.

[L1]

An abelian category is in particular additive and requires the canonical coimage-to-image map to be an isomorphism (Additive category, Abelian category).

Counterexample

1.1L1

Let Fk be the category whose objects are Z-filtered k-vector spaces (V,F∙V) and whose morphisms preserve the filtrations. Pointwise addition on linear maps and direct sums with Fi(V⊕W)=FiV⊕FiW make Fk additive, and kernels and cokernels are computed on the underlying linear map with the induced and quotient filtrations.

2.1L1step 1.1∎

Take V=W=k with FiV=k for i<0 and FiV=0 for i≥0, while FiW=k for i≤0 and FiW=0 for i>0. The identity linear map ι:V→W preserves filtrations, has zero kernel and zero cokernel, so coim⁡(ι)=V and im⁡(ι)=W. But ι is not an isomorphism in Fk, because its inverse does not preserve F0. Hence the canonical map coim⁡(ι)→im⁡(ι) is not an isomorphism, so Fk is not abelian.

CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Torsion-free abelian groups do not form an abelian category

Statement refuted

The full subcategory of torsion-free abelian groups is an abelian category.

Facts & Assumptions

Given: The full subcategory Abtf of torsion-free abelian groups.

[L2]

Abelian categories are balanced (An abelian category is balanced).

Counterexample

1.1L1

In Abtf, multiplication by 2 on Z is monic and epic. Indeed, if 2u=2v for maps into or out of a torsion-free group T, then 2(u(x)−v(x))=0 for every x, so torsion-freeness forces u=v.

2.1L2step 1.1∎

The map 2:Z→Z is not an isomorphism in Abtf, because its inverse would have to send 1 to 1/2, which is not an integer. If Abtf were abelian, [L2] would force every bimorphism to be an isomorphism. So the subcategory is not abelian.

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

FALSE: every additive category with all kernels and cokernels is abelian

Statement

Every additive category with all kernels and cokernels is abelian.

Facts & Assumptions

[L1]

The filtered-vector-space example is additive and has all kernels and cokernels, but it is not abelian (Filtered vector spaces can be additive with kernels and cokernels without being abelian).

Refutation

1.1L1

The cited category satisfies the hypothesis of the statement: it is additive and has kernels and cokernels.

2.1L1step 1.1∎

But [L1] also says that category is not abelian. Therefore the universal statement is false.

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

FALSE: if coimage and image happen to be isomorphic as objects, then the canonical map is automatically an isomorphism

Statement

If the coimage and image of a morphism are isomorphic as objects, then the canonical map from the coimage to the image is automatically an isomorphism.

Facts & Assumptions

Given: The torsion-free abelian-group subcategory and the morphism 2:Z→Z.

[L1]

The torsion-free abelian-group subcategory is not abelian (Torsion-free abelian groups do not form an abelian category).

[L2]

Every morphism with kernels and cokernels has a canonical map from its coimage to its image (The canonical morphism from the coimage to the image exists and is unique).

[L3]

The cokernel of 0→A is A, and dually the kernel of A→0 is A (The cokernel of the zero map out of the zero object is the target, and dually for kernels).

Refutation

1.1L1L3

In the torsion-free abelian-group subcategory, the morphism 2:Z→Z has zero kernel. Its cokernel in that subcategory is also zero, because any homomorphism out of Z that kills the even subgroup must send 1 to torsion and hence to 0. Therefore [L3] identifies both coim⁡(2) and im⁡(2) with Z.

2.1L2step 1.1∎

The canonical map of [L2] is still the morphism 2:Z→Z, which is not an isomorphism. So isomorphism of the endpoint objects does not force the canonical comparison map itself to be invertible.

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

FALSE: in an abelian category a morphism can be monic and epic without being an isomorphism

Statement

In an abelian category, a morphism can be monic and epic without being an isomorphism.

Facts & Assumptions

Given: An abelian category.

[L1]

Abelian categories are balanced (An abelian category is balanced).

Refutation

1.1L1

The statement asserts the existence of a bimorphism in an abelian category that is not an isomorphism.

2.1L1step 1.1∎

But [L1] says every bimorphism in an abelian category is an isomorphism. So the asserted witness cannot exist, and the statement is false.

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

FALSE: every abelian category is equivalent to a module category

Statement

Every abelian category is equivalent to a category of modules.

Facts & Assumptions

Given: A field F and the full subcategory FinVectF of finite-dimensional F-vector spaces.

[L1]

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

[L2]

Every module category has all small coproducts (For every ring R, the category R-Mod is complete and cocomplete).

Refutation

1.1L1

The category FinVectF is abelian: kernels, cokernels, images, coimages, and finite direct sums of linear maps between finite-dimensional vector spaces stay finite-dimensional, so the abelian-category structure of VectF restricts to this full subcategory.

2.1L2step 1.1∎

The countable coproduct of countably many copies of the one-dimensional space F does not exist in FinVectF, because its usual direct sum is infinite-dimensional. But [L2] says every module category has all small coproducts. Since equivalences preserve which small coproducts exist, FinVectF cannot be equivalent to any module category. Therefore the universal statement is false.

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

FALSE: pullbacks preserve epimorphisms in every category with pullbacks

Statement

In every category with pullbacks, the pullback of an epimorphism is again an epimorphism.

Facts & Assumptions

Given: The full subcategory of Hausdorff spaces and continuous maps.

[L1]
[L3]

The rationals are dense in R, and the irrationals are nonempty (Both Q and R∖Q are dense in R, and every nonempty open subset of R is uncountable).

Refutation

1.1L1L2L3

Let i:QR↪R be the inclusion of the rationals into the real line, regarded as Hausdorff spaces. By [L3], QR is dense in R, so [L2] says that i is epic: any two continuous maps out of R into a Hausdorff space that agree on QR are equal.

2.1L1L2L3step 1.1∎

Choose an irrational point x∈R using [L3], and let j:{x}↪R be the inclusion. The pullback of i along j is the map ∅→{x}, because {x}∩QR=∅. Let D={0,1} with the discrete topology, which is Hausdorff by [L1]. The two constant maps {x}→D are distinct, but their composites with ∅→{x} are equal. So the pullback map is not epic, and the universal statement is false.

Sources