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.

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

Projective and Injective Resolutions — Examples

1 · Prerequisites

2 · Summary

These examples compute the basic constructions from the companion A page in concrete module categories. They show what the standard cyclic-group resolution looks like, how comparison maps and homotopies are written down, how the direct-sum horseshoe behaves in a split extension, and why stable syzygy comparison is weaker than literal isomorphism.

The counterexamples also mark the exact places where the positive theorems stop: enough injectives need not come with enough projectives, and syzygies need not be canonically isomorphic.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01Open item page →

A projective resolution of a cyclic abelian group

Example

For n1, the cyclic abelian group Z/nZ admits the projective resolution 0ZnZZ/nZ0, where the right-hand map is the quotient modulo n.

Facts & Assumptions

Given: An integer n1.

[L1]

Free modules are projective with the recorded choice boundary (Free modules are projective, with the exact choice boundary).

Verification

technique · direct
1.1

The composite of multiplication by n with the quotient modulo n is zero. The kernel of ZZ/nZ is exactly nZ, which is the image of the left map, and the left map is injective. So the sequence is exact.

givenalgebra
2.1

Both copies of Z are free abelian groups of rank one and are therefore projective by [L1]. Hence the exact sequence of step 1.1 is a projective resolution of Z/nZ.

L1step 1.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01Open item page →

The canonical iterated free resolution of a module

Example

Take M=Z/2Z. The canonical free cover on its underlying set {0,1ˉ} is ε0:Ze0Ze1Z/2Z, with ε0(e0)=0 and ε0(e1)=1ˉ. Its kernel is generated by e0 and 2e1, so the next stage of the canonical construction is the free abelian group on that kernel as a set.

Facts & Assumptions

Given: The module M=Z/2Z.

[L1]

The iterated free-cover construction gives a canonical exact free resolution (The iterated free-module resolution is canonical in ZF).

Verification

technique · direct
1.1

A vector ae0+be1 maps to bˉ, so it lies in ker(ε0) exactly when b is even. Therefore ker(ε0)=Ze0Z(2e1).

givenalgebra
2.1

The next free object in the canonical construction is therefore F1=Z(ker(ε0)) together with its canonical surjection F1ker(ε0). This makes concrete what [L1] does: the construction simply repeats the free-on-the-underlying-set cover on the current kernel, with no arbitrary choices. The same pattern starts even for the zero module.

L1step 1.1discharge-construct
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01 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 injective resolution of an abelian group beginning with a divisible group

Example

Assume the Axiom of Choice through Baer's criterion.

For the abelian group Z, the sequence 0ZQQ/Z0 is an injective resolution. It begins with the standard embedding of Z into the divisible group Q.

Facts & Assumptions

Given: The abelian group Z.

[L1]

Every module admits an injective resolution (Every module admits an injective resolution).

[L2]

Every abelian group embeds in a divisible abelian group (Every abelian group embeds in a divisible abelian group).

[L3]

Over Z, injective modules are exactly divisible groups (Over a PID, injective modules are exactly divisible modules).

Verification

technique · direct
1.1

The inclusion ZQ is injective, its cokernel is Q/Z, and both Q and Q/Z are divisible. Therefore both are injective by [L3], and the displayed sequence is exact.

L3givenalgebra
2.1

Thus the sequence is already an injective resolution of Z. It starts with an embedding into the divisible group promised by [L2], and it is a concrete instance of the general existence statement [L1].

L1L2step 1.1
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

Comparison maps between two resolutions of a cyclic group

Example

Let P and Q be two displayed copies of the standard resolution 0ZnZZ/nZ0. For multiplication by m on Z/nZ, multiplication by m in degrees 0 and 1 gives a comparison map PQ.

Facts & Assumptions

Given: Integers n1 and m, and two copies of the standard resolution from A projective resolution of a cyclic abelian group.

[L1]

Projective comparison maps exist (Projective comparison maps exist).

Verification

technique · direct
1.1

Multiplication by m commutes with multiplication by n on Z, so the square with the two differentials commutes. It also commutes with the quotient maps to Z/nZ, because both routes send x to mx.

givenalgebra
2.1

Therefore the degreewise multiplication-by-m maps form an augmentation-preserving chain map between the two resolutions. This is the explicit comparison map whose existence is asserted abstractly in [L1].

L1step 1.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

An explicit comparison homotopy

Example

On two copies of the standard projective resolution 0ZnZZ/nZ0, the degreewise maps f0=f1=1 and g0=g1=1+n are two different comparison maps lifting the identity on Z/nZ. They are joined by the explicit chain homotopy s0=1:ZZ.

Facts & Assumptions

Given: An integer n1 and two copies of the standard resolution.

[L1]

Comparison maps lifting the same object morphism are homotopic (Projective comparison maps are unique up to chain homotopy).

Verification

technique · direct
1.1

Because 1+n1(modn) and (1+n)n=n(1+n), the degreewise maps fi=1 and gi=1+n are both augmentation-preserving chain maps lifting 1Z/nZ. They are distinct as maps on Z whenever n0.

givenalgebra
2.1

Let s0:ZZ be the identity map. Then g0f0=n=d1s0,g1f1=n=s0d1, so s0 is a chain homotopy from f to g. This is the explicit homotopy predicted by [L1].

L1step 1.1discharge-construct
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01 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 horseshoe resolution of an extension of cyclic groups

Example

For the split short exact sequence 0Z/mZZ/mZZ/nZZ/nZ0, the horseshoe resolution is the direct sum of the two standard cyclic-group resolutions: 0ZZ(a,b)(ma,nb)ZZZ/mZZ/nZ0.

Facts & Assumptions

Given: Integers m,n1.

[L1]

A split short exact sequence admits the direct-sum resolution (A split short exact sequence admits the direct-sum resolution).

[L2]

The standard cyclic-group resolution is the basic side resolution (A projective resolution of a cyclic abelian group).

Verification

technique · direct
1.1

Exactness is checked componentwise: the kernel of the quotient map onto Z/mZZ/nZ is mZnZ, which is exactly the image of the displayed differential, and that differential is injective.

givenalgebra
2.1

The resolution in step 1.1 is the direct sum of the two side resolutions from [L2], so [L1] identifies it as the horseshoe resolution for this split extension.

L1L2step 1.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01 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.

Schanuel's lemma for two presentations of a module

Example

For Z/2Z, compare the two short exact sequences 02ZZZ/2Z0 and 02ZZZZZ/2Z0, where the second surjection sends (a,b) to aˉ. Schanuel's lemma predicts 2Z(ZZ)(2ZZ)Z.

Facts & Assumptions

Given: The two displayed short exact sequences.

[L1]

Schanuel's lemma gives a stable isomorphism between the two kernels (Schanuel's lemma in an abelian category).

[L2]

Short exact sequences of modules are exact module-theoretic rows (Exact sequences and short exact sequences of modules).

Verification

technique · direct
1.1

The kernel of ZZ/2Z is 2Z, and the kernel of (a,b)aˉ is 2ZZ. Thus the two displayed rows are short exact in the sense of [L2].

L2givenalgebra
2.1

Since 2ZZ, both sides of Schanuel's conclusion are free abelian groups of rank three. Hence they are isomorphic, exactly as [L1] predicts.

L1step 1.1algebra
CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01 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.

Two projective resolutions with nonisomorphic first syzygies

Statement refuted

Two projective resolutions of the same object must have isomorphic first syzygies.

Facts & Assumptions

Given: The object Z/2Z.

[L1]

The standard cyclic-group resolution is projective (A projective resolution of a cyclic abelian group).

[L2]

First syzygies from two projective resolutions are only stably isomorphic in general (Syzygies from two projective resolutions are stably isomorphic).

Counterexample

1.1

The standard resolution 0Z2ZZ/2Z0 has first syzygy 2ZZ. The stabilized resolution 0ZZ(a,b)(2a,b)ZZZ/2Z0 is again projective and exact, and its first syzygy is 2ZZZZ.

L1algebra
2.1

The groups Z and ZZ are not isomorphic, so the first syzygies of these two projective resolutions are not isomorphic. This is why [L2] stops at stable isomorphism.

L2step 1.1
CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01 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 category with enough injectives but not enough projectives

Statement refuted

Enough injectives implies enough projectives.

Facts & Assumptions

Assume the Axiom of Choice through Baer's criterion.

Given: The category TorAb of torsion abelian groups.

[L1]

Modules over a ring form an abelian category (Modules over a ring form an abelian category).

[L2]

Over Z, injective modules are exactly divisible groups (Over a PID, injective modules are exactly divisible modules).

[L3]

Every abelian group embeds in a divisible group (Every abelian group embeds in a divisible abelian group).

Counterexample

1.1

Kernels, images, and cokernels of homomorphisms between torsion abelian groups are torsion again, so TorAb is an abelian full subcategory of the abelian category from [L1]. If A is torsion, [L3] embeds it into a divisible group D; the torsion subgroup t(D) is still divisible and still contains A. Hence [L2] makes t(D) injective, so TorAb has enough injectives.

L1L2L3construct
1.2

Suppose P were a nonzero projective torsion group. Let P×=P{0}, and for each xP× let nx be the order of x. Form G:=xP×Z/nxZ with generators ex, and define the surjection π:GP by π(ex)=x. Projectivity gives a section s:PG. Since s(P)0, some coordinate projection restricts to a nonzero map PZ/nxZ. Let H be its nonzero cyclic image, write H=d>1, and regard the resulting map u:PHZ/dZ as surjective.

givenconstruct
2.1

Choose xP with u(x)=1Z/dZ. For each n1, projectivity lifts u through the reduction Z/dnZZ/dZ to a map un:PZ/dnZ. The element un(x) is congruent to 1 modulo d, hence is relatively prime to d and has order dn. But the order of un(x) must divide the fixed finite order of x, impossible for arbitrarily large n.

step 1.2givenalgebra
3.1

Therefore TorAb has enough injectives but no nonzero projective objects, so it does not have enough projectives. This refutes the statement.

step 1.1step 2.1

Sources