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.

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.1

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}$ .

givenL1L3

1.2

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.

givenL1L2

2.1

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.

step 1.1L3

2.2

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

step 1.1L1

2.3

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].

L3L4step 1.1step 1.2

3.1

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

step 1.1step 2.1step 2.2step 1.2step 2.3∎

Depends on

Used by

Finite iterated tensor products represent multilinear maps independently of parenthesization Corollary
For flat M, one has IM∩ JM=(I∩ J)M Corollary
M⊗_RR/I≅ M/IM naturally Corollary
Tensor products commute with arbitrary direct sums Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 30 results over 13 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)