Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck 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×NMRN,τ(m,n)=mn.

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×NA, there is a unique group homomorphism

b:MRNA

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

HomAb(MRN,A)BalR(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×NA.

[L1]

The tensor product is F/H, where F=Z(M×N), H is generated by the additivity and balance relations, and mn=e(m,n)+H (The tensor product MRN 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 xEkxex with kxZ (The free module on a set and its standard basis).

[L4]

Every set map u:XP 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:GK kills a normal subgroup H, then it factors uniquely through a group homomorphism G/HK (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

Proof

technique · direct
1.1

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 n0, 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.

givenalgebra
1.2

If h:MRNA is a group homomorphism, then (m,n)h(mn) is balanced because the elementary tensors satisfy all three relations in [L1].

L1algebra
2.1

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

L3L4step 1.1
3.1

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 Hkerb~.

L1L2step 2.1algebra
4.1

By [L5], b~ factors uniquely through a group homomorphism b:F/H=MRNA, and b(mn)=b~(e(m,n))=b(m,n).

L1L5step 2.1step 3.1
5.1

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 MRN. This proves both the asserted uniqueness and the displayed bijection.

step 4.1step 1.2L1
6.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 MRN=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.

L1L2step 5.1

Depends on

Used by

Dependency tree · next 3 levels

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