TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Symmetry and associativity isomorphisms for tensor products over a commutative ring

Statement

Let $R$ be a commutative ring and let $L, M, N$ be $R$ -modules. There are natural $R$ -module isomorphisms

$σ_{M, N} : M \otimes_{R} N ⟶ N \otimes_{R} M, σ_{M, N} (m \otimes n) = n \otimes m,$

and

$α_{L, M, N} : (L \otimes_{R} M) \otimes_{R} N ⟶ L \otimes_{R} (M \otimes_{R} N), α ((l \otimes m) \otimes n) = l \otimes (m \otimes n) .$

Moreover $σ_{N, M} σ_{M, N}$ is the identity.

Facts & Assumptions

Given: A commutative ring $R$ and $R$ -modules $L, M, N$ .

[L1]

The tensor product has the $R$ -module structure $r (m \otimes n) = (r m) \otimes n = m \otimes (r n)$ (Over a commutative ring, $M \otimes_{R} N$ is an $R$ -module with $r (m \otimes n) = (r m) \otimes n = m \otimes (r n)$ ).

[L2]

Compatible bimodules have the canonical associativity isomorphism carrying $(l \otimes m) \otimes n$ to $l \otimes (m \otimes n)$ (Associativity of tensor products for compatible bimodules).

[L3]

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

[L4]

Tensor maps induced by module homomorphisms preserve identities and compositions (Module homomorphisms induce tensor-product homomorphisms functorially).

Proof

technique · direct

1.1givenL1L3

The pairing $(m, n) \mapsto n \otimes m$ is balanced because $(r m, n)$ maps to $n \otimes (r m) = (r n) \otimes m$ , which is also the image of $(m, r n)$ ; hence [L3] induces $σ_{M, N}$ .

1.2givenL1L2

Regard all three modules as $(R, R)$ -bimodules. Then [L2] supplies the displayed associativity isomorphism, and [L1] shows it is $R$ -linear on elementary tensors.

2.1step 1.1L3

Applying the same construction in the opposite order gives $σ_{N, M}$ , and their composite fixes every $m \otimes n$ ; uniqueness in [L3] makes the composite the identity, so $σ_{M, N}$ is an isomorphism.

2.2step 1.1L1

The map $σ_{M, N}$ is $R$ -linear because $σ (r (m \otimes n)) = σ ((r m) \otimes n) = n \otimes (r m) = r (n \otimes m)$ .

2.3L3L4step 1.1step 1.2

Naturality of both maps follows by applying [L4]: after replacing the variables by their images under module homomorphisms, the two candidate composites agree on every elementary tensor, hence agree by [L3].

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

Steps 1.1 through 2.3 prove the two natural $R$ -linear isomorphisms and the involutivity of symmetry.

Depends on

Used by

Dependency tree · two levels

13 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

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