Alphabeta MathHow 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 free module on a set
Statement
Let be a unital ring, a set, and a left -module. Every set map extends uniquely to an -module homomorphism satisfying . Explicitly,
Facts & Assumptions
Given: A set map .
is the direct sum of copies of the regular module , with standard vectors and unique finite coordinate expressions (The free module on a set and its standard basis).
A family of homomorphisms from the summands determines a unique homomorphism from their direct sum (Universal property of a direct sum of modules).
Proof
For each , define the homomorphism by .
By [L1], the family determines a unique homomorphism with .
Since , one has , and additivity gives the displayed finite-sum formula.
Any homomorphism agreeing with on every agrees with on every finite linear combination, hence on all of .
When , [F1] gives and the unique map , so no nonempty choice is hidden. The construction and uniqueness prove the universal property.
Depends on
Used by
- Every module is a quotient of a free module Corollary
- Over a Noetherian ring the homomorphism module between two finitely generated modules is finitely generated Corollary
- Finitely presented modules and finitely presented algebras Definition
- The tensor product M⊗_R N from the additive group underlying the free ℤ-module on M× N, elementary tensors, and finite tensor sums Definition
- The standard basis and a universal map from R³ Example
- For a commutative ring, Hom_R(Rⁿ,N)≅ Nⁿ Lemma
- Submodules of finite modules over a Noetherian ring are finite by induction Lemma
- Finite graded projectives are finite shifted-free summands Theorem
- Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests Theorem
- For a commutative ring R, R-linear G-actions are exactly the compatible left R[G]-module structures Theorem
- Free modules are projective, with the exact choice boundary Theorem
- Module categories have enough injectives Theorem
- Over a Noetherian ring a module is Noetherian exactly when it is finitely generated, exactly when it is finitely presented Theorem
- The elementary tensors of two bases form the product basis of the tensor product Theorem
- The free unital ring functor is left adjoint to the underlying-set functor Theorem
- The free-module functor is left adjoint to the underlying-set functor Theorem
- The group ring R[G] is a unital R-algebra with basis G, and each g∈ G is a unit of R[G] Theorem
- The matrix category is fully faithful in modules and, with chosen bases, equivalent to finite free modules Theorem
- Universal property of the tensor product for balanced maps into abelian groups Theorem
Dependency tree · two levels
5 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
- A. Kleshchev, Lectures on Abstract Algebra for Graduate Students, sections 3.6, 3.14, and 3.15 (standard reference, not scraped)
- The Stacks Project, Algebra (standard reference, not scraped)
- P. Hekmati, Homological Algebra, section 3.1 (standard reference, not scraped)