ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedjudge 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 finite right exact functor needs no infinite-coproduct hypothesis

Example

Let $k$ be a field, let $A = k [ε] / (ε^{2})$ be the algebra of dual numbers (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, The quotient ring $R / I$ with $(r + I) (s + I) = r s + I$ ) and let $S = A / (ε)$ be its simple module (Simple module: a nonzero module with no proper nonzero submodule). Then: (i) $A - m o d$ has no countable coproduct of copies of $A$ , so it is not cocomplete; (ii) nevertheless the functor $T_{S} = S \otimes_{A} -$ , the case $M = S$ of the finite Eilenberg–Watts theorem, is right exact with right adjoint ${Hom}_{A} (S, -)$ , and it is classified by its kernel $T_{S} (A) ≅ S$ . Its right exactness, its right adjoint and its classification use only finite free presentations and the finite biproducts of $A - m o d$ ; no infinite coproducts are formed. Thus the finite classification requires no additional preservation hypothesis about infinite coproducts. Preservation of coproducts that do exist remains a meaningful condition; nonexistence of one countable coproduct does not make that condition vacuous. No choice is used.

Facts & Assumptions

Given: A field $k$ , the algebra $A = k [ε] / (ε^{2})$ of dual numbers, its simple module $S = A / (ε)$ , and the family of countably many copies of the regular module $A$ in $A - m o d$ .

[L1]

The algebra $A = k [ε] / (ε^{2})$ is a commutative unital $k$ -algebra in which the class $ε$ of the indeterminate satisfies $ε^{2} = 0$ and every element has the form $a + b ε$ with $a, b \in k$ ; hence $S = A / (ε)$ is a one-dimensional $k$ -vector space with $ε S = 0$ (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, The quotient ring $R / I$ with $(r + I) (s + I) = r s + I$ , Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

[L2]

$A - m o d$ , the category of finite-dimensional left $A$ -modules, is a finite $k$ -linear abelian category, hence locally finite: hom-spaces are finite-dimensional over $k$ and every object has finite length (Finite-dimensional module categories satisfy the intrinsic finiteness conditions).

[L3]

The $A$ -submodules of $S$ are exactly its $k$ -subspaces, because $A = k \cdot 1 \oplus k ε$ and $ε S = 0$ ; since $S$ is one-dimensional and nonzero, $S$ is a simple $A$ -module (Simple module: a nonzero module with no proper nonzero submodule, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

[L4]

For a left $A$ -module $M$ , evaluation at $1$ is a bijection ${Hom}_{A} (A, M) ≅ M$ of $k$ -vector spaces, since an $A$ -linear map is determined by its value at $1$ and $m \mapsto (a \mapsto a m)$ realizes every $m \in M$ (Universal property of a direct sum of modules, Unital left and right modules over a ring; unqualified module means left module, The abelian group ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition).

[L5]

A coproduct of a family $(X_{n})$ in a category is an object $X$ with morphisms $ȷ_{n} : X_{n} \to X$ such that every family of morphisms $X_{n} \to Y$ extends uniquely to $X \to Y$ ; in particular $Hom (X, Y) ≅ \prod_{n} Hom (X_{n}, Y)$ for every $Y$ , and in the category of $k$ -vector spaces $\prod_{n} k = k^{N}$ contains the countably many linearly independent vectors $e_{n}$ of finite support (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations, The abelian group ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

[L6]

Hom-spaces of $A - m o d$ are finite-dimensional over $k$ since the category is locally finite, and an independent family in a space with a finite spanning set has at most that many elements (Finite-dimensional module categories satisfy the intrinsic finiteness conditions, If $V$ has a spanning set with $n$ elements, then every linearly independent subset of $V$ is finite with at most $n$ elements; in particular $V$ has no linearly independent subset equinumerous with $N$ , Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

[L7]

For the finite-dimensional $(A, A)$ -bimodule $S$ the functor $T_{S} = S \otimes_{A} -$ is $k$ -linear and right exact, has right adjoint ${Hom}_{A} (S, -)$ taking finite-dimensional modules to finite-dimensional modules, and has kernel $T_{S} (A) = S \otimes_{A} A ≅ S$ ; its classification uses only finite free presentations and finite biproducts, and its right exactness and adjoint do not use any coproduct beyond the finite biproducts of $A - m o d$ (Finite Eilenberg–Watts for right exact linear functors, Finite one-sided exactness is equivalent to the existence of the corresponding adjoint, The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ , Unital left and right modules over a ring; unqualified module means left module, Module homomorphism and isomorphism, kernel, image and cokernel).

[L8]

The arbitrary-ring Eilenberg–Watts theorem classifies right exact functors that preserve arbitrary coproducts; its domain is the category of all modules, where arbitrary coproducts exist (Eilenberg-Watts theorem for arbitrary unital rings).

Verification

technique · direct

1.1L1L3algebra

By [L1] the quotient $S = A / (ε)$ is one-dimensional over $k$ with $ε S = 0$ and $S ≅ k$ , and by [L3] the $A$ -submodules of $S$ are its $k$ -subspaces, so $S \neq 0$ is a simple $A$ -module.

1.2L5L6

The space $k^{N}$ is infinite-dimensional: its vectors $e_{n}$ of finite support are linearly independent, so if it had a finite basis with $N$ elements then the $N + 1$ vectors $e_{0}, \dots, e_{N}$ would contradict the bound of [L6].

1.3L7

(ii) By [L7] the functor $T_{S}$ is $k$ -linear and right exact, has the right adjoint ${Hom}_{A} (S, -)$ which preserves finite-dimensional modules, and has kernel $T_{S} (A) ≅ S$ ; the classification of [L7] uses finite free presentations of finite-dimensional modules and only the finite biproducts of $A - m o d$ , so no infinite coproduct is formed.

2.1L4L5step 1.1given

Suppose a coproduct $X$ of the countably many copies of $A$ existed in $A - m o d$ . Taking $Y = S$ in the universal property of [L5] gives a bijection ${Hom}_{A} (X, S) ≅ \prod_{n \in N} {Hom}_{A} (A, S)$ , and ${Hom}_{A} (A, S) ≅ S$ as $k$ -vector spaces by evaluation at $1$ from [L4], The comparison is $k$ -linear, since it sends $f$ to $(f ȷ_{n})_{n}$ and therefore preserves pointwise addition and scalar multiplication. Hence ${Hom}_{A} (X, S) ≅ S^{N} ≅ k^{N}$ as $k$ -vector spaces by step 1.1.

3.1L2L6step 2.1step 1.2

But ${Hom}_{A} (X, S)$ for objects $X, S$ of $A - m o d$ is finite-dimensional by [L2] and [L6]. This contradicts step 2.1 together with step 1.2, so no such coproduct exists; in particular $A - m o d$ is not cocomplete, so it does not satisfy the cocompleteness hypothesis of the arbitrary-ring setting.

4.1L7L8step 1.3step 3.1∎

The finite classification [L7] applies to $T_{S}$ without any additional hypothesis about infinite coproducts, despite the nonexistence of the countable coproduct in step 3.1. The arbitrary-ring theorem [L8] concerns the category of all modules, which has arbitrary coproducts; it is not applied to this finite category. Preservation of existing coproducts is still meaningful here (for example the countable coproduct of zero modules exists), so noncocompleteness alone does not make preservation vacuous. All presentations and biproducts used in the classification are finite, so no choice is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

90 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

Etingof, Gelaki, Nikshych, Ostrik, Tensor Categories, §1.8 (Definitions 1.8.1–1.8.6, Proposition 1.8.10), printed pp.9–11 (standard reference, not scraped)
Fuchs, Schaumann, Schweigert, Eilenberg–Watts calculus for finite categories and a bimodule Radford S^4 theorem, arXiv:1612.04561v3, §2.1 (Lemma 2.1 (R1)-(R4)) (standard reference, not scraped)