CorollaryStatement: 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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 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)