Alphabeta Math
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.

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

Statement

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

λN:R⊗RN⟶N,r⊗n⟼rn,

and

ρM:M⊗RR⟶M,m⊗r⟼mr,

are group isomorphisms. Their inverses are n↦1R⊗n and m↦m⊗1R, 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.1givenL1L2

The pairing (r,n)↦rn is additive in each variable and satisfies (rs)n=r(sn), so it is balanced; [L1] and [L2] give λN.

1.2L1L2algebra

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

2.1step 1.1L1algebra

The additive map ηN:N→R⊗RN, n↦1R⊗n, satisfies λNηN(n)=n, while ηNλN(r⊗n)=1R⊗rn=r⊗n by balance. Uniqueness in [L1] makes the second composite the identity, so λN and ηN are inverse.

3.1step 1.1step 2.1step 1.2algebra

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.

4.1step 2.1step 1.2step 3.1∎

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

Depends on

Used by

Dependency tree · two levels

8 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