Foundational corpus mapping FC04 Atiyah Macdonald

Status: Sweep II complete. C01–C11 are complete.

Canonical catalogue: FC04 — Atiyah–Macdonald, Introduction to Commutative Algebra.

Pinned project baseline: Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Current Mathlib was refreshed 2026-09-06 to 5aedf732b6987e8c26ab3c9ebc855314f82b045f; declarations first appearing after the project pin are reference-port routes, not pinned Mathlib.

Every canonical unit receives exactly one Sweep-II route: mathlib, project-existing, package-import, reference-port, or unmatched. Project source is searched first, followed by pinned/current Mathlib, open/current work, indexed search services, Reservoir/GitHub, and relevant external Lean repositories. External routes record exact revision and compatibility; unmatched rows carry dated scoped negative evidence.

Provenance contract for C01

Chapter 1. Rings and ideals

Provenance contract for C02

Provenance contract for C07

Chapter 7. Noetherian Rings

Provenance contract for C08

Chapter 8. Artin Rings

Provenance contract for C09

Chapter 9. Discrete Valuation Rings and Dedekind Domains

Provenance contract for C10

Chapter 10. Completions

Provenance contract for C11

Chapter 11. Dimension Theory

Chapter 2. Modules

FC04 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC04-C02-U001	exact equivalence of structures	mathlib	Mathlib/Algebra/Module/End.lean::Module.toAddMonoidEnd; Mathlib/Algebra/Module/Hom.lean::AddMonoid.End.applyModule; Mathlib/Algebra/Module/RingHom.lean::Module.compHom	P	An A-module gives the source ring homomorphism into additive endomorphisms, and conversely a ring action on the underlying additive group reconstructs the module structure.
FC04-C02-U002	exact comparison bundle	mathlib	Module; LinearMap.addMonoidHomLequivInt; Module.AEval'; Rep.equivalenceModuleMonoidAlgebra	P	The pinned APIs realize all source models: ideals/modules, vector spaces, abelian groups as ℤ-modules, polynomial-module actions from an endomorphism, and group-algebra modules as representations.
FC04-C02-U003	exact structure	mathlib	Mathlib/Algebra/Module/LinearMap/Defs.lean::LinearMap	P	A bundled linear map preserves addition and scalar multiplication exactly as in the source.
FC04-C02-U004	exact module structure	mathlib	Mathlib/Algebra/Module/LinearMap/Defs.lean; module instance on M →ₗ[A] N	P	Pointwise addition and scalar multiplication give Hom_A(M,N) its canonical A-module structure.
FC04-C02-U005	exact constructions	mathlib	LinearMap.lcomp; LinearMap.compRight	P	Pre- and postcomposition are bundled linear maps on Hom modules with the source formulas.
FC04-C02-U006	exact equivalence	mathlib	Mathlib/Algebra/Module/Equiv/Basic.lean::LinearMap.ringLmapEquivSelf	P	Evaluation at 1 is the linear equivalence Hom_A(A,M) ≃ M, with inverse m ↦ (a ↦ a • m).
FC04-C02-U007	exact structure	mathlib	Mathlib/Algebra/Module/Submodule/Defs.lean::Submodule	P	A Submodule A M is exactly an additive subgroup stable under scalar multiplication.
FC04-C02-U008	exact quotient correspondence	mathlib	Mathlib/LinearAlgebra/Quotient/Basic.lean::Submodule.comapMkQRelIso; Submodule.Quotient	P	The quotient module is bundled and submodules of M/N correspond order-isomorphically to submodules of M containing N.
FC04-C02-U009	exact construction	mathlib	Mathlib/Algebra/Module/Submodule/LinearMap.lean::LinearMap.ker	P	The kernel is the submodule of elements mapped to zero.
FC04-C02-U010	exact construction	mathlib	Mathlib/Algebra/Module/Submodule/LinearMap.lean::LinearMap.range	P	The image/range is a submodule with the expected membership characterization.
FC04-C02-U011	exact cokernel comparison	mathlib	Mathlib/Algebra/Category/ModuleCat/Kernels.lean::ModuleCat.cokernelIsoRangeQuotient; cokernel_π_cokernelIsoRangeQuotient_hom	P	The categorical cokernel is identified with the target quotient by the image, and the cokernel projection is the quotient map.
FC04-C02-U012	exact induced map and first isomorphism	mathlib	Submodule.liftQ; Submodule.ker_liftQ; Mathlib/LinearAlgebra/Isomorphisms.lean::LinearMap.quotKerEquivRange	P	A map killing a submodule factors through the quotient with the expected kernel, and M/ker f ≃ range f gives the first isomorphism theorem.
FC04-C02-U013	exact construction	mathlib	Submodule.iSup; Submodule.mem_iSup_iff_exists_finsupp; iSup_eq_range_dfinsupp_lsum	P	The supremum is the least submodule containing the family; membership is represented by a finite-support sum, exactly the source sum of submodules.
FC04-C02-U014	exact lattice structure	mathlib	Mathlib/Algebra/Module/Submodule/Lattice.lean; Submodule.mem_iInf	P	Submodules form a complete lattice; infima are intersections and suprema are generated sums.
FC04-C02-U015	exact isomorphism theorems	mathlib	Mathlib/LinearAlgebra/Isomorphisms.lean::Submodule.quotientInfEquivSupQuotient; Submodule.quotientQuotientEquivQuotient	P	These are the second/third module isomorphism laws; the remaining displayed form follows by symmetry/relabeling.
FC04-C02-U016	exact construction	mathlib	ideal action I • N; Submodule.mem_ideal_smul_span_iff_exists_sum	P	Ideal multiplication on a module is the submodule of finite sums of aᵢ • xᵢ, matching aM.
FC04-C02-U017	exact definition	mathlib	Mathlib/RingTheory/Ideal/Colon.lean::Submodule.colon; mem_colon; mem_colon_iff_le	P	The colon ideal consists exactly of scalars sending P into N.
FC04-C02-U018	exact definition	mathlib	Mathlib/RingTheory/Ideal/Maps.lean::Module.annihilator; Module.mem_annihilator	P	The annihilator is exactly the ideal of scalars killing every element of the module.
FC04-C02-U019	exact quotient scalar action	mathlib	Module.isTorsionBySet_iff_subset_annihilator; Module.IsTorsionBySet.module; Module.IsTorsionBySet.mk_smul	P	If I ≤ Ann(M), Mathlib constructs the A/I-module structure on M, with quotient classes acting through representatives.
FC04-C02-U020	revision-specific external theorem	reference-port	AxelDlv00/LeanAlgebraicGeometry@f48ddbf1eb13625e8c41acbd549cc4522fb8b79f::MainProjects/Algebraic-Jacobian-Challenge/AlgebraicJacobian/Picard/SchematicSupport.lean::AlgebraicGeometry.faithfulSMul_quotientAnnihilator	E	Pinned Mathlib has Module.annihilator_eq_bot and the canonical quotient-annihilator action but no packaged quotient-faithfulness theorem. The external theorem proves exactly FaithfulSMul (A/Ann(M)) M; its proof was independently compiled unchanged against P. Source project: Apache-2.0, Lean 4.31.0, Mathlib fabf563a7c95a166b8d7b6efca11c8b4dc9d911f.
FC04-C02-U021	exact construction	mathlib	cyclic submodule A ∙ x; Submodule.span_range_eq_iSup	P	A cyclic submodule is the span of one element, and a generating family expresses the module as the supremum/sum of its cyclic submodules.
FC04-C02-U022	exact definition	mathlib	Mathlib/RingTheory/Finiteness/Defs.lean::Module.Finite; Module.finite_def; Module.Finite.exists_fin	P	Module.Finite is finite generation of the top submodule, equivalently a finite generating family.
FC04-C02-U023	exact construction	mathlib	DirectSum; DFinsupp; Mathlib/Algebra/DirectSum/Basic.lean::DirectSum.hasFiniteSupport	P	The direct sum is the finite-support dependent function module with the canonical inclusions and universal finite-support behavior.
FC04-C02-U024	exact comparison	mathlib	Pi module structure; DirectSum.linearEquivFunOnFintype; DirectSum.hasFiniteSupport	P	For finite index sets the direct sum is linearly equivalent to the product; for arbitrary indices direct-sum elements have finite support, distinguishing it from unrestricted products.
FC04-C02-U025	exact decomposition bundle	mathlib	CompleteOrthogonalIdempotents.single; CompleteOrthogonalIdempotents.bijective_pi; DirectSum.idempotent; DirectSum.decompose_eq_mul_idempotent; DirectSum.completeOrthogonalIdempotents_idempotent	P	Pinned Mathlib realizes finite product ideals and the equivalent complete orthogonal-idempotent decomposition, including recovery of summands as principal idempotent ideals.
FC04-C02-U026	exact structure	mathlib	Mathlib/LinearAlgebra/FreeModule/Basic.lean::Module.free_def; Module.Free.chooseBasis; Basis.repr	P	A free module has a basis and is linearly equivalent to a finitely supported direct sum of copies of the base ring.
FC04-C02-U027	exact finite-free model	mathlib	Module.Free.ChooseBasisIndex.fintype; Basis.repr; Finsupp.linearEquivFunOnFinite; Basis.empty	P	Finite free modules identify with A^n; the empty basis gives the zero module at n=0.
FC04-C02-U028	unmatched positive-rank normalization	unmatched	partial: Module.Finite.exists_fin'; Module.Finite.exists_fin_quot_equiv; Module.Finite.of_surjective	N	P/H package finite generation exactly as a quotient of A^n, but only for n : ℕ; no checked declaration supplies the source bundle’s explicit n>0 normalization. Targeted current/open/external search found no exported positive-rank wrapper.
FC04-C02-U029	exact stronger theorem	mathlib	Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean::LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero	P	This is the determinant trick and is stronger than the source: the characteristic coefficients lie in the corresponding powers of the ideal.
FC04-C02-U030	exact corollary	mathlib	Mathlib/RingTheory/Finiteness/Nakayama.lean::Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul	P	From finite generation and M ≤ I • M, it produces an element congruent to 1 modulo I that annihilates the module.
FC04-C02-U031	exact theorem	mathlib	Mathlib/RingTheory/Nakayama.lean::Submodule.eq_bot_of_le_smul_of_le_jacobson_bot	P	This is Nakayama in the source form: finite generation plus I ≤ Jac(A) and M = IM forces M=0.
FC04-C02-U032	exact theorem	mathlib	Mathlib/RingTheory/Nakayama.lean::Submodule.le_of_le_smul_of_le_jacobson_bot	P	The quotient/submodule Nakayama form specializes to M = IM + N ⇒ M=N.
FC04-C02-U033	exact finite residue-field module	mathlib	quotient-module instance in Mathlib/Algebra/Module/Torsion/Basic.lean; Module.Finite.of_restrictScalars_finite	P	For finite M, M/(𝔪M) is finite over A/𝔪; when 𝔪 is maximal this is a finite-dimensional residue-field vector space.
FC04-C02-U034	exact lifting theorem	mathlib	Mathlib/RingTheory/LocalRing/Module.lean::IsLocalRing.map_mkQ_eq_top; IsLocalRing.span_eq_top_of_tmul_eq_basis	P	A family whose residue classes span (in particular form a basis of) M/𝔪M lifts to generators of the finite module.
FC04-C02-U035	exact sequence formalism	mathlib	Mathlib/Algebra/Homology/ExactSequence.lean::ComposableArrows.Exact; ShortComplex.moduleCat_exact_iff_range_eq_ker	P	Exactness of a module sequence is exactly equality of image and kernel at every consecutive pair.
FC04-C02-U036	exact short-exact formalism and decomposition	mathlib	Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean::ShortComplex.ShortExact; ShortComplex.Exact.shortExact	P	ShortExact is exactness plus mono/epi; Exact.shortExact packages each consecutive image/kernel piece into the standard short exact sequence, realizing the formal decomposition used for long exact sequences.
FC04-C02-U037	unmatched converse criterion	unmatched	partial: Mathlib/LinearAlgebra/LeftExact.lean::LinearMap.exact_lcomp_of_exact_of_surjective; ShortComplex.exact_map_iff_of_faithful	N	P/H contain the forward Hom-exactness implications and generic faithful-functor reflection, but no checked declaration realizes both source converses detecting right/left exactness from all Hom tests.
FC04-C02-U038	exact six-term sequence	mathlib	Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean::ShortComplex.SnakeInput.composableArrows; SnakeInput.snake_lemma	P	The snake construction gives the exact six-term sequence from kernels through cokernels for a morphism of short exact sequences.
FC04-C02-U039	exact boundary construction	mathlib	Mathlib/Algebra/Module/SnakeLemma.lean::SnakeLemma.δ'; SnakeLemma.δ'_eq	P	The module-level connecting map is characterized by exactly the lift–map–lift–cokernel-class recipe in the source.
FC04-C02-U040	unmatched abstraction	unmatched	partial: short-exact formalism; finrank additivity theorems	N	No checked P/H or external declaration defines an arbitrary additive function on a class of modules by the short-exact relation λ(M')-λ(M)+λ(M'')=0.
FC04-C02-U041	exact example	mathlib	Mathlib/Algebra/Exact/Sequence.lean::Module.sum_neg_one_pow_finrank_eq_zero_of_exact	P	Specializing the finite exact-sequence Euler formula to a short exact sequence gives additivity of vector-space dimension.
FC04-C02-U042	unmatched arbitrary-invariant theorem	unmatched	partial: Module.sum_neg_one_pow_finrank_eq_zero_of_exact; current Algebra/Homology/EulerCharacteristic.lean	N	P/H prove the Euler relation for finrank, but no checked theorem derives it for an arbitrary source-style additive invariant λ.
FC04-C02-U043	exact definition	mathlib	Mathlib/LinearAlgebra/BilinearMap.lean::LinearMap.mk₂; LinearMap.mk₂_apply; IsBilinearMap	P	These interfaces encode separate A-linearity in the two arguments.
FC04-C02-U044	exact universal property	mathlib	Mathlib/LinearAlgebra/TensorProduct/Basic.lean::TensorProduct.lift; lift.unique; Mathlib/RingTheory/IsTensorProduct.lean::IsTensorProduct.equiv	P	The canonical tensor product represents bilinear maps, and IsTensorProduct.equiv gives uniqueness of any other binary universal target up to linear equivalence.
FC04-C02-U045	exact construction	mathlib	Mathlib/LinearAlgebra/TensorProduct/Defs.lean::TensorProduct.Eqv; TensorProduct.tmul	P	Mathlib constructs the tensor product as a quotient by the additivity and balancing relations; the implementation uses a free-additive-monoid congruence rather than literally a free-module quotient but realizes the same presentation.
FC04-C02-U046	exact notation and generation	mathlib	TensorProduct.tmul; TensorProduct.span_tmul_eq_top	P	Pure tensors are the canonical generators and span the tensor product.
FC04-C02-U047	unmatched concrete example	unmatched	partial: general tensor/quotient APIs	N	No checked P/H, open-work, or external Lean declaration realizes the source example 2ℤ ⊂ ℤ, N=ℤ/2ℤ with the same pure tensor zero in the ambient tensor product but nonzero in the smaller one.
FC04-C02-U048	exact finite witness theorem	mathlib	Mathlib/RingTheory/TensorProduct/DirectLimitFG.lean::TensorProduct.exists_of_fg; TensorProduct.eq_zero_of_fg_of_subtype_eq_zero	P	The direct-limit theorem enlarges a finitely generated submodule until an ambient zero relation already vanishes there; applying it in the two factors gives finitely generated M₀,N₀ carrying the same finite relation.
FC04-C02-U049	exact multi-tensor construction	mathlib	Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean::PiTensorProduct.tprod; PiTensorProduct.lift	P	The dependent Pi tensor product represents multilinear maps for an arbitrary index type, stronger than the source finite-arity construction.
FC04-C02-U050	unmatched arbitrary-target characterization	unmatched	partial: PiTensorProduct.lift; PiTensorProduct.lift.unique	N	The canonical multi-tensor universal property is formalized, but P/H and targeted external search have no IsPiTensorProduct-type theorem showing every arbitrary universal multilinear target is uniquely isomorphic to it.
FC04-C02-U051	exact canonical isomorphisms	mathlib	TensorProduct.comm; TensorProduct.assoc; TensorProduct.lid; TensorProduct.rid; TensorProduct.directSumLeft; TensorProduct.directSumRight	P	Pinned equivalences give symmetry, associativity, unit, and distributivity over direct sums with the expected pure-tensor formulas.
FC04-C02-U052	exact functorial construction	mathlib	Mathlib/LinearAlgebra/TensorProduct/Map.lean::TensorProduct.map; map_tmul; map_comp	P	The induced map is exactly x⊗y ↦ f(x)⊗g(y) and is compatible with composition.
FC04-C02-U053	exact construction	mathlib	Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean::ModuleCat.restrictScalars	P	Restriction of scalars along a ring map uses the source action a • n = f(a) • n.
FC04-C02-U054	exact theorem	mathlib	Mathlib/RingTheory/Finiteness/Basic.lean::Module.Finite.trans	P	Finite over B and B finite over A imply finite over A.
FC04-C02-U055	exact construction	mathlib	Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean::ModuleCat.extendScalars; ModuleCat.ExtendScalars.smul_tmul	P	Extension of scalars is B ⊗_A M, and the displayed B-action on pure tensors is exactly the source formula.
FC04-C02-U056	exact theorem	mathlib	Mathlib/RingTheory/TensorProduct/Finite.lean::Module.Finite.base_change	P	Finite generation is preserved by extension of scalars.
FC04-C02-U057	exact adjunction	mathlib	Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean::ModuleCat.monoidalClosedHomEquiv	P	The closed monoidal Hom equivalence is the tensor–Hom adjunction; tensor symmetry switches to the source ordering.
FC04-C02-U058	exact right-exactness	mathlib	Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean::LinearMap.lTensor_surjective; lTensor_exact; rTensor_exact; right-hand surjectivity analogue	P	Tensoring preserves the exact pair and terminal surjection, exactly right exactness.
FC04-C02-U059	exact adjoint exactness consequences	mathlib	U057; Mathlib/CategoryTheory/Adjunction/Limits.lean::Adjunction.leftAdjoint_preservesColimits; rightAdjoint_preservesLimits; rightExactFunctor_iff; leftExactFunctor_iff	P	The tensor functor is a left adjoint and Hom is a right adjoint, yielding the source one-sided exactness statements.
FC04-C02-U060	unmatched concrete counterexample	unmatched	partial: tensor right-exactness and ZMod quotient APIs	N	No checked P/H, open-work, or external declaration packages the explicit sequence 0→ℤ --×2→ ℤ becoming noninjective after tensoring with ℤ/2ℤ.
FC04-C02-U061	exact equivalent definition	mathlib	Mathlib/RingTheory/Flat/Basic.lean::Module.Flat.iff_lTensor_exact; iff_rTensor_exact; Mathlib/RingTheory/Flat/CategoryTheory.lean	P	Although Module.Flat is encoded via injection preservation, pinned theorems prove equivalence with tensor preserving exact sequences, exactly the source definition.
FC04-C02-U062	exact criterion bundle	mathlib	Module.Flat; Module.Flat.iff_lTensor_preserves_injective_linearMap; iff_rTensor_preserves_injective_linearMap; iff_lTensor_exact; iff_rTensor_exact	P	The defining FG-submodule test and the global injection/exactness equivalences realize the source flatness criteria, including sufficiency of finitely generated tests.
FC04-C02-U063	exact structure	mathlib	Mathlib/Algebra/Algebra/Defs.lean::Algebra	P	An algebra is a ring/semiring equipped with a central structure map, and smul_def' identifies scalar multiplication with multiplication by its image.
FC04-C02-U064	exact comparison bundle	mathlib	Mathlib/RingTheory/SimpleRing/Basic.lean::RingHom.injective; Mathlib/Algebra/Algebra/Basic.lean::Ring.toIntAlgebra	P	A field structure map into a nontrivial algebra is injective, and every ring has its canonical ℤ-algebra structure.
FC04-C02-U065	exact structure characterization	mathlib	Mathlib/Algebra/Algebra/Hom.lean::AlgHom; AlgHomClass.linearMapClass; AlgHom.mk'	P	An algebra homomorphism is a ring homomorphism commuting with the structure maps; pinned coercions/constructors identify this with A-linearity.
FC04-C02-U066	exact definition	mathlib	Mathlib/RingTheory/Finiteness/Defs.lean::RingHom.Finite; finite_algebraMap	P	A ring map is finite exactly when its target is finite as a module over the source.
FC04-C02-U067	exact definition and presentation theorem	mathlib	Mathlib/RingTheory/FiniteType.lean::Algebra.FiniteType; Algebra.FiniteType.iff_quotient_mvPolynomial''	P	Finite type means finitely generated as an algebra and is equivalent to a surjection from a polynomial algebra in finitely many variables.
FC04-C02-U068	exact equivalent encoding	mathlib	Ring.toIntAlgebra; Algebra.FiniteType ℤ B	P	The source notion of a finitely generated ring is exactly finite type for the canonical ℤ-algebra structure.
FC04-C02-U069	exact algebra tensor construction	mathlib	Mathlib/RingTheory/TensorProduct/Basic.lean::Algebra.TensorProduct.one_def; tmul_mul_tmul; includeLeft; includeRight	P	The tensor product carries the source multiplication and unit and the two canonical algebra maps from its factors.

Provenance contract for C03

Chapter 3. Rings and Modules of Fractions; Local Properties

Provenance contract for C04

Chapter 4. Primary Decomposition

Provenance contract for C05

Chapter 5. Integral Dependence and Valuations

Provenance contract for C06

Chapter 6. Chain Conditions