TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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 commuting outer scalar action descends to a tensor product

Statement

Let $M$ be a right $R$ -module and let $_{R} N_{S}$ be an $(R, S)$ -bimodule. There is a unique right $S$ -module structure on $M \otimes_{R} N$ satisfying

$(m \otimes n) s = m \otimes (n s) .$

Dually, if $_{S} M_{R}$ is an $(S, R)$ -bimodule and $N$ is a left $R$ -module, there is a unique left $S$ -module structure satisfying

$s (m \otimes n) = (s m) \otimes n .$

If both outer actions are present, they commute, so the tensor product is an $(S, T)$ -bimodule in the evident handed situation.

Facts & Assumptions

Given: A right $R$ -module $M$ , an $(R, S)$ -bimodule $N$ , and, for the dual assertion, an $(S, R)$ -bimodule $M^{'}$ and a left $R$ -module $N^{'}$ .

[L1]

In a bimodule the left and right scalar actions commute: $(r n) s = r (n s)$ ( $(S, R)$ -bimodules and commuting left and right scalar actions).

[L2]

Every balanced pairing into an abelian group induces a unique homomorphism from the tensor product (Universal property of the tensor product for balanced maps into abelian groups).

[L3]

An elementary-tensor prescription descends exactly when the corresponding pairing is balanced (A formula on elementary tensors defines a homomorphism exactly when its underlying pairing is balanced).

Proof

technique · direct

1.1

For fixed $s \in S$ , the pairing $(m, n) \mapsto m \otimes (n s)$ is additive in both variables and is balanced because $(m r) \otimes (n s) = m \otimes r (n s) = m \otimes (r n) s$ by [L1].

givenL1algebra

1.2

The left-handed construction is identical: for fixed $s \in S$ , the pairing $(m^{'}, n^{'}) \mapsto (s m^{'}) \otimes n^{'}$ is balanced by the commuting actions, and the induced maps satisfy the left module laws on elementary tensors.

L1L2L3algebra

2.1

By [L2] and [L3], step 1.1 induces an additive endomorphism $x \mapsto x s$ of $M \otimes_{R} N$ with $(m \otimes n) s = m \otimes (n s)$ .

step 1.1L2L3

3.1

On every elementary tensor one has $(x (s + s^{'})) = x s + x s^{'}$ , $(x s) s^{'} = x (s s^{'})$ , and $x 1_{S} = x$ , using the right $S$ -module laws of $N$ . In each identity the two sides are additive maps that induce the same balanced pairing, so uniqueness in [L2] makes them equal on all $x$ . Thus step 2.1 defines a right $S$ -module structure.

step 2.1L2algebra

4.1

When a left $S$ -action and a right $T$ -action are both present, $s ((m \otimes n) t) = (s m) \otimes (n t) = (s (m \otimes n)) t$ on elementary tensors, so the actions commute.

step 3.1step 1.2algebra

5.1

The formulas determine every action map on generators, so uniqueness follows from [L2].

step 2.1step 1.2L2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 33 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

C. Dennis, Week 1 recap on tensor products (standard reference, not scraped)