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.

Associativity of tensor products for compatible bimodules

Statement

Let $M$ be a right $R$ -module, let $_{R} N_{S}$ be an $(R, S)$ -bimodule, and let $P$ be a left $S$ -module. There is a canonical group isomorphism

$α_{M, N, P} : (M \otimes_{R} N) \otimes_{S} P ⟶ M \otimes_{R} (N \otimes_{S} P)$

determined by

$α_{M, N, P} ((m \otimes n) \otimes p) = m \otimes (n \otimes p) .$

It respects any compatible outer module actions and is natural in $M, N, P$ .

Facts & Assumptions

Given: A right $R$ -module $M$ , an $(R, S)$ -bimodule $N$ , and a left $S$ -module $P$ .

[L1]

The outer actions make $M \otimes_{R} N$ a right $S$ -module and $N \otimes_{S} P$ a left $R$ -module, with the stated elementary-tensor formulas (A commuting outer scalar action descends to a tensor product).

[L2]

Balanced pairings induce unique homomorphisms from tensor products (Universal property of the tensor product for balanced maps into abelian groups).

[L3]

A formula on elementary tensors descends exactly when its underlying 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 $p \in P$ , the pairing $(m, n) \mapsto m \otimes (n \otimes p)$ is $R$ -balanced: $(m r, n)$ and $(m, r n)$ have the same image by the outer left $R$ -action in [L1]. Thus [L2] and [L3] give a homomorphism $a_{p} : M \otimes_{R} N \to M \otimes_{R} (N \otimes_{S} P)$ .

givenL1L2L3

1.2

For fixed $m \in M$ , the pairing $(n, p) \mapsto (m \otimes n) \otimes p$ is $S$ -balanced, so [L2] and [L3] give $b_{m} : N \otimes_{S} P \to (M \otimes_{R} N) \otimes_{S} P$ .

givenL1L2L3

2.1

The pairing $(x, p) \mapsto a_{p} (x)$ from $(M \otimes_{R} N) \times P$ is $S$ -balanced. On generators, $a_{p} ((m \otimes n) s) = m \otimes ((n s) \otimes p) = m \otimes (n \otimes s p) = a_{s p} (m \otimes n)$ by [L1], and additivity extends the equality to every $x$ . Hence [L2] gives $α_{M, N, P}$ with the displayed formula.

step 1.1L1L2L3

2.2

The pairing $(m, y) \mapsto b_{m} (y)$ is $R$ -balanced. It is enough to check generators $y = n \otimes p$ , where $b_{m r} (n \otimes p) = ((m r) \otimes n) \otimes p = (m \otimes r n) \otimes p = b_{m} ((r n) \otimes p) = b_{m} (r (n \otimes p))$ by [L1]. Therefore [L2] gives $β : M \otimes_{R} (N \otimes_{S} P) \to (M \otimes_{R} N) \otimes_{S} P$ .

step 1.2L1L2L3

3.1

The composite $β α$ fixes every tensor $(m \otimes n) \otimes p$ , and $α β$ fixes every tensor $m \otimes (n \otimes p)$ ; successive applications of uniqueness in [L2] show that these composites are the identity maps.

step 2.1step 2.2L2

3.2

The same elementary-tensor calculation shows compatibility with any outer actions, and replacing $m, n, p$ by their images under compatible homomorphisms proves naturality because both candidate composites agree on all elementary tensors.

step 2.1step 2.2L1L2

4.1

Thus $α_{M, N, P}$ is the asserted canonical natural isomorphism with inverse $β$ .

step 3.1step 3.2∎

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

Stacks Project, Section 10.12: Tensor products (standard reference, not scraped)