Chapter 2. Modules (pp. 17–30)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 24 definitions, 15 propositions, 3 corollaries, 17 constructions, 1 convention and 9 other statements.
Nobody has checked this chapter against Lean yet, so the statements below say nothing about whether they are formalized.
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first for module, exact-sequence, tensor, scalar-change, flatness, and algebra interfaces. The project consumes Mathlib’s foundational algebra APIs downstream but does not own source-shaped replacements for these Chapter 2 units. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, was checked declaration-wise and compile-checked for the critical boundary interfaces. - Current/open Mathlib: upstream
29ea5de9cb981cb62dfa7979aaff0851f50c603a(Apache-2.0, Lean v4.34.0-rc2), denotedH, was refreshed 2026-09-06. Targeted current-tree and open-PR searches were used for the strict negative rows, including Hom-detection converses, arbitrary additive invariants, the concrete tensor counterexamples, and multi-tensor uniqueness. - External positive route:
EisAxelDlv00/LeanAlgebraicGeometry@f48ddbf1eb13625e8c41acbd549cc4522fb8b79f(Apache-2.0). Its Algebraic-Jacobian project pins Lean v4.31.0 and Mathlibfabf563a7c95a166b8d7b6efca11c8b4dc9d911f. The U020 theorem’s proof was independently compiled unchanged against project pinP, so the route is source-revision-specific but port-compatible with the repository baseline. The external repository’s currentHEADwas rechecked immediately before this candidate was assembled and is still exactlyf48ddbf1eb13625e8c41acbd549cc4522fb8b79f. - External negative search: targeted GitHub/indexed Lean searches found no complete owner for the seven strict negative bundles. Partial generic infrastructure is not credited when a concrete example, converse, positive-rank normalization, arbitrary invariant, or arbitrary-target uniqueness clause is missing.
Ndenotes dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant open work, installed packages, and external indexed search.
Definition: A-module
An abelian group M with scalar action A×M→M satisfying distributivity, associativity of scalar multiplication, and 1x=x; equivalently a ring homomorphism A→End(M).
Reusable comparisons: Basic module models
Ideals are A-modules; k-modules are vector spaces; Z-modules are abelian groups; k[x]-modules are vector spaces with one linear operator; k[G]-modules are representations of G (with noncommutative caveat).
Definition: A-module homomorphism / A-linear map
f:M→N is additive and satisfies f(ax)=af(x).
Construction: HomA(M,N) as an A-module
Pointwise addition and scalar multiplication make module homomorphisms M→N into Hom_A(M,N).
Construction: Precomposition and postcomposition on Hom
u:M′→M and v:N→N″ induce f↦f∘u and f↦v∘f, both A-linear.
Canonical comparison: HomA(A,M)≅M
Evaluation at 1 gives the natural isomorphism Hom_A(A,M)≅M.
Definition: Submodule
A subgroup M′⊂M closed under scalar multiplication by A.
Construction / definition: Quotient module M/M′
The quotient abelian group with a(x+M′)=ax+M′; submodules above M′ correspond order-preservingly to submodules of the quotient.
Definition: Kernel of a module homomorphism
ker f={x∈M:f(x)=0}, a submodule of M.
Definition: Image of a module homomorphism
im f=f(M), a submodule of N.
Definition: Cokernel of a module homomorphism
coker f=N/im f.
Construction / comparison: Induced quotient map and first isomorphism theorem
If M′⊆ker f, f induces M/M′→N with kernel ker f/M′; in particular M/ker f≅im f.
Construction: Sum of submodules
ΣMᵢ consists of finite-support sums and is the least submodule containing all Mᵢ.
Construction / comparison: Intersection and complete lattice of submodules
Arbitrary intersections are submodules; submodules form a complete lattice under inclusion.
Proposition 2.1: Isomorphism theorems for quotients and sums
(L/N)/(M/N)≅L/M for L⊇M⊇N; (M₁+M₂)/M₁≅M₂/(M₁∩M₂).
Construction: Ideal–module product 𝔞M
Submodule of M consisting of finite sums Σaᵢxᵢ with aᵢ∈𝔞 and xᵢ∈M.
Definition: Colon ideal (N:P)
For submodules N,P⊂M, (N:P)={a∈A:aP⊆N}, an ideal of A.
Definition: Annihilator of a module
Ann(M)=(0:M)={a∈A:aM=0}.
Construction: Descent of scalars to A/𝔞 when 𝔞 annihilates M
If 𝔞⊆Ann(M), define (x+𝔞)m=xm to make M an A/𝔞-module.
Definition: Faithful module
M is faithful iff Ann(M)=0; if Ann(M)=𝔞, M is faithful over A/𝔞.
Definition / construction: Cyclic submodule and generating set
Ax=(x) is the submodule of multiples of x; {xᵢ} generates M when M=ΣAxᵢ.
Definition: Finitely generated module
An A-module admitting a finite generating set.
Construction: Direct sum of modules
For a family (Mᵢ), ⊕Mᵢ consists of tuples with finite support, with componentwise operations.
Construction: Direct product of modules
∏Mᵢ consists of all tuples; it agrees with the direct sum for finite index sets, but generally not infinite ones.
Reusable comparison: Ring product decompositions, ideals, and idempotents
A=∏Aᵢ decomposes as a direct sum of coordinate ideals; conversely A=⊕𝔞ᵢ yields A≅∏A/𝔟ᵢ, and each 𝔞ᵢ=(eᵢ) for an idempotent identity eᵢ.
Definition: Free module
An A-module isomorphic to a direct sum of copies of A, denoted A^(I).
Convention: Finite free module notation
A finite direct sum of n copies of A is A^n; A^0 is the zero module.
Proposition 2.3: Finite generation via finite free quotient
M is finitely generated iff M is isomorphic to a quotient of A^n for some n>0.
Proposition 2.4: Determinant trick for endomorphisms
If M is finite, φ(M)⊆𝔞M, then φ satisfies a monic relation φn+a₁φ{n−1}+⋯+a_n=0 with aᵢ∈𝔞.
Corollary 2.5: Finite module with 𝔞M=M has near-1 annihilator
If 𝔞M=M, there is x≡1 mod 𝔞 with xM=0.
Proposition 2.6 (Nakayama): Nakayama lemma
For finite M and 𝔞⊆Jac(A), equality 𝔞M=M implies M=0.
Corollary 2.7: Nakayama modulo a submodule
For finite M, N⊂M and 𝔞⊆Jac(A), M=𝔞M+N implies M=N.
Construction / comparison: M/𝔪M as residue-field vector space
For local (A,𝔪) and finite M, M/𝔪M is a finite-dimensional k=A/𝔪 vector space.
Proposition 2.8: Lifting a residue-field basis to generators
If images of x₁,…,xₙ form a basis of M/𝔪M, then x₁,…,xₙ generate M.
Definition: Exact sequence
A sequence is exact at Mᵢ when im fᵢ=ker fᵢ₊₁, and exact when exact at every term.
Definition: Short exact sequence
A sequence 0→M′→M→M″→0 that is exact; any long exact sequence splits formally into such short exact pieces using images/kernels.
Proposition 2.9: Exactness detected by Hom
Right-exact M′→M→M″→0 and left-exact 0→N′→N→N″ are characterized by exactness of the induced Hom sequences for every test module.
Proposition 2.10: Kernel–cokernel exact sequence
A morphism between two short exact sequences induces the six-term exact sequence from kernels through cokernels.
Construction: Boundary homomorphism in Proposition 2.10
For x″∈ker f″, lift to x∈M, lift f(x) through u′, then take its class in coker f′.
Definition: Additive function on a class of modules
λ is additive if λ(M′)−λ(M)+λ(M″)=0 for every short exact sequence in its class.
Reusable example: Dimension is additive
For finite-dimensional k-vector spaces, V↦dim V is additive.
Proposition 2.11: Euler relation for an exact sequence
For an exact finite sequence whose terms and kernels lie in the class of an additive λ, Σ(-1)^i λ(M_i)=0.
Definition: A-bilinear map
f:M×N→P is A-linear separately in each variable.
Proposition 2.12: Tensor product universal property
There is (T,g) with g:M×N→T bilinear such that every bilinear f factors uniquely through an A-linear T→P; (T,g) is unique up to unique isomorphism.
Construction: Tensor product as a quotient of a free module
Take C=A^(M×N), quotient by the submodule generated by additivity/balance relations, and write images of basis pairs as x⊗y.
Definition / notation: Tensor product M⊗A N
The module of Proposition 2.12, generated by pure tensors x⊗y; omit A when unambiguous.
Reusable example: Pure-tensor notation depends on ambient tensor product
For 2Z⊂Z and N=Z/2Z, 2⊗x vanishes in Z⊗N but is nonzero in 2Z⊗N.
Corollary 2.13: Finite submodules witness a tensor relation
If Σxᵢ⊗yᵢ=0 in M⊗N, there are finitely generated M₀⊂M,N₀⊂N in which the same relation is already zero.
Definition / construction: Multilinear maps and multi-tensor product
Multilinear means linear in every variable; M₁⊗⋯⊗M_r is generated by x₁⊗⋯⊗x_r with the corresponding universal construction.
Proposition 2.12: Universal property of the multi-tensor product
Existence and unique-isomorphism characterization for the universal multilinear target.
Proposition 2.14: Canonical tensor isomorphisms
Canonical symmetry, associativity, distributivity over direct sum, and unit A⊗M≅M, characterized on pure tensors.
Construction: Tensor product of homomorphisms
f:M→M′ and g:N→N′ induce f⊗g with (f⊗g)(x⊗y)=f(x)⊗g(y), compatible with composition.
Construction / definition: Restriction of scalars
For f:A→B and B-module N, define a·x=f(a)x to regard N as an A-module.
Proposition 2.16: Finite generation under restriction
If N is finite over B and B finite over A, then N is finite over A.
Construction / definition: Extension of scalars
For A-module M, M_B=B⊗_A M with B-action b(b′⊗x)=bb′⊗x.
Proposition 2.17: Finite generation under extension of scalars
If M is finite over A, then B⊗_A M is finite over B.
Canonical comparison: Tensor–Hom adjunction
Hom(M⊗N,P)≅Hom(M,Hom(N,P)), naturally via bilinear maps.
Proposition 2.18: Right exactness of tensor product
If M′→M→M″→0 is exact, then M′⊗N→M⊗N→M″⊗N→0 is exact.
Reusable comparison: Adjoints and one-sided exactness
Tensoring T(M)=M⊗N is left adjoint to U(P)=Hom(N,P); the argument records that left adjoints are right exact and right adjoints left exact.
Reusable counterexample: Tensor need not preserve injections
Tensor 0→Z –×2→ Z with Z/2Z: the induced map is zero, so left exactness fails.
Definition: Flat module
N is flat when T_N:M↦M⊗_A N sends every exact sequence to an exact sequence.
Proposition 2.19: Equivalent flatness criteria
Flatness is equivalent to preservation of all short exact sequences, to preservation of injections, and it suffices to test injections between finitely generated modules.
Definition: A-algebra
A ring B together with a ring homomorphism f:A→B; scalar multiplication is ab=f(a)b.
Reusable comparisons: K-algebras and Z-algebras
For a field K and B≠0, a K-algebra identifies K with a subring of B; every ring has a canonical Z-algebra structure n↦n·1.
Definition: A-algebra homomorphism
A ring homomorphism h:B→C that is A-linear; equivalently h∘f=g for the structure maps.
Definition: Finite homomorphism / finite A-algebra
f:A→B is finite iff B is finitely generated as an A-module.
Definition: Finite type homomorphism / finitely generated A-algebra
B is generated by finitely many x_i as an A-algebra; equivalently A[t₁,…,tₙ]↠B as A-algebras.
Definition: Finitely generated ring
A ring finitely generated as a Z-algebra.
Construction: Tensor product of A-algebras
For A-algebras B,C, give D=B⊗_A C multiplication (b⊗c)(b′⊗c′)=bb′⊗cc′ and identity 1⊗1; D is an A-algebra with canonical maps such as b↦b⊗1.