Chapter 6. Regular sequences
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 14 definitions, 30 theorems, 1 proposition, 6 lemmas, 3 corollaries, 2 examples, 1 counterexample, 3 constructions, 1 remark and 1 criterion.
Of the 62 statements checked against Lean, 20 are formalized somewhere and 42 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 42 | 68% | A documented search found no Lean statement of it anywhere. |
| in another Lean project | 16 | 26% | Some other Lean development has it; using it means porting that code. |
| in Mathlib | 4 | 6% | Mathlib states and proves it. |
| checked in total | 62 |
- Canonical source block: FC13 Matsumura Chapter 6,
FC13-C06-U001–FC13-C06-U062, §§16–18, in canonical source-ID order from Foundational corpus units FC13 Matsumura. The generator retrieves the promoted catalogue throughagent-memory, verifies all 62 IDs and emits exactly one route per unit. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280(Lean 4.33.0, Apache-2.0). No project-owned wrapper covers a complete C06 unit beyond pinned Mathlib/open upstream developments, so C06 has noproject-existingroute. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Apache-2.0, Lean 4.33.0. Native coverage includesSequence.IsRegular, the pinned Rees Ext/regular-sequence TFAE, and localization of injective modules. P explicitly lists Koszul and quasi-regular sequence theory as TODOs inRegularSequence.lean; those gaps are not papered over by generic homological-complex APIs. - Current Mathlib was refreshed 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493(Lean 4.34.0-rc2). The major exact post-pin owners are still open PRs: #26218 (2a84ea75981e352045999fd11bc7ef6b8fab549f) for depth/Ischebeck/CM definitions and localization; #26245 (22bda9222808563de469a721b6f306abe18ebde5) for CM height/depth/catenary formulas; #26957 (cb58875d409523d7f9fe40519e8aec70c59855a4) for unmixedness; #28599 (fb96036190226357c7ee4450b46e9419df085bc5) for polynomial CM; and the Gorenstein stack #31884/#32035/#41102 for definitions, localization and completion. These arereference-portroutes, not package imports. - Search channels used project source, P, current/open Mathlib, Mathlib source/docs, Loogle/LeanSearch-oriented repository tooling, Reservoir/indexed discovery, and GitHub-wide Lean-code search. Targeted searches for Koszul, quasi-regular sequences, CM completion/power series, injective hulls, Matlis duality, Bass numbers, and big CM found no complete compatible owner beyond the specific PRs recorded. PR #34913 (
c7780ed427bbed31ee0c430a5594ed5ea4c7d5b5) supplies a substantial ring-valued Koszul complex, append exact sequence, annihilator homotopy, and regular-sequence acyclicity, but not Matsumura’s arbitrary coefficient-module/general-complex/converse bundles U010–U014. - Strict bundle semantics were enforced. U008 is not credited from the narrower pinned permutation theorem without Matsumura’s quasi-regular/separated bridge; U021 is not credited from constituent depth/height/projective-dimension facts without the full grade relation bundle; U028 is not credited from regular-sequence height criteria without the parameter-system theorem; U044 is not credited from Gorenstein definitions and Ext lemmas without the full eight-way Theorem 18.1 equivalence; and Matlis/Bass rows U050–U059 remain unmatched without an injective-hull framework.
- Gorenstein terminology is routed only after the source Theorem 18.1 row: PR #31884 selects finite self-injective dimension as the standard equivalent definition, PR #32035 proves prime-local stability, and PR #41102 proves completion invariance. The large source equivalence U044 itself remains unmatched because the open stack does not package all irreducible-parameter-ideal clauses.
- Route totals for C06:
mathlib4,project-existing0,package-import0,reference-port16,unmatched42.
Definition: M-regular element and M-sequence
An element a∈A is M-regular if ax≠0 for every nonzero x∈M. A sequence a_1,…,a_n is M-regular when each a_i is regular on M/(a_1,…,a_{i-1})M and M≠(a_1,…,a_n)M.
Formalized. Mathlib/RingTheory/Regular/IsSMulRegular.lean::IsSMulRegular; Mathlib/RingTheory/Regular/RegularSequence.lean::IsRegular, isRegular_iff — IsSMulRegular M a is injectivity of multiplication by a; Sequence.IsRegular M rs is exactly successive regularity on the quotient by earlier terms together with the final nontriviality condition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 16.1
Positive powers of an M-sequence again form an M-sequence: if a_1,…,a_n is M-regular, then a_1{v_1},…,a_n{v_n} is M-regular for all v_i>0.
Not formalized. Pinned Mathlib proves IsRegular.pow for one regular element, but no checked declaration sends an arbitrary module-regular sequence to arbitrary componentwise positive powers. Current/open/external search found no source-shaped theorem.
Construction: polynomial modules and substitution
Write M[X_1,…,X_n]=M⊗_A A[X_1,…,X_n]; polynomials with coefficients in M admit substitution X_i↦a_i∈A.
Not formalized. Tensor products and multivariate polynomial evaluation are available separately, but no checked declaration packages M[X_1,…,X_n]=M⊗A[X] as coefficient polynomials in M together with the source substitution map.
Definition: M-quasi-regular sequence
For I=(a_1,…,a_n) with IM≠M, the sequence is M-quasi-regular if every homogeneous F of degree v with F(a)∈I^{v+1}M has all coefficients in IM.
Not formalized. Pinned/current Mathlib explicitly lists quasi-regular sequences among the TODOs of RegularSequence.lean; no compatible external completed owner was found.
Criterion: associated-graded criterion for quasi-regularity
The canonical graded surjection (M/IM)[X_1,…,X_n]→gr_I(M), X_i↦a_i, is an isomorphism exactly when a_1,…,a_n is M-quasi-regular.
Not formalized. Pinned/current Mathlib explicitly lists quasi-regular sequences among the TODOs of RegularSequence.lean; no compatible external completed owner was found.
Theorem: Theorem 16.2
Every M-sequence is M-quasi-regular. For an M-quasi-regular sequence generating I, if IM:x=IM then IvM:x=IvM for every v>0.
Not formalized. Pinned/current Mathlib explicitly lists quasi-regular sequences among the TODOs of RegularSequence.lean; no compatible external completed owner was found.
Theorem: Theorem 16.3
For Noetherian A and M≠0, if the successive quotients by a_1,…,a_n are I-adically separated, then an M-quasi-regular sequence is M-regular. The hypothesis holds for finite M with I⊆rad A and in the stated positive-degree graded case.
Not formalized. Pinned/current Mathlib explicitly lists quasi-regular sequences among the TODOs of RegularSequence.lean; no compatible external completed owner was found.
Corollary: permutation invariance under separatedness hypotheses
Under either hypothesis of Theorem 16.3, every permutation of an M-sequence is again an M-sequence.
Not formalized. Pinned Mathlib proves permutation invariance under Noetherian/Jacobson-annihilator hypotheses (IsLocalRing.isRegular_of_perm and related lemmas), but Matsumura’s row bundles the broader separated and graded hypotheses coming from quasi-regularity. Without the missing quasi-regular bridge, the source corollary is not a whole-row match.
Counterexample: regular sequences need not be permutation invariant in general
The source gives A=k[X,Y,Z] and a specific A-sequence whose permutation is not an A-sequence.
Not formalized. No checked declaration owns the displayed k[X,Y,Z] counterexample as a reusable theorem/example.
Construction: Koszul complex
For x_1,…,x_n∈A, K_•(x) has K_p free on p-element subsets and differential d(e_{i_1…i_p})=Σ_r(-1)^{r-1}x_{i_r}e_{i_1…hat{i_r}…i_p}. Put K_•(x,M)=K_•(x)⊗M; tensor products identify K(x_1,…,x_n) with the tensor of the one-variable complexes, hence it is permutation invariant up to isomorphism.
Not formalized. Open Mathlib PR #34913 defines the ring-valued Koszul complex koszulComplex.ofList, exterior-power differential, base change, and append decomposition. Matsumura U010 also includes K(x,M)=K(x)⊗M for an arbitrary A-module M and its tensor-product/permutation package; no compatible declaration for that coefficient-module bundle was found, so the whole row remains unmatched.
Construction: Koszul homology
H_p(x,M) denotes the homology of K_•(x,M); H_0(x,M)=M/(x)M and H_n(x,M) is the common annihilator of the x_i on M.
Not formalized. PR #34913 defines homology of the ring-valued Koszul complex and zeroHomologyOfListLinearEquiv, giving H₀=A/(x). It does not export the source arbitrary-module homology H_p(x,M) nor the top-homology/common-annihilator formula for M, so the row is only partially covered.
Theorem: Theorem 16.4
For a complex C_• and x∈A there is a short exact sequence of complexes 0→C_•→C_•(x)→C_•[1]→0, with the resulting homology long exact sequence; multiplication by x annihilates H_p(C_•(x)).
Not formalized. PR #34913 proves koszulComplex.shortComplexProd_shortExact and the connecting-map formula for adjoining one Koszul generator, and the homotopy file proves generator multiplication is null-homotopic. Matsumura states the construction for an arbitrary complex C together with the resulting long exact homology sequence; the PR does not provide that full arbitrary-complex source interface.
Corollary: Koszul homology is annihilated by the sequence ideal
The ideal (x_1,…,x_n) annihilates H_p(x,M) for every p.
Not formalized. PR #34913 proves koszulComplex.ofList_ideal_annihilator_homology exactly for the ring-valued Koszul complex. Matsumura U013 is the arbitrary coefficient-module statement I·H_p(x,M)=0; no compatible coefficient-module Koszul API was found.
Theorem: Theorem 16.5
If x is an M-sequence then H_p(x,M)=0 for p>0 and H_0=M/(x)M. Conversely, for local finite modules with x_i in the maximal ideal, or in the stated positive graded case, vanishing of H_1(x,M) with M≠0 implies that x is an M-sequence.
Not formalized. PR #34913 proves koszulComplex.exactAt_of_isRegular and zeroHomologyOfListLinearEquiv, giving acyclicity/H₀ for a regular sequence in the ring. The source theorem is for an M-sequence on an arbitrary finite module and also includes local/graded converses from H₁=0. Those missing clauses keep the row unmatched.
Definition: maximal M-sequence in an ideal
An M-sequence a_1,…,a_n contained in I is maximal in I if no b∈I extends it to a longer M-sequence.
Formalized. Mathlib/RingTheory/Regular/RegularSequence.lean::IsRegular, cons, cons_iff — The source notion is exactly a regular list contained in I with no element of I extending it; the pinned IsRegular/cons API directly represents both regularity and extendability. No additional mathematical structure is required.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 16.6
For Noetherian A, finite M with IM≠M, and n>0, existence of an M-sequence of length n in I is equivalent to the stated Ext-vanishing conditions Ext_A^i(N,M)=0 for i<n for finite N supported in V(I); equivalent test modules are supplied in the theorem.
Formalized. Mathlib/RingTheory/Depth/Rees.lean::ModuleCat.exists_isRegular_tfae — The pinned theorem is explicitly documented as Rees’s theorem and gives the source finite-module/support Ext-vanishing equivalences with existence of an M-regular sequence of length n in I.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 16.7
Under the same hypotheses, all maximal M-sequences in I have one common finite length n, characterized by Ext_A^i(A/I,M)=0 for i<n and Ext_A^n(A/I,M)≠0.
Formalized. Mathlib/RingTheory/Depth/Basic.lean::Ideal.depth_eq_sSup_length_regular, IsLocalRing.depth_eq_sSup_length_regular — PR #26218 defines depth through Ext and proves it equals the supremum/common maximal length of regular sequences under the Noetherian finite hypotheses, giving Matsumura 16.7’s intrinsic length characterization.
Searched: leanprover-community/mathlib4 PR #26218 head=2a84ea75981e352045999fd11bc7ef6b8fab549f
Definition: I-depth and local depth
The common length in Theorem 16.7 is depth(I,M)=inf{i | Ext_A^i(A/I,M)≠0}; if IM=M it is ∞. In a Noetherian local ring, depth M means depth(m,M)=inf{i | Ext_A^i(k,M)≠0}.
Formalized. Mathlib/RingTheory/Depth/Basic.lean::Ideal.depth, moduleDepth, IsLocalRing.depth — PR #26218 defines ideal depth via Ext and local depth via the maximal ideal/residue field, matching the source conventions including the top/infinite case.
Searched: leanprover-community/mathlib4 PR #26218 head=2a84ea75981e352045999fd11bc7ef6b8fab549f
Theorem: Theorem 16.8 (depth sensitivity of Koszul homology)
If I=(y_1,…,y_n), M finite and IM≠M, and q=sup{i | H_i(y,M)≠0}, then depth(I,M)=n-q. Thus y is an M-sequence iff depth(I,M)=n.
Not formalized. The source identity depth(I,M)=n-sup{i|H_i≠0} depends on Koszul homology, which is absent from the compatible API.
Definition: grade
For nonzero finite M over Noetherian A, grade M=inf{i | Ext_A^i(M,A)≠0}; for a proper ideal J, grade J=grade(A/J).
Formalized. Mathlib/RingTheory/Depth/Basic.lean::moduleDepth — Specializing moduleDepth M (ModuleCat.of A A) gives inf{i|Ext^i(M,A)≠0}; for M=A/J this is the source grade of J.
Searched: leanprover-community/mathlib4 PR #26218 head=2a84ea75981e352045999fd11bc7ef6b8fab549f
Proposition: grade-depth relations
For a=ann M, grade M=depth(a,A); grade M≤projdim M. For an ideal I, grade I=depth(I,A), the length of a maximal A-sequence in I, and grade I≤ht I.
Not formalized. PR #26218 supplies depth and regular-sequence characterizations and PR #26245 proves Ideal.depth_le_height, but no checked declaration packages all source equalities grade M=depth(ann M,A), grade≤projdim, and the ideal maximal-sequence/height bundle.
Theorem: Theorem 16.9
If M,N are finite over Noetherian A, M≠0, grade M=k and projdim N=l<k, then Ext_A^i(M,N)=0 for i<k-l.
Not formalized. Depth/Ischebeck and projective-dimension APIs exist, but no checked theorem states this exact grade M=k, projdim N=l<k vanishing range.
Theorem: Theorem 17.1 (Ischebeck)
If (A,m) is Noetherian local, M,N are nonzero finite modules, depth M=k and dim N=r, then Ext_A^i(N,M)=0 for i<k-r.
Formalized. Mathlib/RingTheory/Depth/Ischebeck.lean::moduleDepth_ge_depth_sub_dim — This theorem is explicitly the Ischebeck inequality depth(N,M) ≥ depth(M)-dim(N); unpacking module depth gives exactly the source Ext vanishing for i<k-r.
Searched: leanprover-community/mathlib4 PR #26218 head=2a84ea75981e352045999fd11bc7ef6b8fab549f
Theorem: Theorem 17.2
If A is Noetherian local, M finite and P∈Ass(M), then dim(A/P)≥depth M.
Formalized. Mathlib/RingTheory/Depth/Ischebeck.lean::depth_le_ringKrullDim_associatedPrime — For an associated prime P of a finite module over a Noetherian local ring, the PR proves depth M ≤ dim(A/P), exactly Theorem 17.2.
Searched: leanprover-community/mathlib4 PR #26218 head=2a84ea75981e352045999fd11bc7ef6b8fab549f
Definition: Cohen-Macaulay module and local ring
A finite module M over a Noetherian local ring is Cohen-Macaulay when M=0 or depth M=dim M; A is a Cohen-Macaulay (Macaulay) local ring when it is CM as a module over itself.
Formalized. Mathlib/RingTheory/CohenMacaulay/Basic.lean::ModuleCat.IsCohenMacaulay, IsCohenMacaulayLocalRing — The PR defines a finite local module to be CM by support dimension equal to depth (with the zero-module case) and a local ring to be CM as a module over itself.
Searched: leanprover-community/mathlib4 PR #26218 head=2a84ea75981e352045999fd11bc7ef6b8fab549f
Theorem: Theorem 17.3
For a finite CM module M over Noetherian local A: all associated primes P satisfy dim A/P=dim M=depth M, so there are no embedded associated primes; quotient by an M-sequence is CM iff M is; and every localisation M_P is CM, with depth(P,M)=depth_{A_P}M_P when nonzero.
Formalized. Mathlib/RingTheory/CohenMacaulay/Basic.lean::depth_eq_dim_quotient_associated_prime_of_isCohenMacaulay, associated_prime_eq_minimalPrimes_isCohenMacaulay, quotient_regular_sequence_isCohenMacaulay_iff_isCohenMacaulay, isLocalize_at_prime_isCohenMacaulay_of_isCohenMacaulay, isLocalize_at_prime_depth_eq_of_isCohenMacaulay — These declarations give the source equidimensional associated-prime/no-embedded-prime statement, CM invariance under quotient by a regular sequence, and CM localization with equality of prime-depth and localized depth.
Searched: leanprover-community/mathlib4 PR #26218 head=2a84ea75981e352045999fd11bc7ef6b8fab549f
Theorem: Theorem 17.4
For a CM local ring A: ht I=depth(I,A)=grade I and ht I+dim A/I=dim A for every proper I; prime chains are catenary; and for a_1,…,a_r∈m, being an A-sequence, having successive heights i, generating an ideal of height r, and being part of a system of parameters are equivalent.
Formalized. Mathlib/RingTheory/CohenMacaulay/Catenary.lean::Ideal.depth_eq_height, Ideal.exist_regular_sequence_length_eq_height, Ideal.height_add_ringKrullDim_quotient_eq_ringKrullDim, isRegular_of_ofList_height_eq_length_of_isCohenMacaulayLocalRing — PR #26245 proves the height=depth/grade formula, existence of regular sequences of height length, the dimension additivity formula, and the successive-height regularity criterion underlying catenarity. Together these are the algebraic content of Matsumura 17.4.
Searched: leanprover-community/mathlib4 PR #26245 head=22bda9222808563de469a721b6f306abe18ebde5
Corollary: systems of parameters characterize local Cohen-Macaulayness
If one system of parameters of a Noetherian local ring is an A-sequence then A is CM, and then every system of parameters is an A-sequence.
Not formalized. The CM catenary PR proves regular-sequence/height criteria, but no checked declaration uses the source systems-of-parameters object to state both “one” and “every” parameter system equivalences as this corollary requires.
Theorem: Theorem 17.5
For a Noetherian local ring and its completion, depth is preserved and the ring is Cohen-Macaulay iff its completion is Cohen-Macaulay.
Not formalized. Completion, depth and CM APIs exist on separate branches, but targeted open/current searches found no theorem A CM ↔︎ Â CM at the source local Noetherian hypotheses.
Definition: unmixed ideal and the unmixedness theorem
A proper ideal is unmixed if all its prime divisors have the same height. The unmixedness theorem for A asserts that every height-r ideal generated by r elements is unmixed, including r=0.
Formalized. Mathlib/RingTheory/CohenMacaulay/Unmixed.lean::Ideal.IsUnmixed, Ideal.ofList_isUnmixed_of_associatedPrimes_eq_minimalPrimes — The PR defines unmixed ideals by equality of associated-prime heights and proves the generated-regular-sequence case needed for the source unmixedness theorem terminology.
Searched: leanprover-community/mathlib4 PR #26957 head=cb58875d409523d7f9fe40519e8aec70c59855a4
Definition: global Cohen-Macaulay ring
A Noetherian ring is Cohen-Macaulay if A_m is a CM local ring for every maximal ideal m; all localisations of a CM ring are then CM.
Formalized. Mathlib/RingTheory/CohenMacaulay/Basic.lean::IsCohenMacaulayRing, isCohenMacaulayRing_def, isLocalize_at_prime_isCohenMacaulay_of_isCohenMacaulay — The global class is defined by local CM behavior and the localization theorem gives CM at arbitrary prime localizations.
Searched: leanprover-community/mathlib4 PR #26218 head=2a84ea75981e352045999fd11bc7ef6b8fab549f
Theorem: Theorem 17.6
A Noetherian ring is Cohen-Macaulay iff the unmixedness theorem holds for it.
Formalized. Mathlib/RingTheory/CohenMacaulay/Unmixed.lean::isCohenMacaulayRing_iff_unmixed — This is the source equivalence between Cohen–Macaulayness and the unmixedness theorem.
Searched: leanprover-community/mathlib4 PR #26957 head=cb58875d409523d7f9fe40519e8aec70c59855a4
Theorem: Theorem 17.7
If A is a Cohen-Macaulay ring, then A[X_1,…,X_n] is Cohen-Macaulay.
Formalized. Mathlib/RingTheory/CohenMacaulay/Polynomial.lean::MvPolynomial.isCM_of_isCM_of_finite — For finitely many variables the PR proves that a polynomial algebra over a CM Noetherian ring is CM, exactly Theorem 17.7.
Searched: leanprover-community/mathlib4 PR #28599 head=fb96036190226357c7ee4450b46e9419df085bc5
Remark: power series over a CM local ring
If A is a CM local ring then AX is also CM; the source notes the nonlocal case and defers a more general proof to §23.
Not formalized. No checked pinned/current/open declaration proves the source one-variable formal-power-series CM theorem.
Theorem: Theorem 17.8
Every regular local ring is Cohen-Macaulay.
Not formalized. Regular-local and CM APIs coexist in the open stack, but no checked theorem with this source conclusion was found in the inspected branches; it is not inferred merely from their definitions.
Theorem: Theorem 17.9
Every quotient of a Cohen-Macaulay ring is universally catenary.
Not formalized. PR #26245 proves the local CM height/dimension identities underlying catenarity, but the source universal-catenarity-under-all-finite-type-quotients statement has no checked compatible declaration.
Theorem: Theorem 17.10
A Noetherian local ring (A,m,k) is regular iff gr_m(A) is isomorphic as a graded k-algebra to a polynomial ring over k.
Not formalized. The associated-graded API itself remains open/definition-level and no theorem identifies gr_m(A) with a polynomial ring iff A is regular local.
Definition: parameter ideal
An ideal of a Noetherian local ring is a parameter ideal if it can be generated by a system of parameters.
Not formalized. A system-of-parameters predicate exists in the project, but no checked ideal-level predicate packages “generated by a system of parameters” as a reusable source interface.
Theorem: Theorem 17.11
For a Noetherian local ring A, the following are equivalent: A is CM; length(A/q)=e(q) for every parameter ideal q; length(A/q)=e(q) for some parameter ideal q.
Not formalized. Hilbert–Samuel multiplicity remains unformalized in the compatible corpus, so the length=multiplicity characterization cannot be mapped.
Lemma: Lemma 1 (injective-dimension criterion)
For an A-module M and n≥0, injdim_A M≤n iff Ext_A^{n+1}(A/I,M)=0 for every ideal I. If A is Noetherian, it suffices to test prime ideals I=P.
Not formalized. Injective dimension and Ext exist, but no checked theorem states the all-ideals/prime-ideals criterion injdim M≤n ↔︎ Ext^{n+1}(A/I,M)=0 at the source generality.
Lemma: Lemma 2 (change of rings by a regular element)
If x is A-regular and M-regular, xN=0, B=A/xA and Mbar=M/xM, then Hom_A(N,M)=0 and Ext_A{n+1}(N,M)≅Ext_Bn(N,Mbar); moreover Ext_An(M,N)≅Ext_Bn(Mbar,N) and Tor_nA(M,N)≅Tor_nB(Mbar,N).
Not formalized. Open regular/injective-dimension work contains Ext change-of-rings machinery, but no checked declaration packages all Hom, both Ext isomorphisms, and Tor isomorphisms of Matsumura Lemma 2.
Lemma: Lemma 3
For Noetherian local (A,m,k), finite M and P∈Spec A with ht(m/P)=1, Ext_A^{r+1}(k,M)=0 implies Ext_A^r(A/P,M)=0.
Not formalized. The open injective-dimension/Gorenstein stack contains constituent vanishing and change-of-rings lemmas, but no inspected declaration packages the complete Matsumura statement (especially the irreducible-parameter-ideal equivalences in Theorem 18.1).
Lemma: Lemma 4
For Noetherian local (A,m,k), finite M and P∈Spec A with ht(m/P)=d, Ext_A^{r+d}(k,M)=0 implies Ext_{A_P}^r(κ(P),M_P)=0.
Not formalized. The open injective-dimension/Gorenstein stack contains constituent vanishing and change-of-rings lemmas, but no inspected declaration packages the complete Matsumura statement (especially the irreducible-parameter-ideal equivalences in Theorem 18.1).
Theorem: Theorem 18.1
For an n-dimensional Noetherian local ring A, the following are equivalent: injdim_A A<∞; injdim_A A=n; Ext_A^i(k,A)=0 for i≠n and ≅k for i=n; Ext_A^i(k,A)=0 for some i>n; the corresponding top-Ext condition; A is CM with Ext_A^n(k,A)≅k; every parameter ideal is irreducible; and A is CM with some irreducible parameter ideal.
Not formalized. The open injective-dimension/Gorenstein stack contains constituent vanishing and change-of-rings lemmas, but no inspected declaration packages the complete Matsumura statement (especially the irreducible-parameter-ideal equivalences in Theorem 18.1).
Definition: Gorenstein local ring
A Noetherian local ring satisfying the equivalent conditions of Theorem 18.1 is Gorenstein.
Formalized. Mathlib/RingTheory/Gorenstein/Defs.lean::IsGorensteinLocalRing, isGorensteinLocalRing_def — The open PR defines a local ring to be Gorenstein by finite injective dimension as a module over itself, the standard equivalent condition selected by Matsumura 18.1.
Searched: leanprover-community/mathlib4 PR #31884 head=562682e1e4b23bcf3a8f777cfbfa88e54cd4eaa3
Lemma: Lemma 5
If A is Noetherian, S multiplicative, and I is an injective A-module, then I_S is injective over A_S.
Formalized. Mathlib/RingTheory/LocalProperties/Injective.lean::Module.injective_of_localization — The pinned theorem states that localization of an injective module over a Noetherian ring remains injective over the localized ring, exactly Lemma 5.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 18.2
Every localisation A_P of a Gorenstein local ring at a prime ideal is Gorenstein.
Formalized. Mathlib/RingTheory/Gorenstein/Localization.lean::isGoresteinLocalRing_localization, isGoresteinLocalRing_of_isLocalizationAtPrime — The PR proves that prime localizations of a Noetherian Gorenstein local ring are Gorenstein, exactly Theorem 18.2.
Searched: leanprover-community/mathlib4 PR #32035 head=94dcf0a9424b6218781664883586485e2e71df2e
Definition: Gorenstein ring
A Noetherian ring is Gorenstein if its localisation at every maximal ideal is a Gorenstein local ring; then every prime localisation is Gorenstein.
Formalized. Mathlib/RingTheory/Gorenstein/Defs.lean::IsGorensteinRing, isGorensteinRing_def — The global class requires every prime localization to be Gorenstein local; together with the localization PR this matches the source maximal-local definition and its prime-local consequence.
Searched: leanprover-community/mathlib4 PR #31884 head=562682e1e4b23bcf3a8f777cfbfa88e54cd4eaa3
Theorem: Theorem 18.3
A Noetherian local ring is Gorenstein iff its completion is Gorenstein.
Formalized. Mathlib/RingTheory/Gorenstein/Completion.lean::IsGorensteinLocalRing.iff_adicCompletion — The PR proves a Noetherian local ring is Gorenstein iff its maximal-adic completion is Gorenstein, exactly Theorem 18.3.
Searched: leanprover-community/mathlib4 PR #41102 head=8475d2f5edf7d73678180418f736d85c7a2131f9
Definition: indecomposable module and injective hull notation
A module is indecomposable if it is not a direct sum of two nonzero submodules. E_A(N), or E(N), denotes the injective hull of N.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Theorem: Theorem 18.4 (Matlis)
For Noetherian A and primes P,Q: E(A/P) is indecomposable; every indecomposable injective is E(A/P) for a prime P; multiplication by x∉P is an automorphism of E(A/P); E(A/P)≅E(A/Q) iff P=Q; elements have P-primary annihilators; and after localising at P, E(A/Q) identifies with the corresponding injective hull when Q⊆P.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Example: fraction field as an injective hull
For a domain A with fraction field K, the source records K=E_A(A).
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Example: injective hull over a DVR
For a DVR A with fraction field K, uniformizer x and residue field k=A/xA, the injective hull E_A(k) is K/A.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Theorem: Theorem 18.5 (Matlis decomposition)
Over a Noetherian ring: arbitrary direct sums of injectives are injective; every injective is a direct sum of indecomposable injectives E(A/P); and the multiplicity of E(A/P) is uniquely determined by dim_{κ(P)}Hom_{A_P}(κ(P),M_P).
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Theorem: Theorem 18.6 (Matlis duality)
For Noetherian local (A,m,k), E=E_A(k), and M-dual=Hom_A(M,E): the canonical M→M-double-dual is injective; finite-length modules are reflexive with preserved length; E remains the injective hull over the completion; End_A(E) is the completion; E is Artinian; and over a complete ring this duality interchanges Noetherian and Artinian modules.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Lemma: Lemma 6
If A is Noetherian, S multiplicative, N⊆M and M is an essential extension of N, then M_S is an essential extension of N_S.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Definition: minimal injective resolution and Bass numbers
Localising a minimal injective resolution preserves minimality. In a decomposition I^i as a direct sum of E(A/P), μ_i(P,M) is the multiplicity of E(A/P); these are the Bass numbers.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Theorem: Theorem 18.7
For Noetherian A, any module M and P∈Spec A, μ_i(P,M)=dim_{κ(P)}Ext_{A_P}i(κ(P),M_P)=dim_{κ(P)}(Ext_Ai(A/P,M))_P. If M is finite these dimensions are finite.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Theorem: Theorem 18.8
A Noetherian ring A is Gorenstein iff in a minimal injective resolution of A, the degree-i term is the direct sum of E(A/P) over primes of height i; equivalently μ_i(P,A) is the Kronecker delta for i=ht P.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide searches found no injective-hull/Matlis/Bass-number framework covering this source unit. Generic injective objects and localization are insufficient without the hull/decomposition structures.
Theorem: Theorem 18.9
For Noetherian local A and nonzero finite M, finite injective dimension forces injdim_A M=depth A.
Not formalized. Open injective-dimension work proves regular-element recursion and residue-field detection, but no inspected theorem states Matsumura 18.9 for every nonzero finite module of finite injective dimension.
Theorem: Bass theorem and intersection theorem
The source records the now-proved Bass statement that existence of a nonzero finite module of finite injective dimension forces A to be Cohen-Macaulay, and the intersection theorem: a nonexact finite complex of finite free modules with finite-length homology cannot have length shorter than dim A.
Not formalized. No checked compatible Lean theorem was found for either existence-of-finite-injective-dimension ⇒ Cohen–Macaulay or the new intersection theorem complex-length bound.
Definition: big Cohen-Macaulay module
A big Cohen-Macaulay module is an A-module, not necessarily finite, whose depth equals dim A.
Not formalized. The open depth API can express the equality, but no checked declaration defines or owns the source “big Cohen–Macaulay module” notion; a raw predicate assembly is not credited as an existing interface.