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.
Every module is a quotient of a free module
Statement
For every left -module , the free module on its underlying set admits a canonical surjection , determined by . Consequently .
Facts & Assumptions
Given: A left -module .
Every set map from a basis set to a module extends uniquely to a homomorphism from the free module (Universal property of the free module on a set).
The quotient module consists of additive cosets and carries the induced module operations (Quotient module with scalar multiplication on additive cosets).
Proof
Apply [L1] to the identity set map on the underlying set of ; this defines with .
Every equals , so is surjective, including when .
Define by . Equality of cosets makes this well defined, and [F1] makes it a homomorphism.
The map is surjective by step 2.1 and injective because exactly when . Hence it is an isomorphism.
Thus is canonically a quotient of a free module.
Depends on
Used by
- Exact finite tensor functors have projective right-module kernels Corollary
- Flat modules need not have projective dimension zero False statement
- Bilinear right exact functors are determined by their value on the regular modules Lemma
- Canonical free presentations force the comparison to be an isomorphism Lemma
- Every abelian group embeds in a divisible abelian group Lemma
- Natural transformations of additive cocontinuous module functors are determined at the regular module Lemma
- Small projective modules are exactly finitely generated projective modules; the progenerator identification Lemma
- The copower presentation construction is left adjoint to the generator Hom functor Lemma
- The iterated free-module resolution is canonical in ZF Proposition
- A short exact sequence with flat quotient remains short exact after tensoring Theorem
- Direct sums of projectives are projective, and module categories have enough projectives Theorem
- Equivalent characterizations of projective modules Theorem
- Equivalent module-theoretic characterizations of semisimple rings Theorem
- Finite abelian categories admit finite-dimensional module models Theorem
- Finite Deligne products exist via tensor-product algebras Theorem
- Finite Eilenberg–Watts for right exact linear functors Theorem
- Finitely generated modules over a left Noetherian ring are Noetherian Theorem
- Higher Tor over the integers vanishes Theorem
- Module categories have enough projectives Theorem
- The integers have global dimension one Theorem
Dependency tree · two levels
7 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)