Chapter 1. Commutative rings and modules
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 21 definitions, 21 theorems, 6 lemmas, 3 corollaries, 4 examples, 4 constructions, 1 convention, 1 notation, 3 criteria and 1 other statements.
Of the 65 statements checked against Lean, 50 are formalized somewhere and 15 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 48 | 74% | Mathlib states and proves it. |
| not formalized | 15 | 23% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 2 | 3% | This repository states and proves it. |
| checked in total | 65 |
- Canonical source block: FC13 Matsumura Chapter 1,
FC13-C01-U001–FC13-C01-U065, §§1–3, in canonical source-ID order from Foundational corpus units FC13 Matsumura. The generator retrieves that promoted catalogue throughagent-memory, asserts all 65 IDs occur exactly once and in order, and emits exactly one Sweep-II route per unit. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280on Lean 4.33.0. Project files are Apache-2.0. Exact project-owned complete interfaces were found for U026 (LeanCategories/Algebra/Concrete/Rings.lean::UniqueFactorizationDomainCat) and U033 (LeanCategories/Modules/Mathlib.lean::FinitelyGeneratedModuleCat). Project wrappers that cover only one clause of a larger source bundle were not used to reclassify Mathlib theorem bundles asproject-existing. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, repositoryleanprover-community/mathlib4, Apache-2.0, Lean 4.33.0, and is directly compatible with the project. The generator verifies that the local Mathlib checkout is exactly P and that every cited pinned path and declaration token exists at P before producing the chapter record. - Current Mathlib was independently refreshed on 2026-09-07 to
H=f15b4f161f6ff698ab91b4494faa75925856d0f5, repositoryleanprover-community/mathlib4, Apache-2.0, Lean 4.34.0-rc2. Current-source inspection and open-PR searches were used especially for every pinned gap; no C01 unit receivesreference-portbecause no exact post-pin declaration was found that closes a source bundle. - Search channels: project source; pinned P; current H; open Mathlib PRs; Loogle and LeanSearch through the pinned project’s LeanSearchClient; Mathlib documentation/source; Lean Reservoir/indexed web results; and discoverable Lean repositories via GitHub code search. External results produced no compatible exact C01 package/import or reference-port route, so C01 has no
package-importroute. - Strict bundle semantics were enforced. In particular: U022 is not credited from the unit/constant-term theorem plus one-variable maximal-ideal results because the source unit is finite-multivariable; U024 is not credited from a PID-only maximal-principal theorem; U041 is not credited from finite local projective-freeness; U048 is not credited from other local length formulas; U063 is not credited merely because the theorem is derivable from lower-level annihilator/Noetherian infrastructure; and U065 is not confused with finite-type Noetherian ascent, which is the opposite direction from Eakin–Nagata.
- U040 was checked specially against its exact arbitrary-commutative-ring hypotheses. The valid pinned route is
OrzechProperty.bijective_of_surjective_endomorphismtogether with the commutative-ringOrzechPropertyinstance, not the more restrictive Noetherian Hopficity theorem. - Route totals for C01:
mathlib48,project-existing2,package-import0,reference-port0,unmatched15.
Construction: quotient-ring ideal correspondence
For I⊲A, ideals of A/I correspond bijectively to ideals J⊇I in A; under J↦J/I, (A/I)/(J/I)≅A/J, and the image/preimage formulas are f(I′)=(I+I′)/I and f⁻¹(f(I′))=I+I′.
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::relIsoOfSurjective; Mathlib/RingTheory/Ideal/Quotient/Operations.lean::comap_map_quotientMk, quotQuotEquivQuotOfLE — The surjective-map interval isomorphism gives ideals of A/I versus ideals above I; comap_map_quotientMk gives I+I′ on contraction after image, and the double-quotient equivalence is the third isomorphism theorem.
Definition: proper ideal and unit
A proper ideal is an ideal distinct from A=(1). An element a is a unit iff it has a multiplicative inverse, equivalently (a)=(1).
Formalized. Mathlib/RingTheory/Ideal/Span.lean::span_singleton_eq_top; Mathlib/Algebra/Group/Units/Defs.lean::isUnit_iff_exists_inv — Proper is I ≠ ⊤; principal ideal (a)=⊤ is equivalent to IsUnit a, and isUnit_iff_exists_inv gives the inverse criterion in the commutative-ring setting.
Lemma: unit plus nilpotent
If a is a unit and x is nilpotent, then a+x is a unit.
Formalized. Mathlib/RingTheory/Nilpotent/Basic.lean::isUnit_add_left_of_commute — IsNilpotent.isUnit_add_left_of_commute specializes in a commutative ring to a unit plus a nilpotent being a unit.
Convention: zero ring
The zero ring A=0 is allowed; it is the ring with 1=0 and hence one element.
Formalized. Mathlib/Algebra/GroupWithZero/Basic.lean::subsingleton_iff_zero_eq_one, subsingleton_of_zero_eq_one — Mathlib permits subsingleton rings; 0=1 is equivalent to subsingleton, hence to the one-element zero ring.
Definition: integral domain and field
An integral domain is a nonzero ring with no nonzero zero-divisors. A field is an integral domain in which every nonzero element is a unit; equivalently it has exactly the ideals (0),(1).
Formalized. Mathlib/Algebra/Ring/Defs.lean::class IsDomain; Mathlib/RingTheory/Ideal/Basic.lean::isField_iff_isSimpleOrder_ideal — IsDomain includes nontriviality and cancellation/no zero divisors; the field theorem identifies fields with rings whose ideal lattice has only bottom and top.
Definition: maximal ideal
A maximal ideal is maximal among proper ideals; m is maximal iff A/m is a field.
Formalized. Mathlib/RingTheory/Ideal/Quotient/Basic.lean::maximal_ideal_iff_isField_quotient — The theorem is exactly m maximal iff A ⧸ m is a field; maximality itself is the maximal proper-ideal predicate.
Theorem: Theorem 1.1
Every proper ideal I is contained in a maximal ideal.
Formalized. Mathlib/RingTheory/Ideal/Maximal.lean::exists_le_maximal — Ideal.exists_le_maximal has hypothesis I ≠ ⊤ and returns a maximal ideal containing I.
Definition: prime ideal
P is prime iff A/P is an integral domain, equivalently P≠A and xy∈P implies x∈P or y∈P. Every maximal ideal is prime.
Formalized. Mathlib/RingTheory/Ideal/Prime.lean::isPrime_iff; Mathlib/RingTheory/Ideal/Quotient/Basic.lean::isDomain_iff_prime; Mathlib/RingTheory/Ideal/Maximal.lean::IsMaximal.isPrime — These give the elementwise prime criterion, quotient-domain equivalence, and maximal-implies-prime statement with the source hypotheses.
Lemma: prime ideal absorbs ideal products
If I,J are ideals and IJ⊆P for a prime ideal P, then I⊆P or J⊆P.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::IsPrime.mul_le — Ideal.IsPrime.mul_le says I*J ≤ P forces I ≤ P ∨ J ≤ P.
Definition: multiplicative subset
A subset S⊆A is multiplicative if 1∈S and x,y∈S imply xy∈S.
Formalized. Mathlib/Algebra/Group/Submonoid/Defs.lean::structure Submonoid — Submonoid records 1 ∈ S and closure under multiplication, exactly the source multiplicative-set data.
Theorem: Theorem 1.2
If S is multiplicative and I∩S=∅, there exists a prime ideal P⊇I with P∩S=∅.
Formalized. Mathlib/RingTheory/Ideal/Maximal.lean::exists_le_prime_disjoint — For a submonoid S, disjointness from I yields a prime P ≥ I disjoint from S, exactly Theorem 1.2.
Definition: radical of an ideal
√I={a∈A | aⁿ∈I for some n>0}; it is an ideal.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::def radical, mem_radical_iff — Ideal.radical is an ideal with membership ∃ n, r^n ∈ I; allowing n=0 is harmless precisely when I=⊤, so it matches the positive-power source definition.
Theorem: radical as intersection of primes
√I is the intersection of all prime ideals containing I.
Formalized. Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean::radical_eq_sInf — Ideal.radical_eq_sInf identifies the radical with the infimum/intersection of prime ideals containing the ideal.
Definition: nilradical, reduced ring, reduction
nil(A)=√(0) is the ideal of nilpotents and the intersection of all prime ideals. A is reduced iff nil(A)=0; A_red=A/nil(A) is reduced.
Formalized. Mathlib/RingTheory/Nilpotent/Lemmas.lean::nilradical_eq_sInf, nilradical_eq_bot_iff; Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean::isRadical_iff_quotient_reduced — Mathlib identifies the nilradical with the intersection of primes and reducedness with nilradical zero; quotienting by a radical ideal is reduced, applied to the nilradical.
Definition: Jacobson radical
rad(A) is the intersection of all maximal ideals of a nonzero ring A.
Formalized. Mathlib/RingTheory/Jacobson/Ideal.lean::def jacobson, jacobson_bot — For I=⊥, Ideal.jacobson is the intersection of maximal ideals above zero, i.e. the ring Jacobson radical.
Criterion: Jacobson-radical unit criterion
x∈rad(A) iff 1+ax is a unit for every a∈A.
Formalized. Mathlib/RingTheory/Jacobson/Ideal.lean::mem_jacobson_bot — mem_jacobson_bot states membership iff x*y+1 is a unit for every y; commutativity gives the source 1+ax form.
Definition: local and semilocal rings; residue field
A local ring has one maximal ideal; a nonzero semilocal ring has finitely many. For a local ring (A,m), k=A/m is its residue field; (A,m,k) records this data.
Formalized. Mathlib/RingTheory/LocalRing/Defs.lean::class IsLocalRing; Mathlib/RingTheory/LocalProperties/Semilocal.lean::Finite (MaximalSpectrum R); Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean::def ResidueField, def residue — IsLocalRing is the unique-maximal/nonunit local structure; Mathlib encodes semilocality by finiteness of MaximalSpectrum, and ResidueField R is the quotient by the maximal ideal.
Criterion: local-ring nonunit criterion
For a local ring (A,m), A∖m is the unit group. Conversely, a nonzero ring whose nonunits form an ideal is local.
Formalized. Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean::mem_maximalIdeal; Mathlib/RingTheory/LocalRing/Basic.lean::of_nonunits_add, nonunitsAddSubmonoid — mem_maximalIdeal identifies the maximal ideal with nonunits. Conversely closure of nonunits under addition (multiplicative absorption is automatic) constructs IsLocalRing; nontriviality is the source nonzero hypothesis.
Definition: coprime ideals
Ideals I,I′ are coprime if I+I′=(1). For coprime ideals, II′=I∩I′; if I is coprime to I′ and I″ then it is coprime to I′I″.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::isCoprime_iff_sup_eq, mul_eq_inf_of_isCoprime, isCoprime_biInf — IsCoprime is sum/top; coprime product equals intersection, and isCoprime_biInf plus that equality gives coprimality with a product from coprimality with each factor.
Theorem: Theorem 1.3
For pairwise coprime ideals I₁,…,Iₙ, their product equals their intersection. In particular, for the finitely many maximal ideals of a semilocal ring, ∏mᵢ=⋂mᵢ.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::prod_eq_iInf_of_pairwise_isCoprime, isCoprime_of_isMaximal — The finite product equals finite intersection for pairwise coprime ideals. Distinct maximal ideals are coprime; semilocality supplies finiteness of the maximal spectrum, giving the stated specialization.
Theorem: Theorem 1.4 (Chinese remainder theorem)
For pairwise coprime ideals I₁,…,Iₙ, A/(I₁⋯Iₙ)≅∏ᵢA/Iᵢ.
Formalized. Mathlib/RingTheory/Ideal/Quotient/Operations.lean::quotientInfRingEquivPiQuotient — This is the finite CRT for pairwise coprime ideals; composing with product=intersection gives the source quotient by the product.
Example: formal power-series units and local rings
In AX₁,…,Xₙ, a series is a unit iff its constant term is a unit. Hence (X₁,…,Xₙ)⊆rad(AX₁,…,Xₙ); if k is a field then kX₁,…,Xₙ is local with maximal ideal (X₁,…,Xₙ).
Not formalized. Pinned/current Mathlib has MvPowerSeries.isUnit_iff_constantCoeff and local-ring instances, and the one-variable field case has PowerSeries.maximalIdeal_eq_span_X; no exact finite-multivariable declaration was found for the full (X₁,…,Xₙ) ⊆ Jac / maximal-ideal bundle. Strict bundle semantics therefore rejects the partial match.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Construction: coefficientwise quotient ideals in polynomial/power-series rings
For I⊲A, coefficientwise ideals I[X] and IX are kernels of reduction to (A/I)[X] and (A/I)X. Thus A[X]/I[X]≅(A/I)[X] and similarly for power series; if P is prime, P[X],PX are prime. For finitely generated I, IX=I·AX, while this can fail without finite generation.
Not formalized. Coefficient maps and quotient infrastructure exist, but no pinned/current/open/external declaration was found covering the coefficientwise IX kernel/quotient equivalence together with primality and the finitely-generated equality IX=I AX plus its failure without finite generation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: irreducible and prime elements
In a domain, a nonunit a is irreducible iff a=bc forces b or c a unit, equivalently (a) is maximal among proper principal ideals. It is prime iff (a) is a prime ideal; prime implies irreducible.
Not formalized. Mathlib has Irreducible, Prime, Ideal.span_singleton_prime, and Prime.irreducible, but the located maximal-principal characterization is under PID hypotheses. No exact general-domain theorem for “(a) maximal among proper principal ideals” was found, so the stronger bundle is unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: uniqueness of factorization into primes
Any two factorizations of the same element into prime elements have the same length and agree up to reordering and associates.
Formalized. Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean::factors_unique — UniqueFactorizationMonoid.factors_unique gives equality up to permutation/associates for factorizations into irreducibles/primes, hence equal lengths and the source uniqueness statement.
Definition: UFD / factorial ring
A UFD (factorial ring) is a domain in which every nonzero nonunit factors as a product of prime elements.
Formalized. LeanCategories/Algebra/Concrete/Rings.lean::UniqueFactorizationDomainCat — At project HEAD this full subcategory is exactly IsDomain R ∧ UniqueFactorizationMonoid R; pinned UniqueFactorizationMonoid.exists_prime_factors supplies the source factorization semantics, so the definition is already owned by the project.
Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280
Definition: principal ideal domain
A PID is a domain in which every ideal is principal. Every PID is a UFD; its nonzero prime ideals are generated by prime elements and are maximal.
Formalized. Mathlib/RingTheory/Ideal/Span.lean::class IsPrincipalIdealRing; Mathlib/RingTheory/PrincipalIdealDomain.lean::to_uniqueFactorizationMonoid, IsPrime.to_maximal_ideal — Mathlib’s PID assumptions are IsDomain plus IsPrincipalIdealRing; it installs UFD structure and proves every nonzero prime ideal maximal, while principality supplies a generator which is prime up to associates.
Example: polynomial UFDs
For a field k, k[X₁,…,Xₙ] is a UFD; an irreducible polynomial generates a prime ideal, which is nonmaximal when n>1.
Not formalized. Pinned Mathlib proves multivariable polynomial UFD and gives prime principal ideals from irreducibles, but no exact declaration was found for the source’s final clause that such an irreducible principal prime is nonmaximal whenever the number of variables is >1. The Krull-dimension API is adjacent but not this bundle.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Example: Z[√−5] is not a UFD
In Z[√−5], 2 is irreducible but not prime because 2·3=(1+√−5)(1−√−5); P=(2,1−√−5) is a maximal ideal containing 2.
Not formalized. Pinned/current Mathlib contains the general Zsqrtd ring but searches found no declaration formalizing this concrete factorization, irreducible-not-prime witness, and maximal ideal (2,1-√-5) bundle.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Notation: colon submodules and annihilators
For N,N′⊆M, (N:N′)={a∈A | aN′⊆N}; for I⊲A, (N:I)={x∈M | Ix⊆N}. ann(M)=(0:M); M is faithful iff ann(M)=0, and ann(x)={a | ax=0}.
Formalized. Mathlib/RingTheory/Ideal/Colon.lean::def colon, mem_colon_iff_le, bot_colon; Mathlib/RingTheory/Ideal/Maps.lean::Module.annihilator, Module.annihilator_eq_bot — Submodule.colon is exactly the scalar colon ideal; bottom-colon/annihilator gives (0:M), and annihilator_eq_bot is equivalent to faithful scalar action. Singleton colon gives element annihilators.
Construction: Hom module
Hom_A(M,M′) is an A-module under pointwise addition and scalar multiplication.
Formalized. Mathlib/Algebra/Module/LinearMap/Defs.lean::instance module — Mathlib equips linear maps M →ₗ[A] M′ with pointwise A-module structure, exactly Hom_A(M,M′).
Construction: module structures via endomorphism rings and restriction of scalars
An A-module structure on an abelian group M is equivalent to a unital ring homomorphism A→End(M). A B-module becomes an A-module along a ring map A→B by restriction of scalars.
Formalized. Mathlib/Algebra/Module/End.lean::Module.toAddMonoidEnd; Mathlib/Algebra/Module/Hom.lean::applyModule; Mathlib/Algebra/Module/RingHom.lean::Module.compHom — Module.toAddMonoidEnd is the action homomorphism into additive endomorphisms, applyModule reconstructs the action from endomorphisms, and Module.compHom restricts scalars along a ring homomorphism.
Definition: finite module
A finitely generated A-module is called a finite A-module (finite over A).
Formalized. LeanCategories/Modules/Mathlib.lean::FinitelyGeneratedModuleCat — The project full subcategory predicate is exactly Mathlib Module.Finite, i.e. finitely generated as a module; this is precisely Matsumura’s “finite module” terminology.
Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280
Theorem: Theorem 2.1 (determinant trick)
If M is generated by n elements and φ(M)⊆IM, then φ satisfies a monic relation φⁿ+a₁φⁿ⁻¹+⋯+aₙ=0 with aᵢ∈Iⁱ.
Formalized. Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean::exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero — This theorem is the determinant trick for an n-generated module stabilized into I•M: it returns a monic degree-n polynomial annihilating the endomorphism with coefficient i in the corresponding power of I.
Comparison: Cayley–Hamilton specialization
For finite free M and I=A, Theorem 2.1 specializes to Cayley–Hamilton: the characteristic polynomial of a matrix endomorphism annihilates that endomorphism.
Formalized. Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean::aeval_self_charpoly — Matrix.aeval_self_charpoly is Cayley–Hamilton; choosing a basis of a finite free module converts the source endomorphism statement to this matrix theorem.
Theorem: Theorem 2.2 (NAK)
If M is finite and M=IM, then some a≡1 mod I annihilates M. If I⊆rad(A), then M=0.
Formalized. Mathlib/RingTheory/Nakayama.lean::exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul, eq_bot_of_le_smul_of_le_jacobson_bot — The first theorem gives an element congruent to 1 modulo I annihilating the finite module under M=IM; the Jacobson-specialized theorem gives vanishing.
Corollary: Nakayama quotient form
If I⊆rad(A), M/N is finite, and M=N+IM, then M=N.
Formalized. Mathlib/RingTheory/Nakayama.lean::le_of_le_smul_of_le_jacobson_bot — Applied to the quotient/submodule formulation, this is exactly M=N+IM with finite M/N and I≤Jac implying M=N.
Definition: minimal basis of a module
A generating set W of M is a minimal basis if no proper subset generates M.
Formalized. Mathlib/Order/Defs/Unbundled.lean::def Minimal; Mathlib/LinearAlgebra/Span/Defs.lean::def span — A Matsumura minimal basis is exactly a set W satisfying Minimal (fun S => Submodule.span A S = ⊤) W; Minimal forbids a proper smaller spanning set. No linear-independence claim is built into this definition.
Theorem: Theorem 2.3 (minimal bases over a local ring)
For finite M over local (A,m,k), minimal bases of M are exactly lifts of k-bases of M/mM. Consequently all have dim_k(M/mM) elements, and transition matrices between minimal bases are invertible over A.
Not formalized. Pinned Mathlib has Nakayama lifting (exists_injOn_mkQ_image_span_eq...) and IsLocalRing.span_eq_top_of_tmul_eq_basis, but no declaration found giving the full iff with residue-field bases, cardinal invariance, and invertibility of transition matrices. The nearby finite-flat basis theorems have stronger hypotheses.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 2.4
A surjective endomorphism of a finite A-module is injective and hence an automorphism.
Formalized. Mathlib/RingTheory/OrzechProperty.lean::bijective_of_surjective_endomorphism; Mathlib/RingTheory/FiniteType.lean::CommRing.orzechProperty — Every commutative ring has OrzechProperty; its bijective_of_surjective_endomorphism applies to any finite module, exactly proving a surjective endomorphism is an automorphism without an extra Noetherian hypothesis.
Theorem: Theorem 2.5 (Kaplansky)
Every projective module over a local ring is free.
Not formalized. Pinned Mathlib proves finite flat/projective modules over local rings are free (Module.free_of_flat_of_isLocalRing), but Matsumura’s theorem has no finiteness hypothesis. Current/open/external searches found no unrestricted compatible declaration, so the finite theorem is rejected.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Lemma: Theorem 2.5, Lemma 1
If F is a direct sum of countably generated R-modules, every direct summand M of F is itself a direct sum of countably generated submodules.
Not formalized. No pinned/current/open Mathlib declaration was found stating that a direct summand of a direct sum of countably generated modules decomposes as a direct sum of countably generated submodules. External hits were not a compatible exact route.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Corollary: projectives decompose into countably generated projectives
Every projective module is a direct sum of countably generated projective modules.
Not formalized. Searches found no compatible declaration that every projective module is a direct sum of countably generated projectives; finite/projective decomposition APIs do not imply this theorem at the stated cardinal generality.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Lemma: Theorem 2.5, Lemma 2
For a projective module M over a local ring and x∈M, there is a free direct summand of M containing x.
Not formalized. No pinned/current/open/external declaration was found for an unrestricted projective module over a local ring admitting, through each element, a free direct summand. Finite local freeness is strictly weaker.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: simple module and classification
A nonzero module is simple if its only submodules are 0 and itself. The simple A-modules are exactly A/m up to isomorphism, for maximal ideals m.
Formalized. Mathlib/RingTheory/SimpleModule/Basic.lean::class IsSimpleModule, isSimpleModule_iff_quot_maximal — IsSimpleModule is the nonzero/no-proper-submodule predicate, and isSimpleModule_iff_quot_maximal classifies simple modules as quotients by maximal (left; hence ordinary in the commutative case) ideals.
Definition: composition series and length
A composition series is a finite strictly descending filtration with simple successive quotients. Its length is independent of the series; l(M) is this common length, or ∞ if no composition series exists.
Formalized. Mathlib/RingTheory/FiniteLength.lean::isFiniteLength_iff_exists_compositionSeries; Mathlib/RingTheory/Length.lean::length_compositionSeries, length_ne_top_iff — Mathlib characterizes finite length by existence of a composition series, proves every composition series has Module.length, and makes length top exactly when finite length fails.
Theorem: finite length and chain conditions
M has finite length iff its submodules satisfy both ACC and DCC. For N⊆M, l(M)=l(N)+l(M/N); finite exact sequences have vanishing alternating sum of lengths.
Formalized. Mathlib/RingTheory/FiniteLength.lean::isFiniteLength_iff_isNoetherian_isArtinian; Mathlib/RingTheory/Length.lean::length_eq_add_of_exact — Finite length is equivalent to Noetherian plus Artinian, and length is additive in short exact sequences; iterating the exact-sequence theorem gives the finite alternating-sum identity.
Lemma: finite length of A/mⁿ
If m is a finitely generated maximal ideal, then l(A/mⁿ)<∞, with l(A/mⁿ)=Σ_{i=0}^{n-1} dim_{A/m}(mⁱ/mⁱ⁺¹).
Not formalized. Length and local-ring APIs are present, but no pinned/current/open/external declaration was found for finite length of A/m^n under only finite generation of m together with the stated sum of residue-field dimensions. Stronger/special local length results do not match this unit.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: finite presentation
M is finitely presented if there is an exact sequence Aᵖ→Aᑫ→M→0; equivalently M has finitely many generators and finitely many relations.
Formalized. Mathlib/Algebra/Module/FinitePresentation.lean::class Module.FinitePresentation, exists_fin, exists_fin' — Module.FinitePresentation is finitely generated with finitely generated relation kernel; exists_fin/exists_fin' provide the finite-free presentation formulation.
Theorem: Theorem 2.6
If M is finitely presented and 0→K→N→M→0 is exact with N finitely generated, then K is finitely generated.
Formalized. Mathlib/Algebra/Module/FinitePresentation.lean::FinitePresentation.fg_ker — Module.FinitePresentation.fg_ker has a surjection from a finite module onto a finitely presented target and concludes the kernel is finitely generated, exactly Theorem 2.6.
Definition: ACC/DCC for posets
For a poset, ACC is equivalent to every nonempty subset having a maximal element; DCC is the order-dual condition. These are also called the maximal/minimal conditions.
Formalized. Mathlib/Order/OrderIsoNat.lean::wellFoundedGT_iff_monotone_chain_condition; Mathlib/Order/Minimal.lean::exists_maximal_ge_of_wellFoundedGT — Well-foundedness of > is equivalent to stabilization of monotone chains; the maximal-element theorem gives maximal points in nonempty subsets. Passing to the order dual gives DCC/minimal condition.
Definition: Noetherian and Artinian rings
A ring is Noetherian if its ideals satisfy ACC and Artinian if its ideals satisfy DCC. Quotients inherit the corresponding property.
Formalized. Mathlib/RingTheory/Noetherian/Defs.lean::IsNoetherianRing; Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_quotient; Mathlib/RingTheory/Artinian/Module.lean::isArtinian_of_quotient_of_artinian — The ring predicates are the ACC/DCC predicates for the regular module/ideal lattice; quotient module instances specialize to quotient rings and preserve the corresponding condition.
Definition: Noetherian and Artinian modules
A module is Noetherian/Artinian when its submodules satisfy ACC/DCC; submodules and quotients inherit the property.
Formalized. Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_iff_submodule_quotient; Mathlib/RingTheory/Artinian/Module.lean::isArtinian_iff_submodule_quotient — Each iff says a module has the chain condition exactly when a submodule and its quotient do, yielding both inheritance directions for submodules and quotients.
Criterion: finite-generation characterization of Noetherian objects
A ring is Noetherian iff every ideal is finitely generated. A module is Noetherian iff every submodule is finitely generated; hence finite modules over Noetherian rings are Noetherian.
Formalized. Mathlib/RingTheory/Noetherian/Defs.lean::isNoetherian_def, isNoetherianRing_iff_ideal_fg; Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_of_isNoetherianRing_of_finite — These are exactly “every submodule/ideal finitely generated” and “finite module over a Noetherian ring is Noetherian.”
Theorem: Theorem 3.1
If M′⊆M and N₁⊆N₂ have N₁∩M′=N₂∩M′ and the same image in M/M′, then N₁=N₂. Hence in 0→M′→M→M″→0, if M′ and M″ are both Noetherian (respectively Artinian), then M is; consequently finite modules over Noetherian/Artinian rings inherit the property.
Formalized. Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_of_range_eq_ker, isNoetherian_iff_submodule_quotient; Mathlib/RingTheory/Artinian/Module.lean::isArtinian_of_range_eq_ker, isArtinian_iff_submodule_quotient, isArtinian_of_fg_of_artinian — The exact-sequence theorems prove extension closure for both chain conditions; their proofs encode the source submodule intersection/image identity, and the finite-module instances give the stated Noetherian/Artinian inheritance.
Theorem: finite length iff Noetherian and Artinian
An A-module has finite length iff it is both Noetherian and Artinian.
Formalized. Mathlib/RingTheory/FiniteLength.lean::isFiniteLength_iff_isNoetherian_isArtinian — This is verbatim the source equivalence.
Example: ACC and DCC are independent for modules
Z is Noetherian but not Artinian as a Z-module; for a prime p, Z[1/p]/Z is Artinian but not Noetherian.
Not formalized. The integer module is covered by standard Noetherian infrastructure, but no pinned/current/open/external declaration was found for the Prüfer p-group presentation Z[1/p]/Z being Artinian and not Noetherian. The two-example source unit is therefore unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 3.2 (Akizuki)
Every Artinian ring is Noetherian.
Formalized. Mathlib/RingTheory/HopkinsLevitzki.lean::instIsNoetherianRingOfIsArtinianRing — Pinned Mathlib directly installs Noetherian-ring structure from Artinian-ring structure, exactly the commutative Akizuki theorem.
Lemma: structure facts used in Akizuki theorem
An Artinian ring has finitely many maximal ideals and nilpotent Jacobson radical; in particular it has finite length as a module over itself.
Formalized. Mathlib/RingTheory/Artinian/Module.lean::setOfPred_isMaximal_finite; Mathlib/RingTheory/Artinian/Ring.lean::isNilpotent_jacobson_bot; Mathlib/RingTheory/HopkinsLevitzki.lean::isArtinianRing_iff_isFiniteLength — These give finiteness of maximal ideals, nilpotence of the Jacobson radical, and finite self-length, respectively.
Theorem: Theorem 3.3 (Hilbert basis / power-series theorem)
If A is Noetherian, then both A[X] and AX are Noetherian.
Formalized. Mathlib/RingTheory/Polynomial/Basic.lean::Polynomial.isNoetherianRing; Mathlib/RingTheory/MvPowerSeries/Equiv.lean::MvPowerSeries.isNoetherianRing — The polynomial theorem is Hilbert basis. The finite-variable multivariable power-series instance specializes to one variable and proves AX Noetherian over Noetherian A.
Corollary: finite-type algebras over Noetherian rings
Every finitely generated A-algebra A[b₁,…,bₙ] over a Noetherian ring A is Noetherian.
Formalized. Mathlib/RingTheory/FiniteType.lean::Algebra.FiniteType.isNoetherianRing — A finite-type algebra over a Noetherian ring is Noetherian, exactly the finitely generated algebra corollary.
Theorem: Theorem 3.4 (I. S. Cohen)
If every prime ideal of A is finitely generated, then A is Noetherian.
Formalized. Mathlib/RingTheory/Noetherian/OfPrime.lean::IsNoetherianRing.of_prime — IsNoetherianRing.of_prime assumes every prime ideal is finitely generated and concludes the ring is Noetherian.
Theorem: Theorem 3.5
If M is a Noetherian A-module, then A/ann(M) is Noetherian; equivalently, a ring with a faithful Noetherian module is Noetherian.
Not formalized. Mathlib defines Module.annihilator, proves faithful iff annihilator is zero, and supplies the quotient-annihilator action, but searches found no pinned/current/open/external theorem with the source conclusion IsNoetherianRing (A/ann M) from IsNoetherian A M. The theorem is not credited from ingredients alone.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 3.6 (Formanek)
If B is a finite faithful A-module and the submodules IB (I⊲A) satisfy ACC, then A is Noetherian.
Not formalized. Pinned/current Mathlib, open PRs, LeanSearch/Loogle, Reservoir and indexed Lean repositories yielded no compatible theorem from ACC on the submodules I•B of a finite faithful A-module to Noetherianity of A.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 3.7 (Eakin–Nagata and variants)
If B is Noetherian and finite as a module over a commutative subring A, then A is Noetherian (Eakin–Nagata). The theorem also gives the stated noncommutative right-ideal and two-sided-ideal variants when A is commutative/central and B is finite over A.
Not formalized. No pinned/current/open/external declaration was found for descent of Noetherianity along a module-finite commutative subring, and no compatible declaration was found for the additional right-/two-sided noncommutative variants. Adjacent finite-type Noetherian ascent is the opposite direction and is rejected.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07