CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-28

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.

Abelian groups do not satisfy AB5*

Statement refuted

The abelian category $A b$ satisfies AB5*.

Facts & Assumptions

Given: The abelian group $A = \prod_{n \geq 1} Z$ , the tail subgroups $T_{n} = {(a_{k}) : a_{1} = \dots = a_{n} = 0}$ , and the direct sum $B = ⨁_{n \geq 1} Z \leq A$ .

[L1]

AB5* is the decreasing-family identity $(⋀_{i} B_{i}) \lor C = ⋀_{i} (B_{i} \lor C)$ (The axioms AB5 and AB5*).

Counterexample

1.1givenalgebra

The family $(T_{n})$ is decreasing, and $⋂_{n \geq 1} T_{n} = 0$ because a sequence whose every coordinate eventually vanishes from the front has all coordinates zero. Also $B \neq A$ , since the constant sequence $(1, 1, 1, \dots)$ lies in $A$ but not in the direct sum $B$ .

2.1L1step 1.1∎

For every $n$ , the subgroup $T_{n} + B$ is all of $A$ : given $a = (a_{k})_{k \geq 1} \in A$ , 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 $b \in B$ and $t \in T_{n}$ . Hence $(⋂_{n \geq 1} T_{n}) + B = B \neq A = ⋂_{n \geq 1} (T_{n} + B) .$ So the AB5* identity [L1] fails in $A b$ .

Depends on

The axioms AB5 and AB5*

Used by

The opposite of abelian groups does not satisfy AB5 Counterexample

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Charles A. Weibel, An Introduction to Homological Algebra, Appendix A.4 (standard reference, not scraped)