LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Canonical free presentations force the comparison to be an isomorphism

Statement

Let $A, B$ be unital rings and let $F : A - M o d \to B - M o d$ be additive, right exact, and coproduct-preserving; put $M = F (A)$ with the $(B, A)$ -bimodule structure of $F (A)$ is a $(B, A)$ -bimodule for every additive functor $F$ . Then the canonical comparison $τ : M \otimes_{A} - \Rightarrow F$ of The canonical comparison to the tensor functor of $F (A)$ is balanced and natural is a natural isomorphism. Consequently $F$ is naturally isomorphic to the tensor functor $T_{F (A)}$ . No commutativity and no choice are used.

Facts & Assumptions

Given: Unital rings $A, B$ , an additive, right exact, coproduct-preserving functor $F : A - M o d \to B - M o d$ , the $(B, A)$ -bimodule $M = F (A)$ , and a left $A$ -module $X$ .

[F1]

The canonical comparison $τ_{X} : M \otimes_{A} X \to F (X)$ satisfies $τ_{X} (m \otimes x) = F (ℓ_{x}) (m)$ for $ℓ_{x} (a) = a x$ , each $τ_{X}$ is $B$ -linear, and $τ$ is natural: $F (u) \circ τ_{X} = τ_{Y} \circ (1_{M} \otimes u)$ (The canonical comparison to the tensor functor of $F (A)$ is balanced and natural).

[F2]

The formula $m a = F (r_{a}) (m)$ with $r_{a} (x) = x a$ makes $M$ a $(B, A)$ -bimodule ( $F (A)$ is a $(B, A)$ -bimodule for every additive functor $F$ ).

[F3]

$ρ_{M} : M \otimes_{A} A \to M$ , $ρ_{M} (m \otimes a) = m a$ , is a group isomorphism (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

[F4]

$T_{M} = M \otimes_{A} -$ is additive, right exact, preserves arbitrary direct sums including the empty one, and its induced maps are $B$ -linear when $M$ is a $(B, A)$ -bimodule (The functor $M \otimes_{A} -$ is additive, right exact, and preserves direct sums over an arbitrary unital ring).

[F5]

For an additive module functor, right exactness together with coproduct preservation is equivalent to preservation of cokernels and arbitrary direct sums (An additive module functor is cocontinuous exactly when it is right exact and preserves coproducts).

[F6]

The free module $A^{(X)}$ admits the canonical surjection $q_{X} : A^{(X)} \to X$ with $q_{X} (e_{x}) = x$ , and $A^{(K)}$ denotes the free module on the underlying set of a module $K$ (Every module is a quotient of a free module).

[F7]

A cokernel of $f : A \to B$ is a map $q : B \to coker (f)$ with $q f = 0$ such that every $h$ with $h f = 0$ factors uniquely as $h = \overline{h} \circ q$ (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

[F8]

The direct sum is the coproduct with coordinate inclusions, a map out of a coproduct is uniquely determined by its components, and the empty direct sum is the zero module (The direct sum of an indexed family of modules, Universal property of a direct sum of modules).

[F9]

Exactness of $A^{(K)} \overset{d}{\to} A^{(X)} \overset{q}{\to} X \to 0$ means $im d = \ker q$ and surjectivity of $q$ (Exact sequences and short exact sequences of modules).

[F10]

Module maps induce tensor maps functorially: $(1 \otimes v) \circ (1 \otimes u) = 1 \otimes (v \circ u)$ , and $(1 \otimes u) (m \otimes x) = m \otimes u (x)$ (Module homomorphisms induce tensor-product homomorphisms functorially).

Proof

technique · direct

1.1F1F2F3

At $A$ : since $ℓ_{a} = r_{a}$ , step [F1] and [F2] give $τ_{A} (m \otimes a) = F (ℓ_{a}) (m) = m a = ρ_{M} (m \otimes a)$ ; by [F3] the map $τ_{A} = ρ_{M}$ is an isomorphism.

1.2F4F5F8

Coproduct preservation: by [F5] the hypotheses make $F$ preserve cokernels and arbitrary direct sums, and $T_{M}$ preserves arbitrary direct sums by [F4]. Hence for any family $(Y_{i})$ the object $F (⨁_{i} Y_{i})$ with the maps $F (ȷ_{i})$ is a coproduct of the family $(F (Y_{i}))$ , and $M \otimes_{A} (⨁_{i} Y_{i})$ with the maps $1_{M} \otimes ȷ_{i}$ is a coproduct of the family $(M \otimes_{A} Y_{i})$ .

1.3F6F9

Presentation: put $K_{X} = \ker q_{X}$ for the canonical surjection $q_{X} : A^{(X)} \to X$ of [F6], let $q_{X}^{'} : A^{(K_{X})} \to K_{X}$ be the canonical surjection of [F6] for $K_{X}$ , and let $d_{X} : A^{(K_{X})} \to A^{(X)}$ be $q_{X}^{'}$ followed by the inclusion $K_{X} ↪ A^{(X)}$ . Then $im d_{X} = K_{X} = \ker q_{X}$ and $q_{X}$ is surjective, so $A^{(K_{X})} \overset{d_{X}}{\to} A^{(X)} \overset{q_{X}}{\to} X \to 0$ is exact.

2.1F1F8step 1.1step 1.2

Free modules: let $I$ be a set with coordinate inclusions $ι_{i} : A \to A^{(I)}$ . Naturality [F1] gives $F (ι_{i}) \circ τ_{A} = τ_{A^{(I)}} \circ (1_{M} \otimes ι_{i})$ for every $i$ . By step 1.2 the $1_{M} \otimes ι_{i}$ exhibit $M \otimes_{A} A^{(I)}$ as a coproduct of copies of $M \otimes_{A} A$ and the $F (ι_{i})$ exhibit $F (A^{(I)})$ as a coproduct of copies of $M$ ; comparing components shows that under these identifications $τ_{A^{(I)}}$ is the coproduct of the maps $τ_{A}$ , namely $⨁_{i} τ_{A}$ . A coproduct of isomorphisms is an isomorphism, its inverse being the map induced by the inverses of the components via [F8]; since $τ_{A}$ is an isomorphism by step 1.1, so is $τ_{A^{(I)}}$ , including $I = \emptyset$ .

2.2F1F4F5F7step 1.3

Induced map at $X$ : by right exactness [F4, F5] the maps $1_{M} \otimes q_{X}$ and $F (q_{X})$ are cokernels of $1_{M} \otimes d_{X}$ and $F (d_{X})$ respectively. Naturality [F1] gives $τ_{A^{(X)}} \circ (1_{M} \otimes d_{X}) = F (d_{X}) \circ τ_{A^{(K_{X})}}$ , so $F (q_{X}) \circ τ_{A^{(X)}}$ kills $im (1_{M} \otimes d_{X})$ ; by the cokernel universal property [F7] there is a unique map $τ_{X} : M \otimes_{A} X \to F (X)$ with $τ_{X} \circ (1_{M} \otimes q_{X}) = F (q_{X}) \circ τ_{A^{(X)}}$ .

3.1F1F7F10step 2.1step 2.2

Inverse at $X$ : since $(1_{M} \otimes q_{X}) \circ (1_{M} \otimes d_{X}) = 1_{M} \otimes (q_{X} \circ d_{X}) = 0$ by [F10] and step 1.3, and $τ_{A^{(X)}}^{- 1} \circ F (d_{X}) = (1_{M} \otimes d_{X}) \circ τ_{A^{(K_{X})}}^{- 1}$ by naturality [F1] and the invertibility of step 2.1, the composite $(1_{M} \otimes q_{X}) \circ τ_{A^{(X)}}^{- 1}$ kills $im F (d_{X})$ ; by [F7] there is a unique map $σ_{X} : F (X) \to M \otimes_{A} X$ with $σ_{X} \circ F (q_{X}) = (1_{M} \otimes q_{X}) \circ τ_{A^{(X)}}^{- 1}$ . Then $σ_{X} \circ τ_{X}$ and the identity agree after composition with the cokernel map $1_{M} \otimes q_{X}$ , and $τ_{X} \circ σ_{X}$ and the identity agree after composition with the cokernel map $F (q_{X})$ ; uniqueness in [F7] makes both composites the identity, so $τ_{X}$ is an isomorphism.

4.1F1step 1.1step 2.1step 3.1∎

Steps 1.1, 2.1 and 3.1 show that every component of the natural transformation $τ$ is an isomorphism, so $τ : M \otimes_{A} - \Rightarrow F$ is a natural isomorphism and $F ≅ T_{F (A)}$ ; the comparison was constructed before any presentation of $X$ was chosen, and no element of an auxiliary set is selected, so no presentation independence argument and no choice are needed.

Depends on

Used by

Dependency tree · two levels

35 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

M. Kamensky, Non-Commutative Algebra (BGU course notes, Spring 2017), §5.1, Theorem 5.1.43, Proposition 5.1.40, Lemma 5.1.46, Corollaries 5.1.48-5.1.49 (standard reference, not scraped)
A. Nyman and S. P. Smith, A Generalization of Watts's Theorem: Right Exact Functors on Module Categories, arXiv:0806.0832, Theorem 1.1-1.2, Propositions 3.2-3.3, Lemma 3.4 (standard reference, not scraped)
P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor Categories, §1.8, Proposition 1.8.10 (finite-dimensional free-presentation argument) (standard reference, not scraped)