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 coproduct-preserving left exact module functor is not tensor

Statement refuted

Every additive module functor that is left exact and preserves coproducts is naturally isomorphic to a tensor functor.

Facts & Assumptions

Given: The functor $F = {Hom}_{Z} (Z / 2, -)$ on abelian groups, the cyclic group $Z / 2$ with classes $[0], [1]$ , and a family $(X_{i})_{i \in I}$ of abelian groups.

[F1]

${Hom}_{Z} (A, B)$ is an abelian group under pointwise addition, and postcomposition is a homomorphism (The abelian group ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition).

[F2]

Covariant ${Hom}_{R} (X, -)$ is left exact (Covariant and contravariant $Hom$ are left exact), and abelian groups are $Z$ -modules with the same homomorphisms (Abelian groups and $Z$ -modules have the same objects and morphisms).

[F3]

The direct sum $⨁_{i} X_{i}$ consists of finitely supported families and is the coproduct with coordinate inclusions; a homomorphism out of it is uniquely determined by its components (The direct sum of an indexed family of modules, Universal property of a direct sum of modules).

[F4]

In $Z / 2$ one has $[1] \neq [0]$ and $2 [1] = [0]$ , and every element is either $[0]$ or $[1]$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ , Addition and multiplication on $Z / n$ by $[a]_{n} + [b]_{n} = [a + b]_{n}$ and $[a]_{n} [b]_{n} = [a b]_{n}$ ). Consequently a homomorphism $φ : Z / 2 \to X$ is determined by $φ ([1])$ and satisfies $2 φ ([1]) = 0$ .

[F5]

A right exact functor between abelian categories preserves epimorphisms (A left exact functor preserves monomorphisms and a right exact functor preserves epimorphisms), and $A b$ is abelian (Abelian groups form an abelian category).

[F6]

Every tensor functor $T_{N} = N \otimes_{Z} - : A b \to A b$ is additive, right exact and coproduct-preserving, and right exactness is preserved under natural isomorphism (Eilenberg-Watts theorem for arbitrary unital rings).

[F7]

A functor is left exact when it preserves every finite limit and right exact when it preserves every finite colimit (Left exact and right exact functors).

Counterexample

technique · direct

1.1F1

$F$ is additive: for parallel homomorphisms $u, v : A \to B$ and $φ \in {Hom}_{Z} (Z / 2, A)$ , postcomposition satisfies $(u + v)_{*} (φ) = (u + v) \circ φ = u \circ φ + v \circ φ$ by [F1], so $F (u + v) = F (u) + F (v)$ .

1.2F3F4

$F$ preserves arbitrary direct sums: the canonical map $⨁_{i} {Hom}_{Z} (Z / 2, X_{i}) \to {Hom}_{Z} (Z / 2, ⨁_{i} X_{i})$ induced by the coordinate inclusions is bijective. It is injective because distinct components differ on $[1]$ in distinct coordinates by [F3]; it is surjective because for $φ$ the element $x = φ ([1])$ has finite support $S$ by [F3] and satisfies $2 x = 0$ by [F4], so each $x_{i}$ satisfies $2 x_{i} = 0$ and the maps $φ_{i} ([1]) = x_{i}$ defined for $i \in S$ and zero elsewhere are well-defined homomorphisms with $φ = \sum_{i} φ_{i}$ .

1.3F2F7

$F$ is left exact by [F2].

1.4F4F5F7

$F$ is not right exact. The map $u : Z \to Z / 2$ , $u (k) = [k]$ , is surjective, hence an epimorphism: if $g \circ u = h \circ u$ then $g$ and $h$ agree on every class. If $F$ were right exact, $F (u)$ would be an epimorphism by [F5]. But ${Hom}_{Z} (Z / 2, Z) = 0$ , since $2 φ ([1]) = 0$ in the torsion-free group $Z$ forces $φ ([1]) = 0$ by [F4]; so $F (u)$ is the zero map from $0$ to ${Hom}_{Z} (Z / 2, Z / 2)$ . That map is not an epimorphism, because the identity and zero endomorphisms of $H : = {Hom}_{Z} (Z / 2, Z / 2)$ are distinct ( $H$ contains the nonzero identity map of $Z / 2$ by [F4]) and both have the same composite with $0 \to H$ . Hence $F$ is not right exact.

2.1F6step 1.4

$F$ is not naturally isomorphic to any tensor functor $T_{N} = N \otimes_{Z} -$ : if $F ≅ T_{N}$ , then $F$ would be right exact, since $T_{N}$ is right exact by [F6] and right exactness is carried across a natural isomorphism, contradicting step 1.4.

3.1step 1.1step 1.2step 1.3step 1.4step 2.1∎

Thus $F$ is an additive functor that is left exact and preserves arbitrary direct sums, but is not tensor; the statement is refuted. No choice is used: the supports occurring in steps 1.2 and 1.4 are determined by the elements involved, and no family of nonempty sets is selected from.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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