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: and
Statement
Let be a unital ring. For every left -module and every right -module , the maps
and
are group isomorphisms. Their inverses are and , respectively. The maps respect every displayed outer module structure.
Facts & Assumptions
Given: A unital ring , a left -module , and a right -module .
Balanced pairings induce unique homomorphisms from tensor products (Universal property of the tensor product for balanced maps into abelian groups).
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
The pairing is additive in each variable and satisfies , so it is balanced; [L1] and [L2] give .
The pairing is balanced, so [L1] and [L2] give . Define the additive map . Then , while by balance; uniqueness in [L1] makes the second composite the identity. Thus and are inverse.
The additive map , , satisfies , while by balance. Uniqueness in [L1] makes the second composite the identity, so and are inverse.
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.
Therefore the regular module is a left and right tensor unit with the stated natural formulas.
Depends on
Used by
- Change of rings: N⊗_RM≅ N⊗_S(S⊗_RM) Corollary
- Euler characteristic in a proper flat family is locally constant Corollary
- Finite iterated tensor products represent multilinear maps independently of parenthesization Corollary
- Global functions on geometrically connected and geometrically reduced proper schemes Corollary
- M⊗_RR/I≅ M/IM naturally Corollary
- Under the stated choice boundary, free modules are projective and hence flat Corollary
- Upper semicontinuity of fibre cohomology dimensions Corollary
- Quasi-finite does not imply finite Counterexample
- Hochschild chains and Hochschild homology with coefficients Definition
- Hochschild homology of the ground field Example
- Tensoring the injection k[x] →(· x) k[x] with k[x]/(x) gives the zero map Example
- False: m⊗ n=0 implies m=0 or n=0 False statement
- False: tensoring preserves injections False statement
- Field extension preserves the graded pieces and the total length of a zero-dimensional projective quotient Lemma
- Finite-type field extensions with zero Ω Lemma
- Flat field extension commutes with coherent cohomology Lemma
- Graded associativity, units, and internal-shift tensor isomorphisms Lemma
- Hochschild chains are bar tensor chains Lemma
- Stalks, coproducts and right exactness of the abelian sheaf tensor product Lemma
- Symmetric algebras are quasi-coherent and commute with pullback Lemma
- Universal finite projective cohomology complex over any base Lemma
- Extension to the fraction field recovers the free rank of a finitely generated PID module Proposition
- Abelian groups are monoidal under the tensor product Theorem
- Cohomology and base change for proper flat coherent families Theorem
- Completion of a finite module is extension of scalars Theorem
- Direct sums and direct summands of flat modules are flat Theorem
- Every projective module over a commutative ring is flat Theorem
- Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests Theorem
- For an R-finite module over a local map, flatness modulo I and injectivity of I ⊗ M → M imply flatness Theorem
- Functoriality and coefficient long exact sequences for Hochschild homology Theorem
- Invertible fractional ideals are exactly the rank-one projective modules Theorem
- Modules over a commutative ring form a monoidal category Theorem
- Over a principal ideal domain flatness is equivalent to torsion-freeness Theorem
- The elementary tensors of two bases form the product basis of the tensor product Theorem
- The equational criterion characterizes flat modules by lifting finite relations on generators Theorem
- The ideal class group is the Picard group of rank-one projectives Theorem
- The two-sided bar complex is a projective Aᵉ-resolution Theorem
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
- Stacks Project, Section 10.12: Tensor products (standard reference, not scraped)