Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

Universal property of the tensor product for balanced maps into abelian groups

Statement

Let R be a unital ring, M a right R-module, N a left R-module, and

τ:M×N⟶M⊗RN,τ(m,n)=m⊗n.

The map τ is balanced (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring). For every abelian group A and every balanced map b:M×N→A, there is a unique group homomorphism

b‾:M⊗RN⟶A

such that b‾(m⊗n)=b(m,n) for all m,n. Consequently composition with τ is a bijection

Hom⁡Ab(M⊗RN,A)≅Bal⁡R(M,N;A).

Facts & Assumptions

Given: A unital ring R, a right R-module M, a left R-module N, an abelian group A, and a balanced map b:M×N→A.

[L1]

The tensor product is F/H, where F=Z(M×N), H is generated by the additivity and balance relations, and m⊗n=e(m,n)+H (The tensor product M⊗RN from the additive group underlying the free Z-module on M×N, elementary tensors, and finite tensor sums).

[L2]

A balanced map is additive in each variable and satisfies b(mr,n)=b(m,rn) (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring).

[L3]

Every element of Z(X) has a unique finite expression ∑x∈Ekxex with kx∈Z (The free module on a set and its standard basis).

[L4]

Every set map u:X→P into a left S-module extends uniquely to an S-module homomorphism S(X)→P taking ex to u(x) (Universal property of the free module on a set).

[L5]

If a group homomorphism f:G→K kills a normal subgroup H, then it factors uniquely through a group homomorphism G/H→K (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

Proof

technique · direct
1.1givenalgebra

Regard A as a Z-module by integer multiplication in its additive group. A group homomorphism between abelian groups is automatically Z-linear: additivity gives f(na)=nf(a) for n≥0, and f(−a)=−f(a) gives the formula for negative integers. Thus Z-module homomorphisms and group homomorphisms between these underlying additive groups are the same maps.

1.2L1algebra

If h:M⊗RN→A is a group homomorphism, then (m,n)↦h(m⊗n) is balanced because the elementary tensors satisfy all three relations in [L1].

2.1L3L4step 1.1

Apply [L4] at S=Z and X=M×N to extend the set map b uniquely to a Z-linear map b~:F→A satisfying b~(e(m,n))=b(m,n).

3.1L1L2step 2.1algebra

By [L2], b~ sends each generator of H to zero: the two additivity generators map respectively to b(m+m′,n)−b(m,n)−b(m′,n) and b(m,n+n′)−b(m,n)−b(m,n′), while the balance generator maps to b(mr,n)−b(m,rn). Hence H⊆ker⁡b~.

4.1L1L5step 2.1step 3.1

By [L5], b~ factors uniquely through a group homomorphism b‾:F/H=M⊗RN→A, and b‾(m⊗n)=b~(e(m,n))=b(m,n).

5.1step 4.1step 1.2L1

The operations in steps 4.1 and 1.2 are inverse: starting from b recovers its values on every pair, while starting from h produces a homomorphism agreeing with h on every elementary tensor, and those tensors generate M⊗RN. This proves both the asserted uniqueness and the displayed bijection.

6.1L1L2step 5.1∎

No selection is made in the construction. If M=0 or N=0, every balanced map out of M×N is zero and the relations make every elementary tensor zero, so the same proof gives M⊗RN=0; the zero ring is covered as well. Since a module contains its zero element, M×N is never empty, so there is no separate empty-domain case.

Depends on

Used by

…and 20 more results.

Dependency tree · two levels

17 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