Alphabeta Math
Session-authored (Fable 5 assisted)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

36 results · all verified · 17 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 19 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Subobject Lattices Generators and the Grothendieck Axioms

1 · Prerequisites

2 · Summary

This page is where the abelian-category block starts behaving like homological algebra rather than like category-theoretic infrastructure. Subobjects become a modular lattice, quotient calculus turns that lattice into the second isomorphism theorem and the butterfly/Jordan-Holder spine, and generators turn size questions from MA-2 into concrete hypotheses one can actually verify.

The Grothendieck axioms are stated here in their primitive lattice form, on purpose. Exact filtered colimits and their duals are later reformulations, not the starting point. The page also keeps the projective/injective interface as lean as possible: enough projectives for module categories is established now, while the deeper enough-injectives theorem for general Grothendieck categories is left to later work.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Modular lattice

Definition

A lattice L (Lattices, distributive lattices, and order ideals) is modular when for every x,y,zL with xz one has

x(yz)=(xy)z.

The hypothesis xz is part of the law. Without it, the displayed identity need not hold.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The join of two subobjects in an abelian category

Definition

Let b:BA and c:CA represent two subobjects of an object A in an abelian category. Because finite biproducts exist (An abelian category has all finite limits and all finite colimits), there is a unique morphism

[b,c]:BCA

whose composites with the two biproduct injections are b and c.

The join of the two subobjects is the subobject of A represented by the image inclusion of [b,c] in the sense of Image and coimage in a category with kernels and cokernels. It is denoted

BC.

The well-definedness obligation on representatives is discharged by The join of two subobjects is their least upper bound .

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The join of two subobjects is their least upper bound

Statement

Let B and C be subobjects of an object A in an abelian category. Then the subobject BC of The join of two subobjects in an abelian category is the least upper bound of B and C in the subobject order of A.

Facts & Assumptions

Given: Monomorphisms b:BA and c:CA representing the two subobjects.

[L1]

The join BC is the image of the induced map [b,c]:BCA (The join of two subobjects in an abelian category).

[L2]

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

[L3]

A subobject inequality is exactly factorization of representatives (Subobjects and quotient objects form oppositely oriented partially ordered collections).

Proof

technique · direct
1.1

Let j:JA be the image inclusion of [b,c]. Since [b,c]ιB=b and [b,c]ιC=c for the biproduct injections, the factorization of [b,c] through j makes both b and c factor through j. Thus BJ and CJ, so J is an upper bound of the two subobjects.

L1L2L3
1.2

Let n:NA be any common upper bound. Then b=nu and c=nv for suitable u:BN and v:CN. By the universal property of BC, the induced map satisfies [b,c]=n[u,v]. Now [L2] says that the image inclusion j factors through every monomorphism through which [b,c] factors, so JN.

L2L3construct
2.1

Step 1.1 gives that J is an upper bound, and step 1.2 gives that it lies below every upper bound. By [L3], this is exactly the least-upper-bound claim.

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

The meet of two subobjects is their pullback

Statement

Let B and C be subobjects of an object A in an abelian category, represented by monomorphisms b:BA and c:CA. Then the meet BC in the subobject order is represented by the pullback of b and c.

Facts & Assumptions

Given: Monomorphisms b:BA and c:CA.

[L1]

Pullbacks are defined by their commutative square and universal property (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L3]

Subobject inequalities are factorization relations between representatives (Subobjects and quotient objects form oppositely oriented partially ordered collections).

Proof

technique · direct
1.1

Form a pullback square tikzcd P \arrow[r, "q"] \arrow[d, "p"'] & C \arrow[d, "c"] \\ B \arrow[r, "b"'] & A. By [L2], the pullback leg p is monic, so the composite m:=bp=cq:PA is monic as well. Because m factors through both b and c, it is a lower bound of the two subobjects.

L1L2L3
1.2

Let n:NA be any lower bound. Then n=bu=cv for some u:NB and v:NC. By the pullback universal property [L1], there is a unique w:NP with pw=u and qw=v. Therefore mw=bu=n, so n factors through m. Hence nm.

L1L3construct
2.1

Steps 1.1 and 1.2 show that m is a lower bound above every other lower bound. By [L3], the pullback subobject is exactly BC.

L3step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The subobjects of an object in an abelian category form a lattice

Statement

For every object A of an abelian category, the subobjects of A form a bounded lattice. The meet is pullback, the join is the image construction of The join of two subobjects in an abelian category, the bottom element is the zero subobject, and the top element is 1A.

Facts & Assumptions

Given: An object A in an abelian category.

[L1]

Any two subobjects of A admit a least upper bound (The join of two subobjects is their least upper bound).

[L2]

Any two subobjects of A admit a greatest lower bound (The meet of two subobjects is their pullback).

[L3]

Subobjects are mutual-factorization classes of monomorphisms into A (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms).

[L4]

An abelian category has a zero object, hence zero morphisms (Abelian category).

Proof

technique · direct
1.1

By [L1] and [L2], every pair of subobjects of A has a join and a meet. That gives the binary lattice operations.

L1L2
1.2

By [L4], the unique map 0A exists. It is monic because every two maps into 0 are equal, so by [L3] it represents a subobject of A. Every monomorphism into A factors through 1A, and 0A factors through every monomorphism into A, so these classes are respectively the top and bottom elements.

L3L4algebra
2.1

Steps 1.1 and 1.2 prove that the subobjects of A form a bounded lattice.

step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The subobject lattice of an abelian category is modular

Statement

For every object A in an abelian category, the lattice of subobjects of A is modular.

Facts & Assumptions

Given: An object A in an abelian category.

[L1]

A modular lattice is one satisfying xzx(yz)=(xy)z (Modular lattice).

[L3]

Quotienting by the kernel identifies a morphism with its image (First isomorphism theorem in an abelian category).

[L4]

Quotienting nested subobjects satisfies the third isomorphism theorem (Third isomorphism theorem in an abelian category).

[L5]

In an abelian category, a morphism that is both monic and epic is an isomorphism (An abelian category is balanced).

[L6]

The join of two subobjects is the image of the induced map from their biproduct (The join of two subobjects in an abelian category).

[L7]

The meet of two subobjects is represented by their pullback (The meet of two subobjects is their pullback).

Proof

technique · direct
1.1

Consider any lattice in which comparable complements of a fixed element coincide in every interval. Let XZ and put U:=X(YZ),V:=(XY)Z. Then UV by monotonicity.

construct
1.2

Fix an interval [B1,B2] of subobjects of A, and write Q:=B2/B1 with quotient map q:B2Q. If D is any intermediate subobject, let qD:B2B2/D be its quotient map. Because B1D, the composite qD kills B1, so it factors through q as a map qD:QB2/D. Define Φ(D) to be the kernel subobject of qD.

L4construct
2.1

Both U and V are complements of Y in the interval [YZ,XY]: one has UY=XY=VY, and YZUZ gives UY=YZ, while VZ and YXY give VY=YZ. By step 1.1, the interval hypothesis forces U=V. Therefore the modular-law identity of [L1] holds.

L1step 1.1algebra
2.2

Conversely, if SQ with quotient map tS:QQ/S, define Ψ(S) to be the kernel subobject of tSq in B2. Then B1Ψ(S)B2. If D lies in the interval, the equality qD=qDq gives Ψ(Φ(D))=D. If SQ, the morphism tSq is epic, so its image is all of Q/S; by [L3], B2/Ψ(S)Q/S. Under this identification, qΨ(S) is a cokernel of S, so Φ(Ψ(S))=S. Thus Φ and Ψ are inverse bijections between [B1,B2] and the subobject lattice of Q.

L3L4step 1.2construct
3.1

If DE in the interval, then qE factors through qD, so qE kills Φ(D). Hence Φ(D)Φ(E). The same argument applied to Ψ shows that Φ is an order isomorphism from [B1,B2] onto Sub(Q).

step 1.2step 2.2
4.1

By step 3.1, it is enough to prove the comparable-complements property in Sub(Q). Let EQ, and let UV be two complements of E. Write t:QQ/E for the quotient map.

construct
5.1

Because UE=0, the pullback description [L7] makes the kernel of the restricted map tU:UQ/E trivial. Because UE=Q, the canonical map [iU,iE]:UEQ has image Q by [L6], so composing with t shows that tU is epic. By [L5], tU is an isomorphism. The same argument shows that tV is an isomorphism. Let i:UV represent the comparison UV. Then tU=(tV)i, so i is an isomorphism. Therefore U and V represent the same subobject of Q.

L5L6L7step 4.1construct
6.1

Step 5.1 proves that every interval in the subobject lattice has the comparable-complements property, and step 2.1 shows that this property implies the modular law of [L1]. With [L2], this proves that the subobject lattice of A is modular.

L1L2step 2.1step 3.1step 5.1
RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The published subgroup modular law is the instance

The subgroup modular law already published as Dedekind's modular law for subgroup products is the concrete group-theoretic instance of the categorical modularity theorem. Item The subobject lattice of an abelian category is modular is the abstract statement: in Ab its subobjects are subgroups, and the modular-law identity becomes exactly Dedekind's law.

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

Second isomorphism theorem in an abelian category

Statement

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

(BC)/C    B/(BC).

Facts & Assumptions

Given: Subobjects b:BA and c:CA.

[L1]

The join BC is the image of the induced map [b,c]:BCA (The join of two subobjects in an abelian category).

[L2]

The meet BC is represented by the pullback of b and c (The meet of two subobjects is their pullback).

[L3]

A morphism modulo its kernel is canonically isomorphic to its image (First isomorphism theorem in an abelian category).

Proof

technique · direct
1.1

Let q:AA/C be the quotient map. Consider the composite qb:BA/C. By [L2], a morphism into B is killed by qb exactly when its composite into A factors through C, which is exactly the pullback condition defining BC. So ker(qb)=BC.

L2construct
2.1

By [L3], step 1.1 gives a canonical isomorphism B/(BC)im(qb). The map q kills C, so its restriction to the join BC factors through the quotient (BC)/C. Conversely, every summand used in the defining map [b,c] lands in im(qb) after composing with q, because the C-summand dies. Hence im(qb) is exactly the image of BC in A/C, namely (BC)/C.

L1L3step 1.1
3.1

Combining steps 1.1 and 2.1 yields the canonical isomorphism (BC)/CB/(BC).

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

Direct and inverse image of a subobject

Definition

Let f:AA be a morphism in an abelian category.

If b:BA represents a subobject of A, its direct image along f is the subobject of A represented by the image inclusion of the composite

BAfA.

It is denoted fB.

If c:CA represents a subobject of A, its inverse image along f is the subobject of A represented by the pullback of c along f (Pullbacks and pushouts as limits and colimits of cospans and spans). It is denoted fC.

The representative-independence of these assignments is discharged by Direct and inverse image of subobjects form a Galois connection .

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

Direct and inverse image of subobjects form a Galois connection

Statement

Let f:AA be a morphism in an abelian category. Then the direct-image map

f:Sub(A)Sub(A)

and the inverse-image map

f:Sub(A)Sub(A)

form a Galois connection:

fBCBfC.

Facts & Assumptions

Given: A morphism f:AA and subobjects BA, CA.

[L1]

Direct image and inverse image are defined by image factorization and pullback respectively (Direct and inverse image of a subobject).

[L2]

A Galois connection between preorders is exactly a pair of monotone maps satisfying the displayed biconditional (Galois connection between preorders).

[L3]

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

Proof

technique · direct
1.1

Assume fBC. By [L1], the composite BAfA factors through the subobject CA. The pullback defining fC therefore gives a factorization of B through fC, so BfC.

L1construct
1.2

Assume BfC. Composing with the pullback leg fCC shows that the composite BA factors through C. By [L3], the image fB is the least subobject of A with that property, so fBC.

L1L3
2.1

Steps 1.1 and 1.2 prove the displayed biconditional, which is exactly the Galois-connection condition of [L2].

L2step 1.1step 1.2
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Inverse image preserves meets and direct image preserves joins

Statement

Let f:AA be a morphism in an abelian category. Then for subobjects C1,C2A and B1,B2A one has

f(C1C2)=fC1fC2,f(B1B2)=fB1fB2.

Facts & Assumptions

Given: A morphism f:AA and the displayed subobjects.

[L1]

The subobject maps f and f form a Galois connection (Direct and inverse image of subobjects form a Galois connection).

[L2]

Subobjects form lattices, so meets and joins are characterized by their order universal properties (The subobjects of an object in an abelian category form a lattice).

Proof

technique · direct
1.1

For any subobject BA, Bf(C1C2)    fBC1C2    fBC1 and fBC2    BfC1 and BfC2. By [L2], this says that f(C1C2) is the meet of fC1 and fC2.

L1L2algebra
1.2

For any subobject CA, f(B1B2)C    B1B2fC    B1fC and B2fC    fB1C and fB2C. Again [L2] identifies this with the universal property of the join fB1fB2.

L1L2algebra
2.1

Steps 1.1 and 1.2 are exactly the two displayed identities.

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

Kernel and image are the inverse and direct images along a morphism

Statement

Let f:AA be a morphism in an abelian category.

  1. The inverse image of the zero subobject of A along f is ker(f).
  2. The direct image of the identity subobject of A along f is im(f).

Facts & Assumptions

Given: A morphism f:AA.

[L1]

Inverse image is defined by pullback and direct image by ordinary image factorization (Direct and inverse image of a subobject).

[L2]

A subobject is represented by a monomorphism; in particular 0A and 1A:AA represent the zero and total subobjects (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms).

[L3]

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

Proof

technique · direct
1.1

Pulling back the zero subobject 0A along f produces exactly the kernel square of f, so by [L1] and [L2] the inverse image f(0) is ker(f).

L1L2
1.2

The direct image of the identity subobject 1A is, by [L1], the image of the composite A1AAfA, which is just the image of f in the sense of [L3].

L1L2L3
2.1

Therefore kernels and images are exactly inverse and direct images along the morphism f.

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

Simple object

Definition

An object S of an abelian category is simple when S0 and its only subobjects are the zero subobject and 1S (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms).

Equivalently, S has no proper nonzero subobject.

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

Composition series and composition factors of an object

Definition

A composition series of an object A in an abelian category is a finite strict chain of subobjects

0=A0  <  A1  <    <  An=A

such that every quotient object Ai/Ai1 is simple (Simple object, The quotient of an object by a subobject).

The simple quotient objects Ai/Ai1 are the composition factors of the series.

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

Zassenhaus butterfly lemma in an abelian category

Statement

Let A0A1 and B0B1 be subobjects of an object X in an abelian category. Then there is a canonical isomorphism

A0(A1B1)A0(A1B0)    (A1B1)B0(A0B1)B0.

Facts & Assumptions

Given: Subobjects A0A1 and B0B1 of an object X.

[L1]

The subobject lattice of X is modular (The subobject lattice of an abelian category is modular).

[L2]

For subobjects U,V of a common object, one has (UV)/VU/(UV) (Second isomorphism theorem in an abelian category).

[L3]

Nested quotients satisfy the third isomorphism theorem (Third isomorphism theorem in an abelian category).

Proof

technique · direct
1.1

Put M:=A1B1, U:=A1B0, and V:=A0B1. Since UM, the second isomorphism theorem [L2] applied to A0 and M inside A0M gives A0MA0UMM(A0U). By modularity [L1] inside the interval below M, M(A0U)=(MA0)U=VU. So the left quotient is canonically isomorphic to M/(VU).

L1L2construct
1.2

Similarly, since VM, the second isomorphism theorem [L2] applied to M and B0 inside MB0 gives MB0VB0MM(VB0). Again modularity yields M(VB0)=V(MB0)=VU. So the right quotient is also canonically isomorphic to M/(VU).

L1L2construct
2.1

The two quotients in steps 1.1 and 1.2 are canonically isomorphic to the same quotient of M, hence to each other. The nested-quotient compatibility of [L3] identifies these isomorphisms with the displayed butterfly quotient comparison.

L3step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Schreier refinement theorem in an abelian category

Statement

Let

0=A0A1Am=X,0=B0B1Bn=X

be finite chains of subobjects in an abelian category. Then they admit refinements whose successive quotient objects can be paired up up to isomorphism.

Facts & Assumptions

Given: The two finite subobject chains displayed in the statement.

[F1]

A refinement is obtained by inserting intermediate subobjects, and two finite chains are equivalent when their nonzero successive quotient objects can be paired up up to isomorphism.

[L1]

Each cell in the refinement grid is governed by the butterfly lemma (Zassenhaus butterfly lemma in an abelian category).

Proof

technique · direct
1.1

For 0i<m and 0jn, define Ai,j:=Ai(Ai+1Bj). Then Ai,0=Ai and Ai,n=Ai+1, while Ai,jAi,j+1 for every j. Concatenating the chains Ai=Ai,0Ai,1Ai,n=Ai+1 over i=0,,m1 gives a refinement of the A-chain. Define Bj,i:=Bj(Bj+1Ai) symmetrically; concatenating those chains refines the B-chain.

F1construct
2.1

For every cell (i,j), apply [L1] to the pairs AiAi+1 and BjBj+1. It gives a canonical isomorphism Ai,j+1Ai,jBj,i+1Bj,i. So the successive quotients of the two refinements are paired by the same grid.

L1step 1.1
3.1

Some adjacent terms may coincide, producing zero successive quotients. By [F1], deleting those repetitions leaves equivalent refinements, and the quotient pairing from step 2.1 survives on every nonzero factor. Hence the original two chains admit equivalent refinements.

F1step 2.1
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Jordan-Holder theorem in an abelian category

Statement

If an object A in an abelian category has two composition series, then the two series have the same length and the same composition factors up to permutation and isomorphism.

Facts & Assumptions

Given: Two composition series of the same object A.

[L1]

A composition series is a finite strict subobject chain with simple successive quotients (Composition series and composition factors of an object, Simple object).

[L2]

Any two finite subobject chains admit equivalent refinements (Schreier refinement theorem in an abelian category).

Proof

technique · direct
1.1

By [L2], the two composition series admit equivalent refinements.

givenL2
1.2

A composition series has no proper refinement. Indeed, if Ai1<K<Ai, then the quotient map AiAi/Ai1 carries K to a nonzero proper subobject of the simple object Ai/Ai1, contradicting [L1]. So any refinement of a composition series differs from it only by repeated adjacent terms.

L1algebra
2.1

Delete repeated adjacent terms from the equivalent refinements of step 1.1. By step 1.2 this recovers the original two composition series, and the quotient pairing survives. Therefore the original series have the same number of factors, and a permutation matches their factors up to isomorphism.

step 1.1step 1.2
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Object of finite length

Definition

An object A of an abelian category has finite length when it admits a composition series in the sense of Composition series and composition factors of an object.

Its length (A) is the number of successive simple factors in any composition series. The Jordan-Hölder theorem Jordan-Holder theorem in an abelian category makes this number independent of the chosen series.

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

Length is additive along a subobject

Statement

Let BA be a subobject in an abelian category. If any two of the objects A, B, and A/B have finite length, then so does the third, and whenever all three do one has

(A)=(B)+(A/B).

Facts & Assumptions

Given: A subobject BA.

[L1]

Finite length means admitting a composition series, and length is the common number of factors in such a series (Object of finite length).

[L2]

Jordan-Hölder makes the factor count independent of the chosen composition series (Jordan-Holder theorem in an abelian category).

[L3]

The second isomorphism theorem identifies the factors that arise from pulling a chain across a quotient or intersecting with a subobject (Second isomorphism theorem in an abelian category).

Proof

technique · direct
1.1

Assume B and A/B have finite length. Choose composition series 0=B0<<Br=B,0=C0<<Cs=A/B. Let q:AA/B be the quotient map and put Dj:=q1(Cj). Then B=D0<D1<<Ds=A, and [L3] identifies each quotient Dj/Dj1 with Cj/Cj1. So 0=B0<<Br=D0<D1<<Ds=A is a composition series of A. Therefore A has finite length and (A)=r+s=(B)+(A/B).

L1L3chooseconstruct
1.2

Assume now that A has finite length, with composition series 0=A0<A1<<An=A. Intersecting with B gives an increasing chain 0=A0BA1BAnB=B, and quotienting by B gives an increasing chain in A/B. By [L3], each successive factor in either chain is a subquotient of a simple factor Ai/Ai1, hence is either 0 or simple. Deleting repeated adjacent terms therefore yields composition series of B and of A/B.

L1L3construct
2.1

Step 1.1 proves the extension direction and the displayed additive formula. Step 1.2 proves that finite length passes to subobjects and quotients. The number in the formula is independent of the chosen composition series by [L2].

L2step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Objects of finite length form an abelian subcategory

Statement

In an abelian category, the full subcategory whose objects have finite length is an abelian subcategory.

Facts & Assumptions

Given: An abelian category A.

[L1]

Finite length is the property defined in Object of finite length.

[L2]

Finite length is stable under passing to subobjects and quotients, and is additive across a subobject (Length is additive along a subobject).

[L3]

A full subcategory is abelian precisely when it is closed under kernels, cokernels, and finite biproducts computed in the ambient abelian category (Abelian subcategory and exact embedding).

Proof

technique · direct
1.1

Let f:XY be a morphism between finite-length objects. Since ker(f)X and im(f)Y, [L2] makes both ker(f) and im(f) finite length. The quotient Y/im(f) is then finite length by [L2], so the cokernel of f is finite length as well.

L1L2construct
1.2

If X and Y have finite length, then the inclusion XXY has quotient Y. Applying [L2] to that inclusion shows that XY has finite length. So the finite-length objects are closed under finite biproducts.

L2construct
2.1

Steps 1.1 and 1.2 are exactly the kernel, cokernel, and finite-biproduct closures required by [L3]. Therefore the full subcategory of finite-length objects is an abelian subcategory.

L3step 1.1step 1.2
RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The published abelian-group composition-series development is the instance

When restricted to abelian groups, the published group-theory items The Zassenhaus butterfly lemma, The Schreier refinement theorem, The Jordan–Hölder theorem for groups, and Composition series, composition factors, and composition length are the special cases of the categorical results on this page when the ambient abelian category is Ab and subobjects are subgroups. For arbitrary nonabelian groups the comparison does not apply: Grp is not an abelian category, normality is a genuine extra condition, and nonabelian simple factors lie outside Ab. The present page therefore abstracts precisely the abelian-group restriction, not the full published group theorems.

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

Generator and cogenerator of a category

Definition

An object G of a category C is a generator when the singleton set {G} is separating in the sense of Separating and coseparating sets of objects.

Dually, an object Q is a cogenerator when {Q} is coseparating.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The axioms AB3 and AB3*

Definition

An abelian category satisfies AB3 when it has all small coproducts, and it satisfies AB3* when it has all small products (Finite, small, and large limits and colimits; complete and cocomplete categories).

Because an abelian category already has cokernels and kernels, the criterion A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers identifies AB3 with cocompleteness and AB3* with completeness inside the abelian setting.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The cancellation and epimorphism descriptions of a generator agree

Statement

Let A be a locally small abelian category satisfying AB3, and let G be an object of A. Then the following are equivalent:

  1. G is a generator.
  2. The representable functor A(G,) is faithful.
  3. For every object A, the canonical morphism uA(G,A)GA is an epimorphism.

Facts & Assumptions

Given: A locally small abelian category A satisfying AB3 and an object G.

[L1]

A generator is exactly a one-object separating set (Generator and cogenerator of a category).

[L2]

AB3 supplies the small coproducts indexed by hom-sets (The axioms AB3 and AB3*).

[L3]

In a locally small category, a separating set is equivalently a jointly faithful family of representables (In a locally small category, separating and coseparating sets are equivalently jointly faithful families of representables).

Proof

technique · direct
1.1

By [L1] and [L3], condition 1 is equivalent to condition 2: the singleton {G} is separating exactly when the one-member family A(G,) is faithful.

L1L3
1.2

Assume condition 2, and fix an object A. By [L2], form the canonical map eA:uA(G,A)GA whose u-th coproduct injection is sent to u. Let q:AQ be its cokernel. If q0, faithfulness of A(G,) gives some u:GA with qu0. But u is one of the coproduct components of eA, so qu=0 because qeA=0, a contradiction. Hence q=0, and therefore eA is epic. So condition 2 implies condition 3.

L2L3construct
2.1

Assume condition 3. If f,g:XY are distinct, then h:=fg0. Apply condition 3 to X: if hu=0 for every u:GX, then heX=0, and since eX is epic that would force h=0. So some u:GX satisfies hu0, equivalently fugu. Thus G separates maps, hence is a generator by [L1]. Therefore condition 3 implies condition 1.

L1step 1.2algebra
3.1

Steps 1.1, 1.2, and 2.1 prove the equivalence of the three descriptions.

step 1.1step 1.2step 2.1
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

An AB3 locally small abelian category with a generator is well-powered

Statement

Every locally small abelian category satisfying AB3 and having a generator is well-powered.

Facts & Assumptions

Given: A locally small abelian category A satisfying AB3 and a generator G.

[L1]

In AB3, the canonical coproduct map from copies of a generator onto an object is epic (The cancellation and epimorphism descriptions of a generator agree).

[L2]

Well-powered means that each object admits a set of monomorphisms representing all of its subobject classes (Well-powered and co-well-powered categories, and supplied well-powerings).

[L3]

A generator is an object in the sense of Generator and cogenerator of a category.

Proof

technique · direct
1.1

Fix an object A. For each subobject m:BA, let SmA(G,A) be the subset of those maps u:GA that factor through m. Because A is locally small, A(G,A) is a set, so its power set P(A(G,A)) is a set as well.

L3construct
2.1

For each subset SA(G,A), use AB3 and [L1] to form the canonical map eS:uSGA and let iS:ISA be its image. If m:BA is any subobject, then [L1] applied to B gives an epic canonical map vA(G,B)GB. Composing with m produces exactly the family of maps in Sm, so the image of the resulting composite is m. Hence iSm represents the same subobject as m.

L1step 1.1construct
3.1

The set of monomorphisms {iS:ISASA(G,A)} therefore contains a representative of every subobject class of A. By [L2], A is well-powered.

L2step 2.1
RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Generator, separator, and the three inequivalent-looking definitions

The library defined a separating set on the adjoint-functor page and uses generator here for the one-object version. Grothendieck and the Stacks Project phrase the notion by canonical epimorphisms from coproducts of copies of the object, while Freyd phrases it by faithfulness of A(G,). Item The cancellation and epimorphism descriptions of a generator agree shows that these are equivalent in the cocomplete abelian setting; the three definitions are not the same sentence, which is why the page records the terminology rather than silently treating one as notation for another.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A cocomplete locally small abelian category with a generator supplies the category-side SAFT hypotheses dually

Statement

Let A be a cocomplete locally small abelian category with a generator. Then A is well-powered and co-well-powered. In the opposite category Aop, the object G is coseparating. If a supplied well-powering of A is given, taking cokernels supplies a co-well-powering of A, equivalently a supplied well-powering of Aop. Thus Aop supplies the category-side data in the supplied-well-powering branch of the objectwise special adjoint functor theorem. The target-category and continuity hypotheses remain hypotheses on the particular functor to which that theorem is applied.

Facts & Assumptions

Given: A cocomplete locally small abelian category A with a generator G.

[L2]

The supplied-well-powering branch of objectwise SAFT requires a complete locally small domain with a supplied small coseparating set and a supplied well-powering; the target must be locally small and the functor must preserve all small limits. (Special adjoint functor theorem, objectwise form with explicit intersection smallness or preservation data)

[L3]

In an abelian category, subobjects and quotient objects correspond by kernel and cokernel (Kernel and cokernel are mutually inverse order-preserving correspondences between subobjects and quotient objects).

[L4]

A generator is a separating object (Generator and cogenerator of a category).

[L5]

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

Proof

technique · direct
1.1

By [L1], every object of A has a set of representative monomorphisms for its subobject classes. By [L3], taking cokernels transfers these to representative epimorphisms for all quotient-object classes. Thus A is both well-powered and co-well-powered.

L1L3
1.2

By [L5], Aop is abelian, and cocompleteness of A becomes completeness of Aop. Local smallness is unchanged. The separating property of G from [L4] becomes the coseparating property in the opposite category.

L4L5algebra
2.1

A supplied well-powering of A gives a supplied family of representative monomorphisms. Applying cokernels objectwise using [L3] gives a supplied co-well-powering of A, which is a supplied well-powering of Aop. Hence the domain-side hypotheses in branch 1 of [L2] hold for Aop.

L2L3step 1.1step 1.2construct
3.1

Therefore the category supplies exactly the stated dual SAFT data. As [L2] requires, any application must still provide a locally small target and a functor preserving all small limits; those are not consequences of the present category-level hypotheses.

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

A generator detects comparison of subobjects

Statement

Let G be a generator of an abelian category, and let B,CA be subobjects. Then

BCevery morphism GA factoring through B also factors through C.

Facts & Assumptions

Given: A generator G and subobjects B,CA, represented by monomorphisms b:BA and c:CA.

[L1]

A generator separates distinct morphisms by precomposition (Generator and cogenerator of a category).

[L2]

The meet BC is represented by the pullback of b and c (The meet of two subobjects is their pullback).

[L3]

In an abelian category, a morphism that is both monic and epic is an isomorphism (An abelian category is balanced).

[L4]

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

[L5]

Abelian categories have cokernels (Abelian category).

Proof

technique · direct
1.1

If BC, then any map GA factoring through B also factors through C by composition.

givenalgebra
1.2

To prove the converse, assume BC. By [L2], let p:PB be the pullback subobject of b and c. If p were epic, then [L3] would make it an isomorphism, forcing b to factor through c. So p is not epic.

L2L3contrapositive-reduce
2.1

Let q:BQ be a cokernel of p, which exists by [L5]. Since p is not epic, [L4] implies q0.

L4L5step 1.2
3.1

The morphisms q and 0B,Q are therefore distinct, so [L1] gives some u:GB with qu0. If bu factored through c, the pullback property in [L2] would force u to factor through p, hence qu=0, impossible. Thus bu:GA factors through B but not through C.

L1L2step 2.1construct
4.1

Step 1.1 proves the forward implication, and steps 1.2, 2.1, and 3.1 prove the contrapositive of the reverse implication. Therefore BC exactly when every morphism GA factoring through B also factors through C.

step 1.1step 1.2step 2.1step 3.1discharge-contrapositive: reverse implication
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The axioms AB4 and AB4*

Definition

An abelian category satisfies AB4 when it satisfies AB3 and every small coproduct of monomorphisms is again a monomorphism.

Dually, it satisfies AB4* when it satisfies AB3* and every small product of epimorphisms is again an epimorphism.

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

The axioms AB5 and AB5*

Definition

First fix the small-family operations used below. In an AB3 abelian category, the join of a small family (BiA)iI is the image of the induced morphism

iIBiA.

In an AB3* abelian category, let qi:AA/Bi be the quotient maps (The quotient of an object by a subobject). The meet of the family is the kernel of the induced morphism

AiIA/Bi.

These constructions have the claimed order properties. Indeed, each component BiA factors through the image of iBiA, while any common upper bound receives the coproduct map; image minimality (The image is the least subobject through which a morphism factors) therefore makes that image the least upper bound. Dually, the displayed kernel lies in every Bi because BiA is the kernel of qi (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel), and every common lower bound is killed by every qi, hence by the product map, so it factors through the displayed kernel. Thus that kernel is the greatest lower bound. For a two-member family these constructions agree with the binary operations of The subobjects of an object in an abelian category form a lattice. The empty join is 0 and the empty meet is A.

An abelian category satisfies AB5 when it satisfies AB3 and for every small directed family of subobjects (Bi) of an object A and every subobject CA one has

(iBi)C=i(BiC).

It satisfies AB5* when it satisfies AB3* and for every small decreasing family of subobjects (Bi) of an object A and every subobject CA one has

(iBi)C=i(BiC).

The joins and meets in these formulas are the small-family constructions above.

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

AB5 implies AB4

Statement

Every abelian category satisfying AB5 also satisfies AB4.

Facts & Assumptions

Given: An abelian category satisfying AB5.

[L1]

AB5 is the directed-join distributivity law together with AB3 (The axioms AB5 and AB5*).

[L2]

AB4 is the assertion that small coproducts of monomorphisms are monic (The axioms AB4 and AB4*).

Proof

technique · direct
1.1

Let (mi:BiAi)iI be a small family of monomorphisms, and let m:iIBiiIAi be the induced coproduct map, which exists by the AB3 part of [L1]. Let k:KiBi be its kernel. For each finite subset FI, let SFiBi be the finite partial sum of the summands with indices in F. Because finite coproducts in an abelian category are biproducts, the restriction of m to SF is a finite direct sum of monomorphisms and is therefore monic. Hence KSF=0 for every finite F.

L1construct
2.1

The family (SF) is directed and has join iBi. Applying the AB5 identity [L1] with the fixed subobject K gives K=(FSF)K=F(SFK)=0. So the kernel of m is zero, and therefore m is monic. By [L2], this is exactly AB4.

L1L2step 1.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Grothendieck category

Definition

A Grothendieck category is an abelian category that satisfies AB5 and has a generator (The axioms AB5 and AB5*, Generator and cogenerator of a category).

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

Module categories are Grothendieck categories

Statement

For every ring R, the category R-Mod of left R-modules is a Grothendieck category.

Facts & Assumptions

Given: A ring R.

[L1]

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

[L2]

In an AB3 category, an object is a generator exactly when the canonical coproduct map from its copies onto every object is epic (The cancellation and epimorphism descriptions of a generator agree).

[L3]

Equality in filtered colimits of sets is eventually witnessed at one common stage (Two representatives in a filtered colimit of sets are equal exactly when they become equal at one common later stage).

[F1]

For a left R-module M, every module map RM is determined by the image of 1, and every element mM defines such a map by rrm.

Proof

technique · direct
1.1

By [L1], the category R-Mod has all small coproducts, so it satisfies AB3. For any left R-module M, the bijection [F1] identifies the canonical coproduct uHomR(R,M)R with a copy of R for each element of M, and the canonical map to M sends the basis vector indexed by m to m. It is therefore surjective, hence epic. By [L2], R is a generator.

L1L2F1
1.2

Let (Bi) be a directed family of submodules of a module A, and let CA. The join iBi is the union iBi, because directedness makes finite sums of elements land in one later stage. Thus every element of (iBi)C already lies in some BiC, and the reverse inclusion is immediate. So (iBi)C=i(BiC). This is exactly AB5. The eventual-equality principle [L3] is the set-level form behind the same filtered-colimit exactness statement.

L3algebra
2.1

Step 1.1 gives a generator and step 1.2 gives AB5. Therefore R-Mod is a Grothendieck category by Grothendieck category.

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

Assuming the Axiom of Choice, abelian groups satisfy AB4*

Statement

Assume the Axiom of Choice. Then the abelian category Ab satisfies AB4*.

Facts & Assumptions

Given: The Axiom of Choice and a small family of epimorphisms of abelian groups ei:AiBi.

[L1]

AB4* means that small products of epimorphisms remain epimorphic (The axioms AB4 and AB4*).

[L2]

The Axiom of Choice gives a choice function for every family of nonempty sets (The Axiom of Choice).

[F1]

In Ab, epimorphisms are exactly surjective homomorphisms.

Proof

technique · direct
1.1

Let b=(bi)iBi. By [F1], each ei is surjective, so every fibre ei1(bi) is nonempty. By [L2], choose aiAi with ei(ai)=bi for every index i. Then a=(ai)iAi satisfies (iei)(a)=b. So iei is surjective, hence epic in Ab.

L2F1construct
2.1

This is exactly the AB4* condition of [L1]. Therefore, assuming the Axiom of Choice, Ab satisfies AB4*.

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

A nonzero abelian category cannot satisfy both AB5 and AB5*

Statement

If an abelian category satisfies both AB5 and AB5*, then it is the zero category. Equivalently, no nonzero abelian category satisfies both axioms.

Facts & Assumptions

Given: An abelian category A satisfying both AB5 and AB5*.

[L1]

AB5 and AB5* are the directed-join and decreasing-meet distributivity laws of The axioms AB5 and AB5*.

[L2]

An abelian category has zero objects, kernels, cokernels, and finite biproducts (Abelian category).

Proof

technique · direct
1.1

Suppose X is a nonzero object. Let S:=n0X and P:=n0X, which exist by the AB3 and AB3* parts of [L1]. Let s:SP be the canonical map. For each n, let TnP be the tail subobject knX. Then (Tn) is decreasing, nTn=0 because the product projections jointly detect morphisms, and Tnim(s)=P because the finite head XnS together with the tail generates all of P. Applying AB5* to the family (Tn) and the subobject im(s) gives im(s)=P.

L1L2chooseconstruct
2.1

For each n, let SnS be the finite partial sum Xn. The family (Sn) is directed and has join S. Transport the product diagonal δ:XP across the isomorphism SP from step 1.1, and let DS be its image. The diagonal is monic because each product projection composed with it is 1X, so D0. But for every n one has DSn=0: a map factoring through both D and Sn has zero (n+1)-st coproduct projection because it factors through Sn, while through D that same projection is the factor map itself, so the map is zero.

step 1.1L2construct
3.1

Applying AB5 to the directed family (Sn) and the fixed subobject D gives D=(nSn)D=n(SnD)=0, contradicting step 2.1. Therefore no nonzero object X exists, so A is the zero category.

L1step 2.1contradiction: nonzero object
4.1

Step 3.1 proves that satisfying both AB5 and AB5* forces the category to be zero, which is the contrapositive form of the theorem's second sentence.

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

Projective object

Definition

An object P of an abelian category is projective when for every epimorphism q:EM and every morphism f:PM, there exists a morphism f~:PE with

qf~=f.

The lift f~ need not be unique.

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

Projective object characterisations

Statement

For an object P of an abelian category, the following are equivalent:

  1. P is projective.
  2. For every short exact sequence 0KEM0, the induced sequence 0A(P,K)A(P,E)A(P,M)0 is exact.
  3. Every epimorphism EP splits.

Facts & Assumptions

Given: An object P in an abelian category.

[L1]

Projectivity is the lifting property against epimorphisms (Projective object).

[L2]

In an abelian category, the pullback of an epimorphism is an epimorphism (The pullback of an epimorphism is an epimorphism).

[F1]

For every short exact sequence, the functor A(P,) is left exact; projectivity is exactly the extra surjectivity at the right-hand end.

Proof

technique · direct
1.1

Assume P is projective. Then [L1] gives a lift of every map PM across every epimorphism EM, so the last map in condition 2 is surjective. Together with the left exactness in [F1], this proves condition 2.

L1F1assume-hyp
1.2

Condition 2 clearly implies condition 1, because surjectivity of A(P,E)A(P,M) for every short exact sequence is exactly the lifting property [L1].

L1assume-hyp
1.3

If P is projective and q:EP is epic, apply [L1] to 1P:PP. A lift s:PE with qs=1P is a section, so q splits.

L1assume-hyp
1.4

Assume condition 3. Given an epimorphism q:EM and a map f:PM, form the pullback of q along f. By [L2], its projection to P is epic, so condition 3 makes it split. Composing such a section with the other pullback leg gives a lift of f across q. Thus P is projective.

L2assume-hypconstruct
2.1

Steps 1.1 and 1.2 prove 12, and steps 1.3 and 1.4 prove 13. Hence all three conditions are equivalent.

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

Injective object

Definition

An object I of an abelian category is injective when for every monomorphism m:ME and every morphism f:MI, there exists a morphism f~:EI with

f~m=f.

The extension f~ need not be unique.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Injective object characterisations

Statement

For an object I of an abelian category, the following are equivalent:

  1. I is injective.
  2. For every short exact sequence 0KEM0, the induced sequence 0A(M,I)A(E,I)A(K,I)0 is exact.
  3. Every monomorphism IE splits.

Facts & Assumptions

Given: An object I in an abelian category.

[L1]

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

[L2]

Projective objects are characterized by exactness of Hom and by splitting of epimorphisms onto them (Projective object characterisations).

[L3]

Injectivity is the dual lifting property (Injective object).

Proof

technique · direct
1.1

By [L1], the opposite category Aop is abelian. In that opposite category, the object I is projective exactly when it is injective in A, because monomorphisms and epimorphisms are exchanged.

L1L3
2.1

Apply the projective characterization [L2] to I inside Aop. The exactness statement there becomes exactness of A(,I) on short exact sequences in A, and splitting of an epimorphism onto I in the opposite category is splitting of a monomorphism out of I in A.

L1L2step 1.1
3.1

Therefore conditions 1, 2, and 3 are equivalent in A.

L3step 2.1
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A coproduct of projectives is projective and a product of injectives is injective

Statement

Assume an abelian category satisfies AB3 and AB3*.

  1. Every finite coproduct of projective objects is projective, and every finite product of injective objects is injective.
  2. For an arbitrary small family, the same conclusion holds provided one may choose one lift or one extension for each index in each lifting problem; in particular it holds under the Axiom of Choice.

Facts & Assumptions

Given: An abelian category satisfying AB3 and AB3*, and small families (Pi) of projective objects and (Ii) of injective objects.

[L1]

AB3 and AB3* supply the required coproducts and products (The axioms AB3 and AB3*).

[L2]

Projective objects are characterized by the lifting property against epimorphisms, and injective objects dually by the extension property against monomorphisms (Projective object characterisations, Injective object characterisations).

Proof

technique · direct
1.1

By [L1], let P=iPi. Given an epimorphism q:EM and a morphism f:PM, write fi=fιi on the coproduct summands. Because each Pi is projective, [L2] gives a lift f~i:PiE of fi. For a finite family these lifts are chosen explicitly; for an arbitrary small family they are exactly the stated choice-dependent data. The coproduct universal property then assembles the f~i into a lift f~:PE, so P is projective.

L1L2chooseconstruct
1.2

The injective claim is dual. By [L1], let I=iIi. Given a monomorphism m:ME and a morphism f:MI, write fi=πif. Each injective object Ii admits an extension f~i:EIi by [L2]. The product universal property assembles them into f~:EI extending f. So I is injective.

L1L2chooseconstruct
2.1

Steps 1.1 and 1.2 prove the finite case without extra choice and the arbitrary small-family case with the stated choice boundary.

step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A direct summand of a projective is projective

Statement

Every direct summand of a projective object in an abelian category is projective.

Facts & Assumptions

Given: A projective object P with a decomposition PQQ.

[L1]

Projective objects are exactly those with the lifting property against epimorphisms (Projective object characterisations).

Proof

technique · direct
1.1

Let q:EM be epic and let f:QM be any morphism. Write i:QP and r:PQ for the split inclusion and retraction, so ri=1Q. The composite fr:PM lifts across q by [L1] to a map g~:PE.

L1construct
2.1

Put f~:=g~i:QE. Then qf~=qg~i=fri=f. So Q has the lifting property against every epimorphism, hence is projective by [L1].

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

A category with enough projectives and with enough injectives

Definition

An abelian category has enough projectives when every object A admits an epimorphism PA with P projective (Projective object).

It has enough injectives when every object A admits a monomorphism AI with I injective (Injective object).

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

Module categories have enough projectives

Statement

Assume the Axiom of Choice. For every ring R, the abelian category R-Mod has enough projectives.

Facts & Assumptions

Given: A ring R.

[L1]

Every left R-module is a quotient of a free left R-module (Every module is a quotient of a free module).

[L2]

Under the Axiom of Choice, free modules are projective (Equivalent characterizations of projective modules).

[L3]

Having enough projectives means admitting a projective epimorphism onto every object (A category with enough projectives and with enough injectives).

Proof

technique · direct
1.1

Let M be a left R-module. By [L1], the canonical free module R(M) admits a surjection R(M)M.

L1
2.1

Under the Axiom of Choice, [L2] makes R(M) projective. So M admits a projective epimorphism from step 1.1.

L2step 1.1
3.1

Since M was arbitrary, [L3] shows that R-Mod has enough projectives.

L3step 2.1
RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Module categories have enough injectives is already published

The module-specific injective theory is already published as Module categories have enough injectives and Baer's criterion for injective modules. The present page only records the general ambient definition A category with enough projectives and with enough injectives and does not claim the deeper theorem that every Grothendieck category has enough injectives.

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

A projective generator detects isomorphisms

Statement

Let P be a projective generator of an abelian category. If

A(P,f):A(P,A)A(P,B)

is an isomorphism for a morphism f:AB, then f is an isomorphism.

Facts & Assumptions

Given: A projective generator P and a morphism f:AB.

[L1]

Projectivity makes A(P,) exact on short exact sequences (Projective object characterisations).

[L2]

A generator is equivalently an object whose canonical coproduct maps are epic (The cancellation and epimorphism descriptions of a generator agree).

Proof

technique · direct
1.1

Apply [L1] to the short exact sequences 0ker(f)Aim(f)0 and 0im(f)Bcoker(f)0. Since A(P,f) is an isomorphism, the first sequence forces A(P,ker(f))=0 and the second forces A(P,coker(f))=0.

L1construct
2.1

Let X be any object with A(P,X)=0. By [L2], the canonical map uA(P,X)PX is epic. But the indexing set is empty, so this is the zero map 0X. An epic zero map forces X=0. Applying this to the objects in step 1.1 gives ker(f)=0=coker(f).

L2step 1.1
3.1

Therefore f is both monic and epic, hence an isomorphism in an abelian category.

step 2.1

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A subobject lattice of an abelian category need not be distributive

Statement refuted

Every subobject lattice of an object in an abelian category is distributive.

Facts & Assumptions

Given: The abelian group A=(Z/2)(Z/2).

[L1]

Subobject lattices in an abelian category are modular (The subobject lattice of an abelian category is modular).

[L2]

A lattice is distributive when meet distributes over join (Lattices, distributive lattices, and order ideals).

Counterexample

1.1

The nonzero proper subgroups of A are exactly the three one-dimensional subspaces L1=(1,0),L2=(0,1),L3=(1,1). For ij, the intersection LiLj is 0, and Li+Lj=A. So the subobject lattice of A is the diamond M3.

givenalgebra
2.1

Now L1(L2L3)=L1A=L1, while (L1L2)(L1L3)=00=0. Hence the distributive law of [L2] fails in this subobject lattice. By [L1], the example is modular but not distributive.

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

Abelian groups do not satisfy AB5*

Statement refuted

The abelian category Ab satisfies AB5*.

Facts & Assumptions

Given: The abelian group A=n1Z, the tail subgroups Tn={(ak):a1==an=0}, and the direct sum B=n1ZA.

[L1]

AB5* is the decreasing-family identity (iBi)C=i(BiC) (The axioms AB5 and AB5*).

Counterexample

1.1

The family (Tn) is decreasing, and n1Tn=0 because a sequence whose every coordinate eventually vanishes from the front has all coordinates zero. Also BA, since the constant sequence (1,1,1,) lies in A but not in the direct sum B.

givenalgebra
2.1

For every n, the subgroup Tn+B is all of A: given a=(ak)k1A, write a=b+t where b has the same first n coordinates as a and all later coordinates 0, while t has first n coordinates 0 and later coordinates equal to those of a. Then bB and tTn. Hence (n1Tn)+B=BA=n1(Tn+B). So the AB5* identity [L1] fails in Ab.

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

The opposite of abelian groups does not satisfy AB5

Statement refuted

The opposite category Abop satisfies AB5.

Facts & Assumptions

Given: The abelian category Ab.

[L1]

The category Ab does not satisfy AB5* (Abelian groups do not satisfy AB5*).

[L2]

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

Counterexample

1.1

By [L2], the opposite category Abop is again abelian. Passing to the opposite exchanges joins with meets and AB5 with AB5*.

L2algebra
2.1

If Abop satisfied AB5, then Ab would satisfy AB5*. This contradicts [L1]. Therefore Abop does not satisfy AB5.

L1step 1.1
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

FALSE: every subobject lattice in an abelian category is distributive

Statement

Every subobject lattice in an abelian category is distributive.

Facts & Assumptions

Given: The object (Z/2)(Z/2) in Ab.

[L1]

The subobject lattice of this object is a concrete modular but non-distributive diamond (A subobject lattice of an abelian category need not be distributive).

Refutation

1.1

The example [L1] exhibits an object of an abelian category whose subobject lattice is not distributive.

L1
2.1

Therefore the universal statement is false. In particular, modularity of subobject lattices does not imply distributivity.

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

FALSE: every abelian category has a generator

Statement

Every abelian category has a generator.

Facts & Assumptions

Given: The abelian category FinAb of finite abelian groups.

[L1]

A generator must separate distinct morphisms by precomposition (Generator and cogenerator of a category).

[L2]

An abelian category is a category with the usual additive exact structure (Abelian category).

Refutation

1.1

The category FinAb is abelian: kernels, cokernels, and finite biproducts of morphisms of finite abelian groups are again finite abelian groups. So [L2] applies to it.

L2algebra
2.1

Let G be any finite abelian group. Choose a prime p not dividing the exponent of G. Then every homomorphism GZ/p is zero. Hence the identity map and the zero map of Z/p cannot be separated by precomposition with any map from G, so G is not a generator by [L1]. Since G was arbitrary, FinAb has no generator.

L1step 1.1choose
3.1

Thus not every abelian category has a generator.

step 2.1
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

FALSE: every object of an abelian category has a composition series

Statement

Every object of an abelian category has a composition series.

Facts & Assumptions

Given: The abelian group Z.

[L1]

A composition series is a finite strict chain with simple successive quotients (Composition series and composition factors of an object).

[L2]

Finite-length objects are exactly those admitting composition series (Object of finite length).

Refutation

1.1

Every nonzero subgroup of Z is of the form nZ, hence is isomorphic to Z. So if a composition series 0=A0<<An=Z existed, the first nonzero term A1 would satisfy A1Z, and the first quotient A1/A0=A1 would not be simple. This contradicts [L1].

L1algebra
2.1

Therefore Z has no composition series, so by [L2] it is not of finite length. The universal statement is false even in Ab.

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

FALSE under the Axiom of Choice: AB4 implies AB5

Statement

Assume the Axiom of Choice. Then AB4 implies AB5.

Facts & Assumptions

Given: The Axiom of Choice and the opposite category Abop.

[A1]

The Axiom of Choice (The Axiom of Choice).

[L1]

The category Abop does not satisfy AB5 (The opposite of abelian groups does not satisfy AB5).

[L2]

AB4 is the coproduct-monomorphism axiom (The axioms AB4 and AB4*).

[L3]

Assuming the Axiom of Choice, Ab satisfies AB4* (Assuming the Axiom of Choice, abelian groups satisfy AB4*).

[L4]

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

Refutation

1.1

By [L4], the opposite category Abop is abelian. Passing to the opposite exchanges AB4 with AB4*, so [L3] implies that Abop satisfies AB4 in the sense of [L2].

L2L3L4algebra
2.1

But [L1] shows that Abop does not satisfy AB5. So, even under [A1], AB4 does not imply AB5.

A1L1step 1.1
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

FALSE: a generator is automatically projective

Statement

A generator is the same thing as a projective generator.

Facts & Assumptions

Given: The abelian group G=ZZ/p for a prime p.

[L1]

Generators are defined by separation of morphisms (Generator and cogenerator of a category).

[L2]

Direct summands of projectives are projective (A direct summand of a projective is projective).

[L3]

Projective objects are the lifting objects of Projective object.

Refutation

1.1

The summand Z is a generator of Ab, so G=ZZ/p is also a generator: precompose with the inclusion ZG and then use the generator property of Z.

L1algebra
2.1

If G were projective, then its direct summand Z/p would be projective by [L2]. But the quotient map ZZ/p does not split, so Z/p does not have the lifting property [L3]. Therefore G is a generator that is not projective.

L2L3step 1.1
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28 rests on unproved material (inherited)Open item page →
Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

FALSE: Jordan-Holder needs finiteness only of the ambient category

Statement

The Jordan-Holder theorem needs a finiteness hypothesis only on the ambient category, not on the object.

Facts & Assumptions

Given: The abelian category Ab and the objects Z/p and Z.

[L1]

Jordan-Holder compares composition series of a single object (Jordan-Holder theorem in an abelian category).

[L2]

Finite length is an objectwise condition (Object of finite length).

Refutation

1.1

The object Z/p has finite length, while by the previous false statement witness Z has no composition series and so is not of finite length. Both live in the same abelian category Ab.

L2algebra
2.1

Therefore the relevant finiteness hypothesis is on the object whose composition series are being compared, not on the category alone. That is exactly how [L1] and [L2] are stated, so the displayed statement is false.

L1L2step 1.1

Sources