Pipeline-generated

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.

✓ 12 results · all verified · 12 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 12 also cleared it.

Eilenberg–Watts Theorem and Natural Transformations

1 · Prerequisites

2 · Summary

This page develops the Eilenberg–Watts theorem for arbitrary unital rings, with left modules throughout and no commutativity assumption. It begins by defining the additive cocontinuous functors $A - M o d \to B - M o d$ and proving the schematic category laws and local smallness: every natural transformation is determined by its component at the regular module, and admissible components form a set for each fixed pair of functors. The categorical notation is metatheoretic shorthand under the library's definable-class convention; proper-class functors and transformation families are not treated as set-coded objects or morphisms. It also characterizes cocontinuity as right exactness plus preservation of arbitrary coproducts. Two local suppliers for the arbitrary-ring route record that $M \otimes_{A} -$ is additive, right exact and direct-sum-preserving for every right $A$ -module $M$ , and that the bimodule tensor–Hom adjunction $T_{M} ⊣ {Hom}_{B} (M, -)$ holds over arbitrary unital rings.

On that base the page constructs, for an additive functor $F$ , the $(B, A)$ -bimodule structure on $F (A)$ , the canonical balanced comparison $τ_{X} : M \otimes_{A} X \to F (X)$ defined before any presentation is chosen, and its naturality. Canonical free presentations then show $τ$ is an isomorphism whenever $F$ is right exact and coproduct-preserving, which yields the Eilenberg–Watts theorem: up to natural isomorphism the additive cocontinuous functors are exactly the tensor functors with bimodule kernels, the quasi-inverse being $F \mapsto F (_{A} A)$ .

The remaining items classify and apply the theorem: natural transformations between tensor functors correspond bijectively to bimodule maps with $η_{X} = f \otimes 1_{X}$ ; the classification is full, faithful and essentially surjective, hence a schematic equivalence of categories; every additive cocontinuous functor acquires a right adjoint ${Hom}_{B} (M, -)$ by transferring the unit and counit along $F ≅ T_{F (A)}$ ; and a tensor functor is exact exactly when its kernel is flat as a right module. The argument is choice-free, and the exactness criterion makes no left-side projectivity claim.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)Open item page →

Additive cocontinuous module functors and their schematic category

Definition

Let $A$ and $B$ be unital rings, and let $A - M o d$ and $B - M o d$ be their categories of unital left modules (Unital left and right modules over a ring; unqualified module means left module). A functor $F : A - M o d \to B - M o d$ is additive when its induced maps on hom-groups are group homomorphisms (Additive functor), and cocontinuous when it preserves every small (set-indexed) colimit (Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors). The functor is additive cocontinuous when it is both additive and cocontinuous.

Cocontinuity has a module-theoretic reformulation: an additive functor $F : A - M o d \to B - M o d$ preserves all small colimits if and only if it is right exact (Left exact and right exact functors) and preserves arbitrary direct sums. The characterization is proved in An additive module functor is cocontinuous exactly when it is right exact and preserves coproducts ↗.

We write ${F u n}_{a d d}^{c o c} (A - M o d, B - M o d)$ for the schematic category of these functors and natural transformations, with componentwise identities and vertical composition. As prescribed by Functor category $[C, D]$ and Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why $C A T$ is not formed, this is metatheoretic shorthand: functors on the large module category are fixed definable-class schemas, not set-coded objects of a ZFC class category. All categorical assertions here and in the Eilenberg–Watts equivalence are understood componentwise for fixed such schemas. For each fixed pair $F, G$ , Natural transformations of additive cocontinuous module functors are determined at the regular module ↗ proves that a natural transformation is determined by its component at $A$ and that the admissible components form a set. We use that set as $Nat (F, G)$ ; the corresponding proper-class families themselves are not elements of a set. No category of all definable-class functors is formed.

The term is a property of a functor; no commutativity of $A$ or $B$ is assumed, and no choice is used.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Natural transformations of additive cocontinuous module functors are determined at the regular module

Statement

Let $A, B$ be unital rings. The additive cocontinuous functors $A - M o d \to B - M o d$ (Additive cocontinuous module functors and their schematic category), satisfy the category laws schematically, with componentwise identities and vertical composition. For each fixed pair $F, G$ , every natural transformation $F \Rightarrow G$ is determined by its component at $A$ . The admissible components constitute a subset of ${Hom}_{B} (F (A), G (A))$ , giving a set of codes $Nat (F, G)$ . This is local smallness in the schematic sense of Additive cocontinuous module functors and their schematic category; it does not make proper-class functors or component families into sets. No choice is used.

Facts & Assumptions

Given: Unital rings $A$ and $B$ , additive cocontinuous functors $F, G : A - M o d \to B - M o d$ , and a natural transformation $η : F \Rightarrow G$ .

[F1]

A functor is additive cocontinuous when it is additive and preserves every small colimit; the categorical notation is schematic under the definable-class convention (Additive cocontinuous module functors and their schematic category).

[F2]

Additivity means that the induced maps on hom-groups are group homomorphisms; in particular the identity functor and composites of additive functors are additive (Additive functor).

[F3]

A natural transformation $η : F \Rightarrow G$ satisfies the naturality equation $G (u) \circ η_{X} = η_{Y} \circ F (u)$ for every $u : X \to Y$ (Natural transformation and its components).

[F4]

Identity transformations are natural, and the vertical composite $β \circ α$ of natural transformations is natural (componentwise) and is associative and unital componentwise (Identity natural transformation and vertical composition, Vertical composites of natural transformations satisfy naturality).

[F5]

The free module $A^{(X)}$ on the underlying set of a left $A$ -module $X$ carries the canonical surjection $q_{X} : A^{(X)} \to X$ with $q_{X} (e_{x}) = x$ (Every module is a quotient of a free module).

[F6]

A right exact functor between abelian categories preserves epimorphisms (A left exact functor preserves monomorphisms and a right exact functor preserves epimorphisms).

[F7]

$A - M o d$ and $B - M o d$ are abelian categories (Modules over a ring form an abelian category).

[F8]

A functor is right exact when it preserves every finite colimit; a cocontinuous functor preserves all small colimits and therefore every finite colimit (Left exact and right exact functors).

[F9]

The direct sum $⨁_{i \in I} X_{i}$ is the coproduct of the family with its coordinate inclusions $ȷ_{i}$ , and a homomorphism out of it is uniquely determined by its composites with the $ȷ_{i}$ (The direct sum of an indexed family of modules, Universal property of a direct sum of modules).

Proof

technique · direct

1.1F1F2

The identity functor $1_{A - M o d}$ is additive, its induced maps on hom-groups being identity homomorphisms, and it preserves every colimit; hence it is additive cocontinuous.

1.2F1F2

If $F : A - M o d \to B - M o d$ and $G : B - M o d \to C - M o d$ are additive cocontinuous, then $G F$ is additive, a composite of hom-group homomorphisms being one, and cocontinuous, since for a small diagram $D$ with colimit $L$ the object $F (L)$ is a colimit of $F \circ D$ and $G (F (L))$ is a colimit of $G \circ F \circ D$ .

1.3F1F3F4

Identity transformations and vertical composites are natural by [F4]. Associativity and the identity laws hold at each component. Thus the categorical operations satisfy their laws for fixed functor and transformation schemas; this does not form a category whose objects are proper classes.

1.4F1F3F9

Free modules: let $I$ be a set and let $ι_{i} : A \to A^{(I)}$ be the coordinate inclusions of the free module $A^{(I)} = ⨁_{i \in I} A$ , a coproduct of copies of $A$ . Since $F$ and $G$ preserve this coproduct, $F (A^{(I)})$ with the maps $F (ι_{i}) : M \to F (A^{(I)})$ , where $M = F (A)$ , is a coproduct of copies of $M$ , and by [F9] a map out of $F (A^{(I)})$ is determined by its composites with the maps $F (ι_{i})$ ; the same holds for $G (A^{(I)})$ with $N = G (A)$ . Naturality [F3] gives $η_{A^{(I)}} \circ F (ι_{i}) = G (ι_{i}) \circ η_{A}$ for every $i$ , so $η_{A^{(I)}}$ is determined by $η_{A}$ : if $η_{A} = 0$ then $η_{A^{(I)}} = 0$ .

1.5F5F6F7F8

Epic free covers: the canonical surjection $q_{X} : A^{(X)} \to X$ is an epimorphism, since two maps out of $X$ agreeing after composition with $q_{X}$ agree everywhere by surjectivity of $q_{X}$ . Each of $F, G$ is right exact by [F8], and $A - M o d$ , $B - M o d$ are abelian by [F7], so $F (q_{X})$ and $G (q_{X})$ are epimorphisms by [F6].

2.1F3step 1.4step 1.5

Suppose $η_{A} = θ_{A}$ for two natural transformations $F \Rightarrow G$ . Step 1.4 and naturality at every coordinate inclusion give $η_{A^{(X)}} = θ_{A^{(X)}}$ . Naturality at $q_{X}$ then gives $η_{X} \circ F (q_{X}) = G (q_{X}) \circ η_{A^{(X)}} = G (q_{X}) \circ θ_{A^{(X)}} = θ_{X} \circ F (q_{X})$ ; epicness of $F (q_{X})$ from step 1.5 yields $η_{X} = θ_{X}$ . Hence the transformations agree at every module.

3.1F1F3F5F9step 1.3step 1.5step 2.1∎

To obtain set codes, fix the defining formulas and parameters for $F, G$ . For $h \in {Hom}_{B} (F (A), G (A))$ and a module $X$ , let $p_{h, X} : F (A^{(X)}) \to G (X)$ be the unique map whose composite with $F (ι_{x})$ is $G (q_{X} ι_{x}) h$ for every $x \in X$ ; it exists by coproduct preservation and [F9]. Call $h$ admissible when, for every $X$ , there is a map $a_{X} : F (X) \to G (X)$ with $a_{X} F (q_{X}) = p_{h, X}$ , these maps satisfy $G (u) a_{X} = a_{Y} F (u)$ for every $u : X \to Y$ , and $a_{A} = h$ . The descents are unique by step 1.5, so this is a predicate quantifying only over sets and set-coded module maps, not over class families. Separation gives the set of admissible $h$ . Every natural transformation gives such a code by naturality at $q_{X} ι_{x}$ , and each admissible code defines its component family uniquely. Together with steps 1.3 and 2.1 this proves the claimed schematic category laws and local smallness, without applying replacement to proper-class-valued outputs. No choice is used.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

An additive module functor is cocontinuous exactly when it is right exact and preserves coproducts

Statement

Let $A, B$ be unital rings and $F : A - M o d \to B - M o d$ additive. Then $F$ preserves all small colimits if and only if $F$ preserves cokernels and arbitrary direct sums. Equivalently, $F$ is additive cocontinuous (Additive cocontinuous module functors and their schematic category) if and only if it is right exact (preserves every finite colimit that exists, Left exact and right exact functors) and preserves arbitrary coproducts. No commutativity and no choice are used.

Facts & Assumptions

Given: Unital rings $A$ and $B$ and an additive functor $F : A - M o d \to B - M o d$ .

[F1]

$F$ is additive cocontinuous when it is additive and preserves every small colimit (Additive cocontinuous module functors and their schematic category).

[F2]

A functor is right exact when it preserves every finite colimit that exists in its source category (Left exact and right exact functors).

[F3]

If $D : J \to C$ is small and the coproducts $R = ∐_{u : j \to k} D (j)$ , $S = ∐_{j} D (j)$ and the coequalizer of $d, c : R ⇉ S$ , with $d ι_{u} = ι_{j}$ and $c ι_{u} = ι_{k} D (u)$ , exist, then that coequalizer is a colimit of $D$ , with cocone built from the coproduct inclusions and the coequalizer map (Every small colimit can be constructed as a coequalizer between coproducts over the arrows and objects of the index category).

[F4]

$A - M o d$ has all small colimits (For every ring R, the category R-Mod is complete and cocomplete).

[F5]

In the additive category $A - M o d$ a coequalizer of a parallel pair is exactly a cokernel of the difference, and conversely (In a preadditive category, the coequalizer of a parallel pair is the cokernel of their difference); a cokernel is a coequalizer of the pair $(f, 0)$ , hence a finite colimit.

[F6]

An additive functor between additive categories preserves finite biproducts (An additive functor preserves finite biproducts).

[F7]

$A - M o d$ and $B - M o d$ are abelian, hence additive (Modules over a ring form an abelian category).

[F8]

In a module category the direct sum $⨁_{i \in I} X_{i}$ is the coproduct of the family with coordinate inclusions $ȷ_{i}$ , so a functor preserving arbitrary direct sums carries the coproduct cone of every family to a coproduct cone, and conversely (The direct sum of an indexed family of modules, Universal property of a direct sum of modules).

Proof

technique · direct

1.1F1F2F5F8

If $F$ preserves all small colimits, then it preserves cokernels and arbitrary direct sums, since a cokernel is the coequalizer of the pair $(f, 0)$ and a direct sum is a coproduct, both small colimits by [F5] and [F8]; and it is right exact, since every finite colimit is a small colimit. Hence the first alternative implies the second.

1.2F3F4F8

Conversely assume $F$ preserves cokernels and arbitrary direct sums, and let $D : J \to A - M o d$ be a small diagram with colimit $L$ . By [F4] the coproducts $R = ∐_{u : j \to k} D (j)$ and $S = ∐_{j} D (j)$ exist, and by [F3] the coequalizer $q : S \to L$ of $d, c : R ⇉ S$ is a colimit of $D$ with its canonical cocone.

1.3F2F3F5F6F8

The two hypothesis families agree for additive $F$ : if $F$ is right exact and preserves arbitrary coproducts, then it preserves cokernels, since cokernels are finite colimits; and conversely, if $F$ preserves cokernels and arbitrary direct sums, then it preserves every finite coproduct by [F6], because finite coproducts in an additive category are finite biproducts, and it preserves every finite colimit by the finite instance of the construction [F3] together with [F5], since the coproducts over the arrows and objects of a finite index category are finite coproducts. Hence cokernel-plus-direct-sum preservation is equivalent to right-exactness-plus-coproduct preservation.

2.1F3F5F7F8step 1.2

Under the assumption of step 1.2, $F (R)$ together with the maps $F (ι_{u})$ is a coproduct of the family $(F (D (j)))_{u : j \to k}$ and $F (S)$ with the maps $F (ι_{j})$ is a coproduct of the family $(F (D (j)))_{j}$ , because $F$ preserves the coproduct cones by [F8]; moreover $F (d) \circ F (ι_{u}) = F (ι_{j})$ and $F (c) \circ F (ι_{u}) = F (ι_{k}) F (D (u))$ , and $F (q)$ is a cokernel of $F (d - c) = F (d) - F (c)$ because $F$ preserves the cokernel of $d - c$ . By [F5] applied in $B - M o d$ , $F (q)$ is therefore the coequalizer of $F (d), F (c)$ , and by [F3] applied to the small diagram $F \circ D$ the object $F (L)$ with the image of the colimit cocone of $D$ is a colimit of $F \circ D$ . Hence $F$ preserves the colimit of $D$ .

3.1F1step 1.1step 1.3step 2.1∎

Step 1.1 gives the forward and step 2.1 the reverse implication of the first equivalence, so an additive $F$ preserves all small colimits exactly when it preserves cokernels and arbitrary direct sums; step 1.3 identifies the second hypothesis family with right exactness plus coproduct preservation, so $F$ is additive cocontinuous if and only if it is right exact and preserves arbitrary coproducts. No element, presentation, or diagram is chosen globally, so no choice is used.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

$F (A)$ is a $(B, A)$ -bimodule for every additive functor $F$

Statement

Let $A$ and $B$ be unital rings and let $F : A - M o d \to B - M o d$ be an additive functor (Additive functor). On the left $B$ -module $M = F (A)$ define, for $a \in A$ and $m \in M$ ,

$m a : = F (r_{a}) (m),$

where $r_{a} : A \to A$ , $r_{a} (x) = x a$ , is right multiplication, a left $A$ -linear endomorphism of $A$ . Together with the given left $B$ -action this makes $M$ a $(B, A)$ -bimodule ( $(S, R)$ -bimodules and commuting left and right scalar actions): the right $A$ -action satisfies the unit, associativity and distributivity laws of Unital left and right modules over a ring; unqualified module means left module and commutes with the left $B$ -action. No commutativity of the rings is assumed and no choice is used.

Facts & Assumptions

Given: Unital rings $A$ and $B$ , an additive functor $F : A - M o d \to B - M o d$ , and the left $B$ -module $M = F (A)$ .

[F1]

A right $R$ -module is an abelian group with an action $(m, r) \mapsto m r$ satisfying the right-handed analogues of the left-module axioms, in particular $m 1 = m$ , $(m + m^{'}) a = m a + m^{'} a$ , $m (a + a^{'}) = m a + m a^{'}$ and $(m a) a^{'} = m (a a^{'})$ (Unital left and right modules over a ring; unqualified module means left module). Multiplication in a ring satisfies $(c x) a = c (x a)$ and $x (a + a^{'}) = x a + x a^{'}$ .

[F2]

An additive functor satisfies $F (f + g) = F f + F g$ for every parallel pair of morphisms $f, g$ (Additive functor).

[F3]

A functor satisfies $F (1_{X}) = 1_{F X}$ and $F (g \circ f) = F g \circ F f$ (Covariant functor, identity functor, composite functor, and contravariant functor).

[F4]

An $(S, R)$ -bimodule is an abelian group that is a left $S$ -module and a right $R$ -module whose two actions commute ( $(S, R)$ -bimodules and commuting left and right scalar actions).

Proof

technique · direct

1.1F1F3

For $a \in A$ the map $r_{a} : A \to A$ , $r_{a} (x) = x a$ , is a left $A$ -module endomorphism, because $r_{a} (x + y) = r_{a} (x) + r_{a} (y)$ and $r_{a} (c x) = (c x) a = c (x a) = c r_{a} (x)$ by the ring laws. Hence $F (r_{a}) : M \to M$ is a $B$ -linear, in particular additive, endomorphism, and $m a : = F (r_{a}) (m)$ defines a map $M \times A \to M$ with $(m + m^{'}) a = m a + m^{'} a$ for all $m, m^{'} \in M$ .

1.2F1F3

Unit law: $r_{1} = {i d}_{A}$ because $x 1 = x$ , so $m 1 = F ({i d}_{A}) (m) = F (1_{A}) (m) = 1_{M} (m) = m$ for every $m \in M$ .

1.3F1F3

Associativity: $r_{a a^{'}} = r_{a^{'}} \circ r_{a}$ because $x (a a^{'}) = (x a) a^{'}$ , so functoriality gives $F (r_{a a^{'}}) = F (r_{a^{'}}) F (r_{a})$ and hence $m (a a^{'}) = (m a) a^{'}$ for all $m \in M$ and $a, a^{'} \in A$ .

1.4F1F2

Additivity in the ring variable: $r_{a + a^{'}} = r_{a} + r_{a^{'}}$ because $x (a + a^{'}) = x a + x a^{'}$ , and additivity of $F$ gives $F (r_{a + a^{'}}) = F (r_{a}) + F (r_{a^{'}})$ , so $m (a + a^{'}) = m a + m a^{'}$ .

2.1F4givenstep 1.1

Commutation with the left $B$ -action: for $b \in B$ and $m \in M$ we have $b (m a) = b (F (r_{a}) (m)) = F (r_{a}) (b m) = (b m) a$ , since the morphism $F (r_{a})$ of $B - M o d$ is $B$ -linear.

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

Steps 1.1-1.4 make $M$ a right $A$ -module for the assignment $(m, a) \mapsto m a$ , and step 2.1 shows that this right $A$ -action commutes with the given left $B$ -action; by [F4] the abelian group $M$ is a $(B, A)$ -bimodule.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The canonical comparison to the tensor functor of $F (A)$ is balanced and natural

Statement

Let $A, B$ be unital rings, let $F : A - M o d \to B - M o d$ be additive, and let $M = F (A)$ carry the $(B, A)$ -bimodule structure of $F (A)$ is a $(B, A)$ -bimodule for every additive functor $F$ . For $x \in X$ let $ℓ_{x} : A \to X$ , $ℓ_{x} (a) = a x$ . Then

$β_{X} : M \times X \to F (X), β_{X} (m, x) = F (ℓ_{x}) (m),$

is balanced (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring) and $B$ -linear in $m$ , so it induces a unique group homomorphism

$τ_{X} : M \otimes_{A} X \to F (X), τ_{X} (m \otimes x) = F (ℓ_{x}) (m),$

and each $τ_{X}$ is $B$ -linear. Moreover $τ : M \otimes_{A} - \Rightarrow F$ is natural: $F (u) \circ τ_{X} = τ_{Y} \circ (1_{M} \otimes u)$ for every left $A$ -linear $u : X \to Y$ (Natural transformation and its components). The construction of $τ$ chooses no presentation of $X$ and no elements.

Facts & Assumptions

Given: Unital rings $A$ , $B$ , an additive functor $F : A - M o d \to B - M o d$ , the $(B, A)$ -bimodule $M = F (A)$ with $m a = F (r_{a}) (m)$ for $r_{a} (x) = x a$ , a left $A$ -module $X$ , and $x, x^{'} \in X$ , $a \in A$ , $m \in M$ , $b \in B$ .

[F1]

Left $A$ -modules satisfy the module axioms, and right multiplication $r_{a} (x) = x a$ is an endomorphism of the left $A$ -module $A$ (Unital left and right modules over a ring; unqualified module means left module).

[F2]

The formula $m a = F (r_{a}) (m)$ makes $M = F (A)$ a $(B, A)$ -bimodule, so the right $A$ -action and the left $B$ -action are defined and commute: $b (m a) = (b m) a$ ( $F (A)$ is a $(B, A)$ -bimodule for every additive functor $F$ ).

[F3]

A balanced map $M \times X \to W$ into an abelian group is additive in each variable and satisfies $c (m a, x) = c (m, a x)$ (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring).

[F4]

Every balanced map $b : M \times X \to W$ into an abelian group factors uniquely as $b = \overline{b} \circ τ$ through the universal balanced map $τ (m, x) = m \otimes x$ (Universal property of the tensor product for balanced maps into abelian groups).

[F5]

If $M$ is a $(B, A)$ -bimodule, then $M \otimes_{A} X$ carries a left $B$ -module structure with $b (m \otimes x) = (b m) \otimes x$ (A commuting outer scalar action descends to a tensor product).

[F6]

A natural transformation $α : F \Rightarrow G$ is a family of components satisfying $G (u) \circ α_{X} = α_{Y} \circ F (u)$ for every $u : X \to Y$ (Natural transformation and its components).

[F7]

Module maps induce tensor maps with $(1_{M} \otimes u) (m \otimes x) = m \otimes u (x)$ , functorially (Module homomorphisms induce tensor-product homomorphisms functorially).

Proof

technique · direct

1.1F1

For each $x \in X$ the map $ℓ_{x} : A \to X$ , $ℓ_{x} (a) = a x$ , is left $A$ -linear, since $(a + a^{'}) x = a x + a^{'} x$ and $(c a) x = c (a x)$ ; moreover $ℓ_{x + x^{'}} = ℓ_{x} + ℓ_{x^{'}}$ and $ℓ_{a x} = ℓ_{x} \circ r_{a}$ , because $ℓ_{a x} (c) = (c a) x = c (a x) = (ℓ_{x} \circ r_{a}) (c)$ .

2.1F1F2F3step 1.1

The pairing $β_{X} (m, x) = F (ℓ_{x}) (m)$ is well defined because $F (ℓ_{x}) : M \to F (X)$ is a $B$ -module homomorphism; it is additive in $m$ and $B$ -linear in $m$ because $F (ℓ_{x})$ is, and additive in $x$ because $F (ℓ_{x + x^{'}}) = F (ℓ_{x}) + F (ℓ_{x^{'}})$ by additivity of $F$ and step 1.1. It is balanced: $β_{X} (m a, x) = F (ℓ_{x}) (m a) = F (ℓ_{x}) (F (r_{a}) (m)) = F (ℓ_{x} \circ r_{a}) (m) = F (ℓ_{a x}) (m) = β_{X} (m, a x)$ by step 1.1, [F2] and functoriality.

3.1F4F5step 2.1

By [F4] the balanced pairing $β_{X}$ induces a unique group homomorphism $τ_{X} : M \otimes_{A} X \to F (X)$ with $τ_{X} (m \otimes x) = F (ℓ_{x}) (m)$ . It is $B$ -linear: by [F5] the left $B$ -action on $M \otimes_{A} X$ satisfies $b (m \otimes x) = (b m) \otimes x$ , and $τ_{X} (b (m \otimes x)) = F (ℓ_{x}) (b m) = b F (ℓ_{x}) (m) = b τ_{X} (m \otimes x)$ , because $F (ℓ_{x})$ is $B$ -linear and elementary tensors generate; both sides are additive in the tensor variable, so equality on elementary tensors suffices.

4.1F6F7step 3.1

Naturality: for left $A$ -linear $u : X \to Y$ one has $u \circ ℓ_{x} = ℓ_{u (x)}$ , since $u (a x) = a u (x)$ , hence $F (u) \circ F (ℓ_{x}) = F (ℓ_{u (x)})$ by functoriality. Evaluating at $m$ and using $[F 7]$ gives $F (u) (τ_{X} (m \otimes x)) = F (ℓ_{u (x)}) (m) = τ_{Y} (m \otimes u (x)) = τ_{Y} ((1_{M} \otimes u) (m \otimes x))$ ; both sides are additive in the tensor variable and agree on elementary tensors, so $F (u) \circ τ_{X} = τ_{Y} \circ (1_{M} \otimes u)$ .

5.1F6step 3.1step 4.1∎

Steps 3.1 and 4.1 show that the components $τ_{X}$ are $B$ -linear maps assembling into a natural transformation $τ : M \otimes_{A} - \Rightarrow F$ with $τ_{X} (m \otimes x) = F (ℓ_{x}) (m)$ ; the formulas used only the given element $x$ and the module $A$ , never a presentation of $X$ , and no element of an auxiliary set is selected, so no presentation and no choice are involved.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Eilenberg-Watts theorem for arbitrary unital rings

Statement

Let $A, B$ be unital rings.

(i) For every $(B, A)$ -bimodule $M$ ( $(S, R)$ -bimodules and commuting left and right scalar actions) the functor $T_{M} = M \otimes_{A} - : A - M o d \to B - M o d$ is additive, right exact, coproduct-preserving and therefore cocontinuous (Additive cocontinuous module functors and their schematic category), and the assignment $M \mapsto T_{M}$ is functorial: a bimodule map $f : M \to M^{'}$ gives the natural transformation with components $f \otimes 1_{X}$ .

(ii) Conversely every additive cocontinuous functor $F : A - M o d \to B - M o d$ is naturally isomorphic to $T_{F (A)}$ , where $F (A)$ carries the $(B, A)$ -bimodule structure $m a = F (r_{a}) (m)$ ( $F (A)$ is a $(B, A)$ -bimodule for every additive functor $F$ ).

Hence, up to natural isomorphism, the additive cocontinuous functors are exactly the tensor functors with bimodule kernels: the quasi-inverse of $M \mapsto T_{M}$ is $F \mapsto F (_{A} A)$ , with categorical language interpreted schematically as in Additive cocontinuous module functors and their schematic category. No commutativity of $A$ or $B$ is assumed and no choice is used.

Facts & Assumptions

Given: Unital rings $A, B$ ; the class of additive cocontinuous functors $A - M o d \to B - M o d$ ; $(B, A)$ -bimodules $M, M^{'}$ ; an additive cocontinuous functor $F$ ; a bimodule map $f : M \to M^{'}$ .

[F1]

A functor is additive cocontinuous when it is additive and preserves every small colimit (Additive cocontinuous module functors and their schematic category).

[F2]

The additive cocontinuous functors with all natural transformations as morphisms satisfy the category laws schematically, with a set of component codes for each fixed Hom-collection, componentwise identities and vertical composition (Natural transformations of additive cocontinuous module functors are determined at the regular module).

[F3]

An additive module functor is cocontinuous if and only if it is right exact and preserves arbitrary coproducts; equivalently if and only if it preserves cokernels and arbitrary direct sums (An additive module functor is cocontinuous exactly when it is right exact and preserves coproducts).

[F4]

$T_{M} = M \otimes_{A} -$ is additive, right exact and preserves arbitrary direct sums, including the empty one; if $M$ is a $(B, A)$ -bimodule then $T_{M}$ takes values in left $B$ -modules and all displayed maps are $B$ -linear (The functor $M \otimes_{A} -$ is additive, right exact, and preserves direct sums over an arbitrary unital ring).

[F5]

Every bimodule map $f : M \to M^{'}$ yields a natural transformation $T_{M} \Rightarrow T_{M^{'}}$ with components $f \otimes 1_{X}$ , and the assignment is compatible with identities and vertical composition (Natural transformations between tensor functors are bimodule maps).

[F6]

If $F$ is additive and $M = F (A)$ , then $m a = F (r_{a}) (m)$ makes $M$ a $(B, A)$ -bimodule ( $F (A)$ is a $(B, A)$ -bimodule for every additive functor $F$ ).

[F7]

If $F$ is additive, right exact and coproduct-preserving and $M = F (A)$ with that bimodule structure, then the canonical comparison $τ : M \otimes_{A} - \Rightarrow F$ is a natural isomorphism (Canonical free presentations force the comparison to be an isomorphism).

[F8]

$ρ_{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$ ).

Proof

technique · direct

1.1F1F2F3F4F5

For a $(B, A)$ -bimodule $M$ the functor $T_{M}$ is additive, right exact and coproduct-preserving by [F4], hence cocontinuous by the equivalence [F3]. Given a bimodule map $f : M \to M^{'}$ , the components $f \otimes 1_{X}$ are natural in $X$ and compatible with identities and vertical composition by [F5], so they define a morphism $T_{M} \Rightarrow T_{M^{'}}$ in the category of [F2]; this makes $M \mapsto T_{M}$ a functor from $(B, A)$ -bimodules to the additive cocontinuous functors.

1.2F3F6F7

Let $F$ be additive cocontinuous. By [F3] it is right exact and coproduct-preserving, and $M : = F (A)$ is a $(B, A)$ -bimodule by [F6]. The canonical comparison $τ : M \otimes_{A} - \Rightarrow F$ is then a natural isomorphism by [F7], so $F ≅ T_{F (A)}$ .

2.1F8step 1.1step 1.2

The two assignments are inverse up to natural isomorphism: for a bimodule $M$ one has $T_{M} (A) = M \otimes_{A} A ≅ M$ by the unit isomorphism [F8], and for additive cocontinuous $F$ one has $F ≅ T_{F (A)}$ by step 1.2. Steps 1.1 and 1.2 therefore show that, up to natural isomorphism, the additive cocontinuous functors $A - M o d \to B - M o d$ are exactly the functors $T_{M}$ with $M$ a $(B, A)$ -bimodule, with quasi-inverse $F \mapsto F (_{A} A)$ .

3.1step 1.1step 1.2step 2.1∎

The construction of $τ$ used no presentation of any module and no element selection, and the module category is treated over arbitrary unital rings; hence neither commutativity of $A$ or $B$ nor the axiom of choice is used.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Natural transformations between tensor functors are bimodule maps

Statement

Let $A, B$ be unital rings and let $M, M^{'}$ be $(B, A)$ -bimodules ( $(S, R)$ -bimodules and commuting left and right scalar actions), with tensor functors $T_{M} = M \otimes_{A} -$ and $T_{M^{'}} = M^{'} \otimes_{A} -$ . Under the tensor-unit isomorphisms $ρ_{M} : M \otimes_{A} A \to M$ and $ρ_{M^{'}} : M^{'} \otimes_{A} A \to M^{'}$ of The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ , every natural transformation $η : T_{M} \Rightarrow T_{M^{'}}$ corresponds to the $B$ -linear map

$f = ρ_{M^{'}} \circ η_{A} \circ ρ_{M}^{- 1} : M ⟶ M^{'}, f (m) = ρ_{M^{'}} (η_{A} (m \otimes 1)),$

which satisfies $f (m a) = f (m) a$ for all $a \in A$ , i.e. is a $(B, A)$ -bimodule map, and then $η_{X} = f \otimes 1_{X}$ for every left $A$ -module $X$ . Conversely every bimodule map $f : M \to M^{'}$ yields a natural transformation with components $f \otimes 1_{X}$ . The two assignments are inverse bijections $Nat (T_{M}, T_{M^{'}}) ≅ {Hom}_{B - A} (M, M^{'})$ , compatible with addition, identities, and vertical composition. No commutativity and no choice are used. Here $Nat (T_{M}, T_{M^{'}})$ uses bimodule maps as set codes for the component families, not those proper-class families as elements of a set.

Facts & Assumptions

Given: Unital rings $A, B$ , $(B, A)$ -bimodules $M, M^{'}$ , a left $A$ -module $X$ , and a natural transformation $η : T_{M} \Rightarrow T_{M^{'}}$ .

[F1]

The tensor-unit map $ρ_{N} : N \otimes_{A} A \to N$ , $ρ_{N} (n \otimes a) = n a$ , is an isomorphism with inverse $n \mapsto n \otimes 1$ and respects every displayed outer module structure (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

[F2]

If $M$ is a $(B, A)$ -bimodule and $X$ a left $A$ -module, then $M \otimes_{A} X$ is a left $B$ -module with $b (m \otimes x) = (b m) \otimes x$ , so $T_{M}, T_{M^{'}}$ take values in $B - M o d$ (A commuting outer scalar action descends to a tensor product).

[F3]

A $(B, A)$ -bimodule has commuting left $B$ -action and right $A$ -action; a $(B, A)$ -bimodule map is a map that is both $B$ -linear and $A$ -linear ( $(S, R)$ -bimodules and commuting left and right scalar actions).

[F4]

Naturality of $η$ : for every left $A$ -linear $u : X \to Y$ one has $(1_{M^{'}} \otimes u) \circ η_{X} = η_{Y} \circ (1_{M} \otimes u)$ (Natural transformation and its components).

[F5]

Module maps induce tensor maps with $(f \otimes g) (m \otimes x) = f (m) \otimes g (x)$ , functorially: $id \otimes id = id$ and $(f^{'} \circ f) \otimes (g^{'} \circ g) = (f^{'} \otimes g^{'}) \circ (f \otimes g)$ (Module homomorphisms induce tensor-product homomorphisms functorially).

[F6]

Vertical composition is componentwise, $(ξ \circ η)_{X} = ξ_{X} \circ η_{X}$ (Identity natural transformation and vertical composition).

[F7]

For left $R$ -modules, ${Hom}_{R}$ is an abelian group under pointwise addition, with postcomposition and precomposition homomorphisms (The abelian group ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition).

Proof

technique · direct

1.1F1F2F3F4

Define $f : = ρ_{M^{'}} \circ η_{A} \circ ρ_{M}^{- 1}$ , so $f (m) = ρ_{M^{'}} (η_{A} (m \otimes 1))$ by [F1]. Then $f$ is $B$ -linear, as a composite of the $B$ -linear maps $ρ_{M}^{- 1}$ , $η_{A}$ (a morphism in $B - M o d$ by [F2] and [F4]) and $ρ_{M^{'}}$ , which respect the outer structures by [F1]. Moreover $f (m a) = f (m) a$ for all $a \in A$ : naturality at the left $A$ -linear map $r_{a} : A \to A$ , $r_{a} (x) = x a$ , reads $η_{A} \circ (1_{M} \otimes r_{a}) = (1_{M^{'}} \otimes r_{a}) \circ η_{A}$ , and $m a \otimes 1 = (1_{M} \otimes r_{a}) (m \otimes 1)$ ; evaluating there and using that $ρ_{M^{'}}$ is $A$ -linear, so that $ρ_{M^{'}} ((1_{M^{'}} \otimes r_{a}) (y)) = ρ_{M^{'}} (y) a$ , gives $f (m a) = ρ_{M^{'}} (η_{A} (m \otimes 1)) a = f (m) a$ . By [F3] the map $f$ is a $(B, A)$ -bimodule map.

1.2F2F3F4F5

Conversely, let $f : M \to M^{'}$ be a $(B, A)$ -bimodule map and put $η_{X} : = f \otimes 1_{X} : M \otimes_{A} X \to M^{'} \otimes_{A} X$ by [F5]. Each $η_{X}$ is $B$ -linear, since $η_{X} (b (m \otimes x)) = f (b m) \otimes x = b (f (m) \otimes x)$ , and the family is natural: for $u : X \to Y$ functoriality in [F5] gives $(f \otimes 1_{Y}) \circ (1_{M} \otimes u) = f \otimes u = (1_{M^{'}} \otimes u) \circ (f \otimes 1_{X})$ .

2.1F1F4F5step 1.1

Let $η$ be natural with associated $f$ from step 1.1. Naturality at $ℓ_{x} : A \to X$ , $ℓ_{x} (a) = a x$ , gives $η_{X} \circ (1_{M} \otimes ℓ_{x}) = (1_{M^{'}} \otimes ℓ_{x}) \circ η_{A}$ ; evaluated at $m \otimes 1$ the left side is $η_{X} (m \otimes x)$ , while the right side is $(1_{M^{'}} \otimes ℓ_{x}) (f (m) \otimes 1) = f (m) \otimes x$ , using $f (m) = ρ_{M^{'}} (η_{A} (m \otimes 1))$ and $ρ_{M^{'}}^{- 1} (f (m)) = f (m) \otimes 1$ from [F1]. Both $η_{X}$ and $f \otimes 1_{X}$ are homomorphisms agreeing on every elementary tensor, so $η_{X} = f \otimes 1_{X}$ ; in particular $η$ is determined by $f$ .

3.1F1F3F5step 1.1step 1.2step 2.1

The assignments are inverse: starting from a bimodule map $f$ , the transformation of step 1.2 has associated map $f^{'} = ρ_{M^{'}} \circ (f \otimes 1_{A}) \circ ρ_{M}^{- 1}$ , and $f^{'} (m) = ρ_{M^{'}} (f (m) \otimes 1) = f (m)$ by [F1] and [F5]; starting from $η$ , its associated $f$ satisfies $f \otimes 1_{X} = η_{X}$ for all $X$ by step 2.1. Hence $η \mapsto f$ is a bijection onto the set of $(B, A)$ -bimodule maps.

4.1F5F6F7step 1.1step 2.1step 3.1

Compatibility: sums of natural transformations, defined componentwise, are natural, and $f_{η + η^{'}} = f_{η} + f_{η^{'}}$ because $ρ_{M^{'}}$ and $η \mapsto η_{A}$ are additive; conversely sums of bimodule maps are bimodule maps and $(f + f^{'}) \otimes 1_{X} = f \otimes 1_{X} + f^{'} \otimes 1_{X}$ by [F5] and agreement on elementary tensors. The identity $1_{T_{M}}$ corresponds to $1_{M}$ in both directions, since $ρ_{M} (m \otimes 1) = m$ and $1_{M} \otimes 1_{X} = id$ by [F5]. Vertical composition corresponds to composition: by [F6] and step 2.1, for $ξ : T_{M^{'}} \Rightarrow T_{M^{''}}$ with associated $g$ one has $(ξ \circ η)_{A} (m \otimes 1) = ξ_{A} (f (m) \otimes 1) = g (f (m)) \otimes 1$ , so $ξ \circ η$ is associated with $g \circ f$ , while $(g \otimes 1_{X}) \circ (f \otimes 1_{X}) = (g \circ f) \otimes 1_{X}$ by [F5]; by [F7] these operations are the additions and compositions on the two Hom-groups.

5.1step 1.1step 1.2step 2.1step 3.1step 4.1∎

Steps 1.1-3.1 establish the bijection $Nat (T_{M}, T_{M^{'}}) ≅ {Hom}_{B - A} (M, M^{'})$ with $η_{X} = f \otimes 1_{X}$ , and step 4.1 shows it is compatible with addition, identities and vertical composition. Nothing was chosen, and no commutativity was used.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Eilenberg-Watts is a schematic equivalence of Hom categories

Statement

Let $A, B$ be unital rings. The assignment $M \mapsto T_{M}$ extends to an schematic equivalence between the category of $(B, A)$ -bimodules with bimodule maps ( $(S, R)$ -bimodules and commuting left and right scalar actions) and the category of additive cocontinuous functors $A - M o d \to B - M o d$ with natural transformations (Natural transformations of additive cocontinuous module functors are determined at the regular module). It is full and faithful with $Nat (T_{M}, T_{M^{'}}) ≅ {Hom}_{B - A} (M, M^{'})$ , naturally in $M$ and $M^{'}$ , and essentially surjective by Eilenberg-Watts theorem for arbitrary unital rings; a quasi-inverse is $F \mapsto F (_{A} A)$ . In particular $T_{M} ≅ T_{M^{'}}$ if and only if $M ≅ M^{'}$ as $(B, A)$ -bimodules. Categorical language has the schematic meaning of Additive cocontinuous module functors and their schematic category; no category with proper-class functors as set-coded objects is asserted. No commutativity and no choice are used.

Facts & Assumptions

Given: Unital rings $A, B$ and $(B, A)$ -bimodules $M, M^{'}, M_{1}, M_{2}$ .

[F1]

The assignment $M \mapsto T_{M} = M \otimes_{A} -$ lands in additive cocontinuous functors, and a bimodule map $f : M \to M^{'}$ gives the natural transformation with components $f \otimes 1_{X}$ , compatibly with identities and vertical composition; every additive cocontinuous functor $F$ is naturally isomorphic to $T_{F (A)}$ (Eilenberg-Watts theorem for arbitrary unital rings).

[F2]

The additive cocontinuous functors with all natural transformations form a schematic category with set-coded fixed Hom-collections, and the $(B, A)$ -bimodules with bimodule maps form a locally small category because each Hom-collection is a set of functions (Natural transformations of additive cocontinuous module functors are determined at the regular module, $(S, R)$ -bimodules and commuting left and right scalar actions).

[F3]

The assignment $f \mapsto (f \otimes 1_{X})$ is a bijection ${Hom}_{B - A} (M, M^{'}) \to Nat (T_{M}, T_{M^{'}})$ , and the two assignments are compatible with addition, identities and vertical composition; the inverse sends $η$ to $ρ_{M^{'}} \circ η_{A} \circ ρ_{M}^{- 1}$ (Natural transformations between tensor functors are bimodule maps).

[F4]

A functor is fully faithful when every induced hom-map is bijective and split essentially surjective when the data assign to every object $D$ of the target an object $C$ with an isomorphism $F C ≅ D$ ; such a functor is an equivalence, and no choice principle is needed because the splitting is part of the data (Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors, A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice).

[F5]

A natural isomorphism has an inverse natural transformation (Natural isomorphism).

Proof

technique · direct

1.1F1F2

Let $Φ$ be the assignment $M \mapsto T_{M}$ on objects of the bimodule category and $f \mapsto (f \otimes 1_{X})$ on morphisms. By [F1] the objects are additive cocontinuous functors and the morphisms are natural transformations, compatibly with identities and vertical composition, so $Φ$ respects the schematic category operations of [F2]; fixed Hom-collections are represented by sets by [F2].

1.2F3

$Φ$ is full and faithful: for every pair $M, M^{'}$ the map $Φ_{M, M^{'}} : {Hom}_{B - A} (M, M^{'}) \to Nat (T_{M}, T_{M^{'}})$ is the bijection of [F3].

1.3F1

$Φ$ is split essentially surjective: by [F1] every additive cocontinuous $F$ is naturally isomorphic to $T_{F (A)} = Φ (F (A))$ , and $F (A)$ together with that isomorphism is determined by $F$ , so the required data are supplied without any selection.

2.1F1F3F4step 1.1step 1.2step 1.3

The construction proving [F4] applies schematically: for $η : F \Rightarrow G$ , define $E (η)$ as the unique bimodule map whose tensor transformation is $τ_{G}^{- 1} \circ η \circ τ_{F}$ , using the canonical comparisons $τ_{F} : T_{F (A)} \Rightarrow F$ of [F1] and the bijection [F3]. Composition compatibility makes $E$ functorial, and $τ$ is natural in $F$ by this defining equation. Since $τ_{F, A} = ρ_{F (A)}$ , [F3] gives $E (η) = η_{A}$ . The tensor-unit maps give the other natural isomorphism $E (T_{M}) ≅ M$ : the reconstructed right action is $(m \otimes a) b = m \otimes a b$ , and $ρ_{M} (m \otimes a b) = (m a) b$ , while naturality follows on elementary tensors, so $E (F) = F (A)$ is a schematic quasi-inverse. No quantification over objects that are proper classes is needed.

2.2F3step 1.2

Naturality in $M$ and $M^{'}$ : for a bimodule map $h : M_{1} \to M_{2}$ and $f^{'} : M_{2} \to M^{'}$ , the bijection of [F3] sends $f^{'} \circ h$ to the vertical composite of $(f^{'} \otimes 1_{X})$ with $(h \otimes 1_{X})$ by the composition compatibility in [F3]; likewise postcomposition with a bimodule map corresponds to postcomposition with its tensor transformation. Hence the bijections are natural in both variables.

2.3F3F5step 1.2

The bijection identifies natural isomorphisms with bimodule isomorphisms: if $η : T_{M} \Rightarrow T_{M^{'}}$ is a natural isomorphism with associated $f$ and inverse $η^{- 1}$ with associated $g$ , then the identities $η^{- 1} \circ η = 1_{T_{M}}$ and $η \circ η^{- 1} = 1_{T_{M^{'}}}$ translate under the compatibility of [F3] into $g \circ f = 1_{M}$ and $f \circ g = 1_{M^{'}}$ , because the bijection sends $1_{T_{M}}$ to $1_{M}$ ; conversely, for a bimodule isomorphism $f$ the transformation with components $f \otimes 1_{X}$ is a natural isomorphism with components $f^{- 1} \otimes 1_{X}$ . Hence $T_{M} ≅ T_{M^{'}}$ if and only if $M ≅ M^{'}$ .

3.1step 1.1step 1.2step 1.3step 2.1step 2.2step 2.3∎

Steps 1.1-2.1 exhibit the equivalence $Φ$ with quasi-inverse $F \mapsto F (A)$ , step 2.2 its naturality in both variables, and step 2.3 the isomorphism statement. No object or presentation was chosen, and no commutativity is used.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Additive cocontinuous module functors admit right adjoints

Statement

Let $A, B$ be unital rings. Every additive cocontinuous functor $F : A - M o d \to B - M o d$ admits a right adjoint $B - M o d \to A - M o d$ : if $M$ is a $(B, A)$ -bimodule with $F ≅ T_{M}$ , then $F$ is left adjoint to ${Hom}_{B} (M, -)$ . In particular $F$ is a left adjoint, so it preserves every colimit that exists. No commutativity and no choice are used.

Facts & Assumptions

Given: Unital rings $A, B$ , an additive cocontinuous functor $F : A - M o d \to B - M o d$ , and $G : = {Hom}_{B} (M, -)$ for $M : = F (A)$ .

[F1]

$M = F (A)$ is a $(B, A)$ -bimodule and $F$ is naturally isomorphic to $T_{M} = M \otimes_{A} -$ (Eilenberg-Watts theorem for arbitrary unital rings, $(S, R)$ -bimodules and commuting left and right scalar actions).

[F2]

$T_{M}$ is left adjoint to ${Hom}_{B} (M, -)$ : there are a unit $η : 1 \Rightarrow G T_{M}$ and a counit $ε : T_{M} G \Rightarrow 1$ satisfying the triangle identities (Tensor-Hom adjunction for bimodules over arbitrary unital rings).

[F3]

An adjunction is a unit and counit satisfying $(ε F) \circ (F η) = 1_{F}$ and $(G ε) \circ (η G) = 1_{G}$ ; componentwise, $ε_{F X} \circ F (η_{X}) = 1_{F X}$ and $G (ε_{Y}) \circ η_{G Y} = 1_{G Y}$ (Adjunction by unit, counit, and the triangle identities).

[F4]

Left whiskering $H α$ has components $H (α_{A})$ and right whiskering $α K$ has components $α_{K B}$ (Whiskering and horizontal composition of natural transformations).

[F5]

A natural isomorphism $σ$ has an inverse natural transformation $σ^{- 1}$ with $σ^{- 1} \circ σ = 1$ and $σ \circ σ^{- 1} = 1$ (Natural isomorphism); vertical composition is componentwise (Identity natural transformation and vertical composition).

[F6]

A left adjoint preserves every colimit that exists (Left adjoints preserve every colimit that exists).

Proof

technique · direct

1.1F1F2F5

By [F1] there is a natural isomorphism $σ : T_{M} \Rightarrow F$ with inverse $σ^{- 1} : F \Rightarrow T_{M}$ , and $M$ is a $(B, A)$ -bimodule. By [F2] there are a unit $η : 1 \Rightarrow G T_{M}$ and a counit $ε : T_{M} G \Rightarrow 1$ satisfying the triangle identities of [F3] for the adjunction $T_{M} ⊣ G$ .

2.1F3F4F5step 1.1

Transfer: put $η^{'} : = (G σ) \circ η : 1 \Rightarrow G F$ and $ε^{'} : = ε \circ (σ^{- 1} G) : F G \Rightarrow 1$ , using the whiskerings of [F4]; these are natural transformations by [F4] and [F5]. They satisfy the triangle identities of [F3]: at $X$ , using naturality of $σ^{- 1}$ at $G (σ_{X})$ , naturality of $σ$ at $η_{X}$ and naturality of $ε$ at $σ_{X}$ , one computes $ε_{F (X)}^{'} \circ F (η_{X}^{'}) = ε_{F (X)} \circ (σ^{- 1})_{G (F (X))} \circ F (G (σ_{X})) \circ F (η_{X}) = ε_{F (X)} \circ T_{M} (G (σ_{X})) \circ T_{M} (η_{X}) \circ σ_{X}^{- 1} = σ_{X} \circ ε_{T_{M} (X)} \circ T_{M} (η_{X}) \circ σ_{X}^{- 1} = σ_{X} \circ σ_{X}^{- 1} = 1_{F (X)}$ ; and at $Y$ one computes $G (ε_{Y}^{'}) \circ η_{G (Y)}^{'} = G (ε_{Y}) \circ G ((σ^{- 1})_{G (Y)}) \circ G (σ_{G (Y)}) \circ η_{G (Y)} = G (ε_{Y}) \circ η_{G (Y)} = 1_{G (Y)}$ , where the middle step cancels the inverse components of [F5]. Hence $F ⊣ G$ in the sense of [F3].

3.1F6step 2.1∎

By step 2.1 the functor $F$ admits $G = {Hom}_{B} (M, -)$ as right adjoint, so it is a left adjoint and [F6] applies; in particular it preserves every colimit that exists, consistently with its assumed cocontinuity. The transfer used only the displayed units, counits and inverse components, so no commutativity and no choice are involved.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Exact module tensor functors correspond to right-flat bimodules

Statement

Let $A, B$ be unital rings and $M$ a $(B, A)$ -bimodule ( $(S, R)$ -bimodules and commuting left and right scalar actions). Then the tensor functor $T_{M} = M \otimes_{A} - : A - M o d \to B - M o d$ is exact (Exact functor between abelian categories) if and only if $M$ is flat as a right $A$ -module (Left and right flat modules over an arbitrary ring). Under the Eilenberg-Watts equivalence this is a bijection between isomorphism classes of exact tensor functors $A - M o d \to B - M o d$ and right-flat $(B, A)$ -bimodules. Isomorphism classes here are a schematic classification, not an assertion that either collection is a set. No commutativity and no choice are used.

Facts & Assumptions

Given: Unital rings $A, B$ and a $(B, A)$ -bimodule $M$ .

[F1]

A right $R$ -module $N$ is flat when $N \otimes_{R} -$ is exact on left $R$ -modules, i.e. when the functor $X \mapsto N \otimes_{R} X$ from left $R$ -modules to abelian groups is exact (Left and right flat modules over an arbitrary ring).

[F2]

A functor between abelian categories is exact when it is additive and both left and right exact (Exact functor between abelian categories).

[F3]

A functor between abelian categories is exact if and only if it carries every short exact sequence to a short exact sequence (Left exactness, right exactness, and exactness are characterized by short exact sequences).

[F4]

For a homomorphism of $B$ -modules, kernel, image and cokernel are computed on the underlying sets as $\ker f = {m : f (m) = 0}$ , $im f = {f (m)}$ and $coker f = N / im f$ ; a sequence of $B$ -modules is exact exactly when $im = \ker$ at every meeting point, and a short exact sequence has injective and surjective outer maps (Module homomorphism and isomorphism, kernel, image and cokernel, Exact sequences and short exact sequences of modules). Consequently a sequence of $B$ -modules is exact, respectively short exact, if and only if its underlying sequence of abelian groups is.

[F5]

$A - M o d$ , $B - M o d$ and $A b$ are abelian categories (Modules over a ring form an abelian category, Abelian groups form an abelian category).

[F6]

$T_{M}$ is additive (and right exact) (The functor $M \otimes_{A} -$ is additive, right exact, and preserves direct sums over an arbitrary unital ring).

[F7]

Under the Eilenberg-Watts equivalence $M \mapsto T_{M}$ is an equivalence of categories in the schematic sense of the cited equivalence, so $T_{M} ≅ T_{M^{'}}$ if and only if $M ≅ M^{'}$ as $(B, A)$ -bimodules (Eilenberg-Watts theorem for arbitrary unital rings, Eilenberg-Watts is a schematic equivalence of Hom categories).

Proof

technique · direct

1.1F2F3F4F5F6

Since $T_{M}$ is additive by [F6] and $A - M o d$ , $B - M o d$ , $A b$ are abelian by [F5], exactness of $T_{M}$ is characterised by short exact sequences by [F3]. By [F4] a sequence of $B$ -modules is short exact exactly when its underlying sequence of abelian groups is, so $T_{M}$ carries every short exact sequence of $A$ -modules to a short exact sequence of $B$ -modules if and only if the composite with the forgetful functor, the functor $X \mapsto M \otimes_{A} X$ from $A - M o d$ to $A b$ , does. That composite is additive, so by [F3] again it carries short exact sequences to short exact sequences if and only if it is exact; by [F2] this is equivalent to exactness of $M \otimes_{A} -$ .

2.1F1step 1.1

By [F1] the right $A$ -module $M$ is flat exactly when $M \otimes_{A} -$ is exact as a functor to abelian groups, which by step 1.1 is exactly when $T_{M}$ is exact. Hence $T_{M}$ is exact if and only if $M$ is right-flat.

3.1F7step 2.1

Isomorphism classes: by [F7] the assignment $M \mapsto T_{M}$ induces a bijection between isomorphism classes of $(B, A)$ -bimodules and isomorphism classes of tensor functors, and exactness is invariant under natural isomorphism, because a natural isomorphism intertwines the images of every short exact sequence termwise and an isomorphic copy of a short exact sequence is short exact by [F4]. Hence restricting along step 2.1 gives a bijection between isomorphism classes of exact tensor functors $A - M o d \to B - M o d$ and isomorphism classes of right-flat $(B, A)$ -bimodules.

4.1step 1.1step 2.1step 3.1∎

The corollary asserts exactness of $T_{M}$ precisely for right-flat $M$ ; it makes no claim about projectivity of $M$ as a left $B$ -module, which governs different functors. No commutativity and no choice are used, since the argument only transports exactness across the forgetful functor and invokes the displayed universal properties.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

The functor $M \otimes_{A} -$ is additive, right exact, and preserves direct sums over an arbitrary unital ring

Statement

Let $A$ be a unital ring and $M$ a right $A$ -module. Then the functor $T_{M} = M \otimes_{A} - : A - M o d \to A b$ is additive, preserves cokernels (so it is right exact: every exact sequence $X \overset{f}{\to} Y \overset{g}{\to} Z \to 0$ of left $A$ -modules induces an exact sequence $M \otimes_{A} X \overset{1 \otimes f}{\to} M \otimes_{A} Y \overset{1 \otimes g}{\to} M \otimes_{A} Z \to 0$ ), and preserves arbitrary direct sums: the natural map $⨁_{i \in I} (M \otimes_{A} X_{i}) \to M \otimes_{A} (⨁_{i \in I} X_{i})$ induced by the coordinate inclusions is an isomorphism, including $I = \emptyset$ . If $M$ is a $(B, A)$ -bimodule then $T_{M}$ takes values in left $B$ -modules and all the displayed maps are $B$ -linear. No commutativity of $A$ or $B$ is assumed and no choice is used.

Facts & Assumptions

Given: A unital ring $A$ , a right $A$ -module $M$ , a family $(X_{i})_{i \in I}$ of left $A$ -modules, parallel left $A$ -linear maps $u, v : X \to Y$ , an exact sequence $X \overset{f}{\to} Y \overset{g}{\to} Z \to 0$ of left $A$ -modules, and, for the final claim, a $(B, A)$ -bimodule structure on $M$ .

[F1]

The universal balanced map $τ (m, x) = m \otimes x$ is balanced, and every balanced map $b : M \times X \to W$ into an abelian group has a unique factorization $b = \overline{b} \circ τ$ with $\overline{b} (m \otimes x) = b (m, x)$ (Universal property of the tensor product for balanced maps into abelian groups).

[F2]

Module maps induce tensor maps with $(u \otimes v) (m \otimes x) = u (m) \otimes v (x)$ , functorially: $id \otimes id = id$ and $(u^{'} \circ u) \otimes (v^{'} \circ v) = (u^{'} \otimes v^{'}) \circ (u \otimes v)$ (Module homomorphisms induce tensor-product homomorphisms functorially).

[F3]

Every element of $M \otimes_{A} X$ is a finite sum of elementary tensors, and $m \otimes (n + n^{'}) = m \otimes n + m \otimes n^{'}$ , $(m + m^{'}) \otimes n = m \otimes n + m^{'} \otimes n$ , $(m a) \otimes n = m \otimes (a n)$ , $0 \otimes n = 0 = m \otimes 0$ (The tensor product $M \otimes_{R} N$ from the additive group underlying the free $Z$ -module on $M \times N$ , elementary tensors, and finite tensor sums). Consequently a homomorphism out of $M \otimes_{A} X$ is determined by its values on elementary tensors.

[F4]

Elements of $⨁_{i \in I} X_{i}$ are finitely supported families, the coordinate inclusions $ȷ_{i} : X_{i} \to ⨁_{j} X_{j}$ place the input in coordinate $i$ and zero elsewhere, and for $I = \emptyset$ the direct sum is the zero module (The direct sum of an indexed family of modules).

[F5]

For every family of maps $u_{i} : X_{i} \to N$ there is a unique $u : ⨁_{i} X_{i} \to N$ with $u \circ ȷ_{i} = u_{i}$ , given by $u ((x_{i})) = \sum_{i} u_{i} (x_{i})$ over the finite support, and for $I = \emptyset$ it is the unique map $0 \to N$ (Universal property of a direct sum of modules). Two homomorphisms out of a direct sum are equal as soon as they agree after composing with every $ȷ_{i}$ .

[F6]

Exactness of $X \overset{f}{\to} Y \overset{g}{\to} Z \to 0$ means $\ker g = im f$ and that $g$ is surjective (Exact sequences and short exact sequences of modules).

[F7]

The kernel of $g$ is ${y : g (y) = 0}$ , the image of $f$ is ${f (x)}$ , and the cokernel of a map is the quotient by its image (Module homomorphism and isomorphism, kernel, image and cokernel).

[F8]

If $M$ is a $(B, A)$ -bimodule then $M \otimes_{A} X$ carries a left $B$ -module structure with $b (m \otimes x) = (b m) \otimes x$ , and the actions of $M$ commute: $b (m a) = (b m) a$ (A commuting outer scalar action descends to a tensor product, $(S, R)$ -bimodules and commuting left and right scalar actions).

Proof

technique · direct

1.1F1F2F3

Additivity: for parallel maps $u, v : X \to Y$ and every elementary tensor, $(1 \otimes (u + v)) (m \otimes x) = m \otimes (u + v) (x) = m \otimes u (x) + m \otimes v (x) = (1 \otimes u) (m \otimes x) + (1 \otimes v) (m \otimes x)$ ; both sides are homomorphisms out of $M \otimes_{A} X$ , so they are equal by [F3]. Hence $T_{M}$ preserves addition of morphisms and is additive.

1.2F2F4F5

Direct sums, first map: by [F5] the maps $1_{M} \otimes ȷ_{i} : M \otimes_{A} X_{i} \to M \otimes_{A} (⨁_{j} X_{j})$ induce a unique homomorphism $Φ : ⨁_{i \in I} (M \otimes_{A} X_{i}) \to M \otimes_{A} (⨁_{i \in I} X_{i})$ whose composite with the coordinate inclusion $ȷ_{i}^{'} : M \otimes_{A} X_{i} \to ⨁_{i} (M \otimes_{A} X_{i})$ is $1_{M} \otimes ȷ_{i}$ for every $i$ .

1.3F1F3F4

Direct sums, inverse: the pairing $b (m, (x_{i})_{i}) : = (m \otimes x_{i})_{i}$ is well defined and balanced because the family $(x_{i})$ has finite support, addition is coordinatewise, and $b (m a, (x_{i})) = (m a \otimes x_{i})_{i} = (m \otimes (a x_{i}))_{i} = b (m, a (x_{i}))$ ; by [F1] it induces $Ψ : M \otimes_{A} (⨁_{i} X_{i}) \to ⨁_{i} (M \otimes_{A} X_{i})$ with $Ψ (m \otimes (x_{i})_{i}) = (m \otimes x_{i})_{i}$ .

1.4F2F3F6

Cokernels, surjectivity and composite: $1 \otimes g$ is surjective, since every element of $M \otimes_{A} Z$ is a finite sum of elementary tensors $m \otimes z$ and $z = g (y)$ for some $y$ by [F6], so it is the image of $\sum m \otimes y$ . Also $(1 \otimes g) \circ (1 \otimes f) = 1 \otimes (g \circ f) = 1 \otimes 0 = 0$ , because $g \circ f = 0$ by [F6] and a homomorphism out of $M \otimes_{A} X$ vanishing on every elementary tensor is zero by [F3].

1.5F1F2F3F6F7

Cokernels, universal property: let $W$ be an abelian group and $v : M \otimes_{A} Y \to W$ a homomorphism with $v \circ (1 \otimes f) = 0$ . For $z \in Z$ choose $y \in Y$ with $g (y) = z$ and set $c (m, z) : = v (m \otimes y)$ . If $y^{'}$ is another lift then $y - y^{'} = f (x)$ for some $x \in X$ by [F6] and [F7], so $m \otimes y - m \otimes y^{'} = m \otimes f (x) = (1 \otimes f) (m \otimes x)$ by [F2] and [F3], whence $v (m \otimes y) = v (m \otimes y^{'})$ : the map $c$ is well defined. It is balanced, being additive in each variable with $c (m a, z) = v (m a \otimes y) = v (m \otimes (a y)) = c (m, a z)$ , so by [F1] it induces a unique homomorphism $w : M \otimes_{A} Z \to W$ with $w (m \otimes z) = v (m \otimes y)$ ; then $w \circ (1 \otimes g) = v$ , since both sides send $m \otimes y$ to $v (m \otimes y)$ , and any $w^{'}$ with $w^{'} \circ (1 \otimes g) = v$ satisfies $w^{'} (m \otimes z) = w^{'} (m \otimes g (y)) = v (m \otimes y)$ , so $w^{'} = w$ by [F3].

2.1F2F5F8step 1.2step 1.3

Bimodules: if $M$ is a $(B, A)$ -bimodule, then $M \otimes_{A} X$ is a left $B$ -module with $b (m \otimes x) = (b m) \otimes x$ by [F8], and every map considered above is $B$ -linear: the induced tensor maps by $(1 \otimes f) (b (m \otimes x)) = (b m) \otimes f (x) = b (m \otimes f (x))$ , and $Φ, Ψ$ because their defining pairings and families are $B$ -linear in $m$ and $B$ -linearity is checked on the generating elementary tensors and coordinate inclusions.

2.2F1F2F3F4F5step 1.2step 1.3

The maps $Φ$ and $Ψ$ are mutually inverse. First, $Ψ \circ Φ$ fixed on the generators $ȷ_{i} (m \otimes x_{i})$ of the direct sum equals $ȷ_{i} (m \otimes x_{i})$ , since $Φ (ȷ_{i} (m \otimes x_{i})) = (1 \otimes ȷ_{i}) (m \otimes x_{i}) = m \otimes ȷ_{i} (x_{i})$ and then $Ψ (m \otimes ȷ_{i} (x_{i})) = (m \otimes x_{i})_{i} = ȷ_{i} (m \otimes x_{i})$ ; by [F5] this forces $Ψ \circ Φ = id$ . Second, $Φ \circ Ψ$ and the identity agree on every elementary tensor $m \otimes (x_{i})_{i}$ , where $Ψ$ gives the finitely supported family $(m \otimes x_{i})_{i}$ , $Φ$ sends it to $\sum_{i} (1 \otimes ȷ_{i}) (m \otimes x_{i}) = \sum_{i} m \otimes ȷ_{i} (x_{i}) = m \otimes \sum_{i} ȷ_{i} (x_{i}) = m \otimes (x_{i})_{i}$ , and $\sum_{i} ȷ_{i} (x_{i}) = (x_{i})$ ; by [F3] this forces $Φ \circ Ψ = id$ . If $I = \emptyset$ , then $⨁_{i} X_{i} = 0$ by [F4], and $M \otimes_{A} 0 = 0$ : the balanced map $τ : M \times 0 \to M \otimes_{A} 0$ is zero by [F3], so the identity and the zero endomorphism of $M \otimes_{A} 0$ , which both compose with $τ$ to $τ$ , are equal by uniqueness in [F1]; the comparison map $0 \to M \otimes_{A} 0$ is then an isomorphism.

3.1F6step 1.1step 1.4step 1.5step 2.1step 2.2∎

Assembling: $T_{M}$ is additive by step 1.1, preserves cokernels by steps 1.4 and 1.5 (so it carries the given exact sequence to the exact sequence with kernel $im (1 \otimes f)$ and surjective $1 \otimes g$ , which is right exactness in the stated sequence form), and preserves arbitrary direct sums including the empty one by step 2.2; in the bimodule case step 2.1 shows that $T_{M}$ takes values in left $B$ -modules and that all displayed maps are $B$ -linear. No element of an auxiliary family is chosen globally, so no choice is used.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Tensor-Hom adjunction for bimodules over arbitrary unital rings

Statement

Let $A$ and $B$ be unital rings, let $M$ be a $(B, A)$ -bimodule, let $X$ be a left $A$ -module and let $Y$ be a left $B$ -module. Then ${Hom}_{B} (M, Y)$ is a left $A$ -module under

$(a φ) (m) = φ (m a),$

and currying

$Θ : {Hom}_{B} (M \otimes_{A} X, Y) \to {Hom}_{A} (X, {Hom}_{B} (M, Y)), Θ (F) (x) = [m \mapsto F (m \otimes x)],$

is a bijection, natural in $X$ and $Y$ , whose inverse sends $φ$ to the $B$ -linear map determined on elementary tensors by $Ψ (φ) (m \otimes x) = φ (x) (m)$ . The unit $η_{X} : X \to {Hom}_{B} (M, M \otimes_{A} X)$ , $η_{X} (x) (m) = m \otimes x$ , and counit $ε_{Y} : M \otimes_{A} {Hom}_{B} (M, Y) \to Y$ , $ε_{Y} (m \otimes φ) = φ (m)$ , satisfy the triangle identities of Adjunction by unit, counit, and the triangle identities. Consequently $T_{M} = M \otimes_{A} -$ is left adjoint to ${Hom}_{B} (M, -)$ . No commutativity is assumed and no choice is used.

Facts & Assumptions

Given: Unital rings $A, B$ , a $(B, A)$ -bimodule $M$ , a left $A$ -module $X$ and a left $B$ -module $Y$ .

[F1]

Module laws: $m (a + a^{'}) = m a + m a^{'}$ , $(m a) a^{'} = m (a a^{'})$ , $m 1 = m$ for the right $A$ -module $M$ , and dually for left modules over $A$ and $B$ (Unital left and right modules over a ring; unqualified module means left module).

[F2]

In a $(B, A)$ -bimodule the two actions commute: $b (m a) = (b m) a$ for all $b \in B$ , $m \in M$ , $a \in A$ ( $(S, R)$ -bimodules and commuting left and right scalar actions).

[F3]

${Hom}_{B} (M, Y)$ is an abelian group under pointwise addition, and postcomposition and precomposition by module maps are group homomorphisms (The abelian group ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition).

[F4]

An $A$ -balanced map $b : M \times X \to Z$ is additive in each variable and satisfies $b (m a, x) = b (m, a x)$ (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring).

[F5]

Every balanced map $M \times X \to Z$ into an abelian group factors uniquely as $\overline{b} \circ τ$ through the universal balanced map $τ (m, x) = m \otimes x$ (Universal property of the tensor product for balanced maps into abelian groups).

[F6]

For a $(B, A)$ -bimodule $M$ and a left $A$ -module $X$ there is a unique left $B$ -module structure on $M \otimes_{A} X$ with $b (m \otimes x) = (b m) \otimes x$ (A commuting outer scalar action descends to a tensor product).

[F7]

Module maps induce maps on tensor products, functorially: $id \otimes id = id$ and $(f^{'} \circ f) \otimes (g^{'} \circ g) = (f^{'} \otimes g^{'}) \circ (f \otimes g)$ (Module homomorphisms induce tensor-product homomorphisms functorially).

[F8]

An adjunction $F ⊣ G$ is a unit and counit satisfying the triangle identities (Adjunction by unit, counit, and the triangle identities).

Proof

technique · direct

1.1F1F2F3

For $a \in A$ and $φ \in {Hom}_{B} (M, Y)$ the map $m \mapsto φ (m a)$ is additive and $B$ -linear, since $φ (b (m a)) = φ ((b m) a) = b φ (m a)$ by [F2] and $B$ -linearity of $φ$ . Hence $(a φ) (m) : = φ (m a)$ defines an element of ${Hom}_{B} (M, Y)$ , and the resulting action satisfies the left $A$ -module axioms, inherited pointwise from the right $A$ -module laws of $M$ and the group structure of ${Hom}_{B} (M, Y)$ : $(a + a^{'}) φ = a φ + a^{'} φ$ , $(a a^{'}) φ = a (a^{'} φ)$ , $1 φ = φ$ and $a (φ + ψ) = a φ + a ψ$ .

1.2F1F3F6

For $F \in {Hom}_{B} (M \otimes_{A} X, Y)$ set $Θ (F) (x) (m) : = F (m \otimes x)$ . For fixed $x$ the map $m \mapsto F (m \otimes x)$ is additive and $B$ -linear, because $b (m \otimes x) = (b m) \otimes x$ by [F6] and $F$ is $B$ -linear, so $Θ (F) (x) \in {Hom}_{B} (M, Y)$ ; moreover $Θ (F) (x + x^{'}) = Θ (F) (x) + Θ (F) (x^{'})$ and $Θ (F) (a x) = a Θ (F) (x)$ because $m \otimes (a x) = (m a) \otimes x$ , so $Θ (F) \in {Hom}_{A} (X, {Hom}_{B} (M, Y))$ , and $Θ$ is additive.

2.1F1F3F4F5F6step 1.1

For $φ \in {Hom}_{A} (X, {Hom}_{B} (M, Y))$ the pairing $u (m, x) : = φ (x) (m)$ is balanced: it is additive in each variable, and $u (m a, x) = φ (x) (m a) = (a φ (x)) (m) = φ (a x) (m) = u (m, a x)$ by step 1.1 and $A$ -linearity of $φ$ . By [F5] it induces a unique group homomorphism $Ψ (φ) : M \otimes_{A} X \to Y$ with $Ψ (φ) (m \otimes x) = φ (x) (m)$ , and $Ψ (φ)$ is $B$ -linear because $Ψ (φ) (b (m \otimes x)) = φ (x) (b m) = b (φ (x) (m))$ by [F6] and $B$ -linearity of each $φ (x)$ .

2.2F3F7step 1.2

Naturality: for $A$ -linear $g : X^{'} \to X$ one has $Θ (F \circ (1_{M} \otimes g)) (x^{'}) (m) = F (m \otimes g (x^{'})) = Θ (F) (g (x^{'})) (m)$ , so $Θ$ is natural in $X$ ; for $B$ -linear $h : Y \to Y^{'}$ one has $Θ (h \circ F) (x) (m) = h (F (m \otimes x)) = h_{*} (Θ (F) (x)) (m)$ , so $Θ$ is natural in $Y$ .

3.1F5step 1.2step 2.1

$Θ$ and $Ψ$ are mutually inverse: $Θ (Ψ (φ)) (x) (m) = Ψ (φ) (m \otimes x) = φ (x) (m)$ , and $Ψ (Θ (F))$ agrees with $F$ on every elementary tensor, so the two $B$ -linear maps are equal by the uniqueness clause of [F5].

4.1F5F7step 1.2step 2.1step 3.1

Put $η_{X} : = Θ (1_{M \otimes_{A} X})$ , so $η_{X} (x) (m) = m \otimes x$ , and $ε_{Y} : = Ψ (1_{{Hom}_{B} (M, Y)})$ , so $ε_{Y} (m \otimes φ) = φ (m)$ . The triangle identities hold: $ε_{M \otimes_{A} X} \circ (1_{M} \otimes η_{X})$ and $1_{M \otimes_{A} X}$ agree on every elementary tensor, since $ε_{M \otimes_{A} X} (m \otimes η_{X} (x)) = η_{X} (x) (m) = m \otimes x$ ; and ${Hom}_{B} (M, ε_{Y}) \circ η_{{Hom}_{B} (M, Y)}$ and the identity agree on every $φ$ , since $ε_{Y} (m \otimes φ) = φ (m)$ for all $m$ .

5.1F8step 4.1∎

By step 4.1 the functors $T_{M} = M \otimes_{A} -$ and ${Hom}_{B} (M, -)$ carry a unit and counit satisfying the triangle identities, so $T_{M}$ is left adjoint to ${Hom}_{B} (M, -)$ in the sense of [F8].

5 · Examples, counterexamples and false statements

None yet.

Eilenberg–Watts Theorem and Natural Transformations

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Additive cocontinuous module functors and their schematic category

Definition

Natural transformations of additive cocontinuous module functors are determined at the regular module

Statement

Facts & Assumptions

Proof

An additive module functor is cocontinuous exactly when it is right exact and preserves coproducts

Statement

Facts & Assumptions

Proof

F(A)F(A) is a (B,A)(B,A)-bimodule for every additive functor FF

Statement

Facts & Assumptions

Proof

The canonical comparison to the tensor functor of F(A)F(A) is balanced and natural

Statement

Facts & Assumptions

Proof

Canonical free presentations force the comparison to be an isomorphism

Statement

Facts & Assumptions

Proof

Eilenberg-Watts theorem for arbitrary unital rings

Statement

Facts & Assumptions

Proof

Natural transformations between tensor functors are bimodule maps

Statement

Facts & Assumptions

Proof

Eilenberg-Watts is a schematic equivalence of Hom categories

Statement

Facts & Assumptions

Proof

Additive cocontinuous module functors admit right adjoints

Statement

Facts & Assumptions

Proof

Exact module tensor functors correspond to right-flat bimodules

Statement

Facts & Assumptions

Proof

The functor M⊗A−M⊗A​− is additive, right exact, and preserves direct sums over an arbitrary unital ring

Statement

Facts & Assumptions

Proof

Tensor-Hom adjunction for bimodules over arbitrary unital rings

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources

$F (A)$ is a $(B, A)$ -bimodule for every additive functor $F$

The canonical comparison to the tensor functor of $F (A)$ is balanced and natural

The functor $M \otimes_{A} -$ is additive, right exact, and preserves direct sums over an arbitrary unital ring