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
- Complexification as ℂ⊗_ℝV with its canonical real-linear embedding Definition
- Complexification of a real-linear map Definition
- Conjugations and real structures on a complex vector space Definition
- Graded balanced tensor product and homogeneous Hom Definition
- Tensor algebra of a vector space Definition
- The tensor product of two complex representations Definition
- S⊗_RR[x]≅ S[x] as S-algebras Example
- Twists on the two-affine projective line Example
- FALSE: the left and right internal homs agree in every monoidal category False statement
- Tor one of R modulo I and M is not always the I-torsion submodule of M False statement
- A flat local map splits regular sequences into base and fibre parts Lemma
- Alternating universal property Lemma
- Dual of a line bundle is its tensor inverse Lemma
- Graded associativity, units, and internal-shift tensor isomorphisms Lemma
- Hochschild chains are bar tensor chains Lemma
- Isotypical evaluation and multiplicity subspaces Lemma
- Kähler differentials commute with scalar base change Lemma
- Projective left and right modules are flat over an arbitrary ring Lemma
- Square-zero vector extensions encode tangent vectors with coefficients Lemma
- Stalks, coproducts and right exactness of the abelian sheaf tensor product Lemma
- Symmetric algebras are quasi-coherent and commute with pullback Lemma
- The diagonal ideal modulo its square is Omega Lemma
- The sheaf attached to a module on an affine scheme Lemma
- A formula on elementary tensors defines a homomorphism exactly when its underlying pairing is balanced Proposition
- Complexification has a canonical conjugation with fixed algebra g zero Proposition
- Degree-zero Tor is the tensor product in either construction Proposition
- Direct-sum, dual, Hom, and tensor representations Proposition
- Enveloping algebra of a direct sum Proposition
- Module homomorphisms induce tensor-product homomorphisms functorially Proposition
- Positive Tor vanishes when the resolved variable is projective Proposition
- Riemannian metrics induce metrics on dual tensor and exterior bundles Proposition
- The function model of induction agrees with the tensor-product model k[G]⊗_k[H]W Remark
- A commuting outer scalar action descends to a tensor product Theorem
- A left module is flat exactly when Tor one against every right module vanishes Theorem
- A right module is flat exactly when Tor one against every left module vanishes Theorem
- Abelian groups are monoidal under the tensor product Theorem
- Associative and graded bimodule tensor–Hom adjunction Theorem
…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
- Stacks Project, Section 10.12: Tensor products (standard reference, not scraped)
- C. Dennis, Week 1 recap on tensor products (standard reference, not scraped)