CounterexampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

A projective generator need not be small

Statement refuted

False claim: every projective generator of a module category is small, in the sense that its representable functor preserves every set-indexed coproduct.

Assume the Axiom of Choice. Let $k$ be a field and let $P = k^{(N)} = ⨁_{n \in N} k$ be the free $k$ -module on a countably infinite set, identified with the direct sum of countably many copies of $k$ . Then $P$ is projective and a generator of $k -Mod$ , but it is not small: the identity ${id}_{P}$ is not in the image of the canonical comparison $⨁_{n \in N} {Hom}_{k} (P, k) ⟶ {Hom}_{k} (P, P),$ because every element of the source is a finite-support family of linear functionals and hence has image contained in a finite-dimensional subspace, whereas ${id}_{P}$ does not. Consequently $P$ is a projective generator for which ${Hom}_{k} (P, -)$ fails to preserve a set-indexed coproduct, so the smallness hypothesis in Small projective generators and progenerators cannot be weakened to "projective generator". The Axiom of Choice is used exactly to make the infinite free module $P$ projective; the example is not choice-free.

Facts & Assumptions

Assume the Axiom of Choice.

Given: A field $k$ and the direct sum $P = k^{(N)} = ⨁_{n \in N} k$ over the index set $N$ , with standard basis vectors $e_{n} = ȷ_{n} (1_{k})$ and coordinate maps $π_{n} : P \to k$ , $x \mapsto x_{n}$ .

[F1]

Under AC every free module is projective, and a lift of a map out of a free module through a surjection is obtained by choosing one preimage of each basis value, so an infinite basis set is where AC is used (Free modules are projective, with the exact choice boundary, The Axiom of Choice, Projective modules and the lifting property).

[F2]

Every element of the direct sum $⨁_{n} k$ has finite support, the coordinate maps satisfy $π_{n} ȷ_{m} = δ_{m n}$ and $x = \sum_{n} ȷ_{n} (π_{n} (x))$ for every $x$ , and a family of $k$ -linear maps $f_{n} : k \to Y$ extends uniquely to a $k$ -linear map $⨁_{n} k \to Y$ with components $f_{n}$ (The direct sum of an indexed family of modules, Universal property of a direct sum of modules).

[F3]

${Hom}_{k} (P, k)$ and ${Hom}_{k} (P, P)$ are abelian groups under pointwise addition (The abelian group ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition).

[F4]

A $k$ -module is a vector space over the field $k$ , and the elements $e_{n}$ form a basis: distinct basis vectors are $k$ -linearly independent because a finite linear combination $\sum a_{n} e_{n}$ has $n$ -th coordinate $a_{n}$ (Field, Generated submodule, cyclic and finitely generated modules, module basis and free module).

[F5]

The singleton ${G}$ is a separating set, that is, $G$ is a generator, exactly when for all $u \neq v : X \to Y$ there is $h : G \to X$ with $u \circ h \neq v \circ h$ (Generator and cogenerator of a category, Separating and coseparating sets of objects).

[F6]

The abelian-group-valued functor ${Hom}_{k} (P, -)$ preserves a coproduct $⨁_{i} Y_{i}$ precisely when its comparison $⨁_{i} {Hom}_{k} (P, Y_{i}) \to {Hom}_{k} (P, ⨁_{i} Y_{i})$ , $(h_{i}) \mapsto \sum_{i} ȷ_{i} h_{i}$ , is an isomorphism (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

Counterexample

1.1F1F2F5givenconstruct

( $P$ is projective and a generator.) As the free $k$ -module on $N$ , $P$ is projective by [F1] under the declared Axiom of Choice. For generation, let $u \neq v : X \to Y$ be distinct $k$ -linear maps and pick $x \in X$ with $(u - v) (x) \neq 0$ ; the family with $f_{0} : k \to X$ , $1 \mapsto x$ , and $f_{n} = 0$ for $n \geq 1$ extends by [F2] to a $k$ -linear $h : P \to X$ with $h (e_{0}) = x$ and $h (e_{n}) = 0$ for $n \geq 1$ . Then $(u - v) h \neq 0$ , so $u h \neq v h$ , and by [F5] the object $P$ is a generator.

1.2F2F3givenalgebra

(Every map in the comparison image has finite-dimensional range.) An element of the source $⨁_{n} {Hom}_{k} (P, k)$ is a family $(φ_{n})$ with finite support by [F2], and by the universal property of the direct sum its image under the canonical comparison is the map $c (φ) : x \mapsto \sum_{n} φ_{n} (x) e_{n}$ with $φ_{n} = 0$ off a finite set $F$ . For $x \in P$ one has $c (φ) (x) \in ⨁_{n \in F} k e_{n}$ , a finite-dimensional subspace of $P$ ; hence $im c (φ) \subseteq ⨁_{n \in F} k e_{n}$ .

2.1F4step 1.2givenalgebra

( ${id}_{P}$ is not in that image.) Suppose ${id}_{P} = c (φ)$ for some finite-support family $(φ_{n})$ with support $F$ . Then every basis vector $e_{m}$ with $m \notin F$ would lie in $im c (φ) \subseteq ⨁_{n \in F} k e_{n}$ , so $e_{m}$ would be a finite $k$ -linear combination of the finitely many vectors $e_{n}$ , $n \in F$ , contradicting the linear independence of the basis recorded in [F4]. Hence ${id}_{P}$ is not in the image of the canonical comparison, and that comparison is not surjective.

3.1F1F6step 1.1step 2.1∎

(Conclusion.) By steps 1.1-2.1 the module $P$ is projective and a generator, but the canonical comparison $⨁_{n} {Hom}_{k} (P, k) \to {Hom}_{k} (P, P)$ fails to be surjective, so ${Hom}_{k} (P, -)$ does not preserve the coproduct $⨁_{n} k$ and $P$ is not a small projective generator by [F6] and Small projective generators and progenerators. Equivalently $P$ is not finitely generated, in agreement with Small projective modules are exactly finitely generated projective modules; the progenerator identification. Thus "projective generator" cannot replace "small projective generator", and the only use of choice is the projectivity from [F1], so the failure is not choice-free.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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