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 be a unital ring, a right -module, a left -module, and
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 and every balanced map , there is a unique group homomorphism
such that for all . Consequently composition with is a bijection
Facts & Assumptions
Given: A unital ring , a right -module , a left -module , an abelian group , and a balanced map .
The tensor product is , where , is generated by the additivity and balance relations, and (The tensor product from the additive group underlying the free -module on , elementary tensors, and finite tensor sums).
A balanced map is additive in each variable and satisfies (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring).
Every element of has a unique finite expression with (The free module on a set and its standard basis).
Every set map into a left -module extends uniquely to an -module homomorphism taking to (Universal property of the free module on a set).
If a group homomorphism kills a normal subgroup , then it factors uniquely through a group homomorphism (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).
Proof
Regard as a -module by integer multiplication in its additive group. A group homomorphism between abelian groups is automatically -linear: additivity gives for , and gives the formula for negative integers. Thus -module homomorphisms and group homomorphisms between these underlying additive groups are the same maps.
If is a group homomorphism, then is balanced because the elementary tensors satisfy all three relations in [L1].
Apply [L4] at and to extend the set map uniquely to a -linear map satisfying .
By [L2], sends each generator of to zero: the two additivity generators map respectively to and , while the balance generator maps to . Hence .
By [L5], factors uniquely through a group homomorphism , and .
The operations in steps 4.1 and 1.2 are inverse: starting from recovers its values on every pair, while starting from produces a homomorphism agreeing with on every elementary tensor, and those tensors generate . This proves both the asserted uniqueness and the displayed bijection.
No selection is made in the construction. If or , every balanced map out of is zero and the relations make every elementary tensor zero, so the same proof gives ; the zero ring is covered as well. Since a module contains its zero element, is never empty, so there is no separate empty-domain case.
Depends on
- The tensor product $M\otimes_R N$ from the additive group underlying the free $\mathbb Z$-module on $M\times N$, elementary tensors, and finite tensor sums
- Balanced maps from a right module and a left module, and bilinear maps over a commutative ring
- The free module on a set and its standard basis
- Universal property of the free module on a set
- A homomorphism that kills a normal subgroup factors uniquely through the quotient group
Used by
- Finite iterated tensor products represent multilinear maps independently of parenthesization Corollary
- Tensor products are unique up to a unique isomorphism carrying elementary tensors to elementary tensors Corollary
- Under End_F(V)≅ V^*⊗_FV, tensor contraction is the trace Corollary
- S⊗_RR[x]≅ S[x] as S-algebras Example
- A formula on elementary tensors defines a homomorphism exactly when its underlying pairing is balanced Proposition
- Module homomorphisms induce tensor-product homomorphisms functorially Proposition
- A commuting outer scalar action descends to a tensor product Theorem
- Associativity of tensor products for compatible bimodules Theorem
- Extension of scalars is left adjoint to restriction of scalars Theorem
- For finite-dimensional V, the canonical map V^*⊗_FW toHom_F(V,W) is an isomorphism Theorem
- Hom-tensor adjunction: Hom_R(M⊗_RN,P)congHom_R(M,Hom_R(N,P)) Theorem
- Over a commutative ring, M⊗_RN is an R-module with r(m⊗ n)=(rm)⊗ n=m⊗(rn) Theorem
- Symmetry and associativity isomorphisms for tensor products over a commutative ring Theorem
- Tensor products commute with arbitrary direct sums Theorem
- Tensoring is right exact Theorem
- The character dual of a flat module is injective Theorem
- The regular module is a tensor unit: R⊗_RN≅ N and M⊗_RR≅ M Theorem
- Universal mapping property of the tensor product of commutative algebras Theorem
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
- Stacks Project, Section 10.12: Tensor products (standard reference, not scraped)
- C. Dennis, Week 1 recap on tensor products (standard reference, not scraped)