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.

The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$

Statement

Let $R$ be a unital ring. For every left $R$ -module $N$ and every right $R$ -module $M$ , the maps

$λ_{N} : R \otimes_{R} N ⟶ N, r \otimes n ⟼ r n,$

and

$ρ_{M} : M \otimes_{R} R ⟶ M, m \otimes r ⟼ m r,$

are group isomorphisms. Their inverses are $n \mapsto 1_{R} \otimes n$ and $m \mapsto m \otimes 1_{R}$ , respectively. The maps respect every displayed outer module structure.

Facts & Assumptions

Given: A unital ring $R$ , a left $R$ -module $N$ , and a right $R$ -module $M$ .

[L1]

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

[L2]

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

The pairing $(r, n) \mapsto r n$ is additive in each variable and satisfies $(r s) n = r (s n)$ , so it is balanced; [L1] and [L2] give $λ_{N}$ .

givenL1L2

1.2

The pairing $(m, r) \mapsto m r$ is balanced, so [L1] and [L2] give $ρ_{M}$ . Define the additive map $η_{M} (m) = m \otimes 1_{R}$ . Then $ρ_{M} η_{M} (m) = m$ , while $η_{M} ρ_{M} (m \otimes r) = m r \otimes 1_{R} = m \otimes r$ by balance; uniqueness in [L1] makes the second composite the identity. Thus $ρ_{M}$ and $η_{M}$ are inverse.

L1L2algebra

2.1

The additive map $η_{N} : N \to R \otimes_{R} N$ , $n \mapsto 1_{R} \otimes n$ , satisfies $λ_{N} η_{N} (n) = n$ , while $η_{N} λ_{N} (r \otimes n) = 1_{R} \otimes r n = r \otimes n$ by balance. Uniqueness in [L1] makes the second composite the identity, so $λ_{N}$ and $η_{N}$ are inverse.

step 1.1L1algebra

3.1

Each map commutes with any outer scalar action by associativity of that action, checked on elementary tensors. The calculations remain valid for the zero ring and for zero modules, where all displayed maps are the unique maps between zero groups.

step 1.1step 2.1step 1.2algebra

4.1

Therefore the regular module is a left and right tensor unit with the stated natural formulas.

step 2.1step 1.2step 3.1∎

Depends on

Used by

Change of rings: N⊗_RM≅ N⊗_S(S⊗_RM) Corollary
Finite iterated tensor products represent multilinear maps independently of parenthesization Corollary
M⊗_RR/I≅ M/IM naturally Corollary
Under the stated choice boundary, free modules are projective and hence flat Corollary
Tensoring the injection k[x]xrightarrow· xk[x] with k[x]/(x) gives the zero map Example
False: m⊗ n=0 implies m=0 or n=0 False statement
False: tensoring preserves injections False statement
Every projective module over a commutative ring is flat Theorem
Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests Theorem
The elementary tensors of two bases form the product basis of the tensor product Theorem

Dependency tree · next 3 levels

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

The regular module is a tensor unit: R⊗RN≅NR⊗R​N≅N and M⊗RR≅MM⊗R​R≅M