Chapter 7. Regular rings
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 14 definitions, 25 theorems, 2 propositions, 6 lemmas, 2 corollaries, 2 examples, 2 counterexamples and 2 other statements.
Of the 55 statements checked against Lean, 19 are formalized somewhere and 36 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 36 | 65% | A documented search found no Lean statement of it anywhere. |
| in another Lean project | 12 | 22% | Some other Lean development has it; using it means porting that code. |
| in Mathlib | 7 | 13% | Mathlib states and proves it. |
| checked in total | 55 |
- Canonical source block: FC13 Matsumura Chapter 7,
FC13-C07-U001–FC13-C07-U055, §§19–21, in canonical source-ID order from Foundational corpus units FC13 Matsumura. All 55 IDs are retrieved throughagent-memory, validated once/in-order, and assigned one route each. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280. The project definesLeanCategories.Homological.globalDimension, but U006 bundles additional finite-module and local residue-field theorems not owned by the project, so the definition alone does not earn aproject-existingroute. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native C07 owners includeIsRegularRing, the Noetherian height-one-principal UFD criterion, GCD/lcm infrastructure, Picard modules/groups, and the invertible-fractional-ideal class group withClassGroup.equivPic. - Current Mathlib was refreshed 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493. Exact open-branch owners are recorded asreference-port: PR #26215 (fbbf6add2600af0c6046b367cd16729dc6e94e61) Auslander–Buchsbaum; PR #29802 (9c971a554fb6265f06b80bc62c7b314f4f2d33ec) global dimension/Auslander–Buchsbaum–Serre/localization; PR #39510 (a277a2ff8ecab34f00ad3e962eb7cbd18a35de02) regular local UFD (inspected withoutsorry/admit); PR #34913 (c7780ed427bbed31ee0c430a5594ed5ea4c7d5b5) Koszul/complete-intersection ε₁ theory; and PR #41103 (cb5e638c184221996aa2100f6cbb7074a55795bb) CI⇒Gorenstein and the implication chain. These are ports, not importable package routes. - Search channels used project source, P, H/current/open Mathlib, source/docs, Loogle/LeanSearch-oriented repository tooling, Reservoir/indexed discovery, and GitHub-wide Lean-code search. No compatible André–Quillen/cotangent-complex homology owner was found.
- Strict bundle semantics were enforced. U006 is not credited from a global-dimension definition plus regular-local residue-field theorem because the source local equality is arbitrary Noetherian local; U010/U011 remain unmatched despite derivable/local partial results; U024 is not credited from rank alone without the rank-one torsion-free-to-ideal theorem; and U037/U040–U045 are not mapped through pinned
ClassGroup, because Matsumura uses the Weil divisor class group of a general Krull ring whereas P’s class group is invertible fractional ideals modulo principal ideals. - PR #34913’s Koszul development was also used to correct FC13 C06 provenance before C07 promotion. In C07 it exactly supplies U003 and the ε₁/complete-intersection rows U047–U050; it still does not provide the higher ε_i family U046.
- Route totals for C07:
mathlib7,project-existing0,package-import0,reference-port12,unmatched36.
Definition: minimal free resolution over a local ring
A free resolution of a finite module over a local ring is minimal when every differential has image inside the maximal ideal times the next free module. Minimal resolutions exist, and their free ranks are invariants detected by Tor with the residue field.
Not formalized. Projective dimension and Tor infrastructure exist, but no checked pinned/current/open declaration constructs Matsumura’s minimal free resolution over a local ring with differentials in the maximal ideal and identifies all Betti ranks with Tor against the residue field.
Lemma: Lemma 1
If L_• is a minimal free resolution of finite M over local (A,m,k), then dim_k Tor_i^A(M,k)=rank L_i; in particular Tor_i(M,k)=0 forces all later terms to vanish and projdim M<i.
Not formalized. Projective dimension and Tor infrastructure exist, but no checked pinned/current/open declaration constructs Matsumura’s minimal free resolution over a local ring with differentials in the maximal ideal and identifies all Betti ranks with Tor against the residue field.
Example: Koszul resolution of a quotient by a regular sequence
If x_1,…,x_n is an A-sequence, the Koszul complex augmented by A/(x) is a free resolution of A/(x).
Formalized. Mathlib/RingTheory/KoszulComplex/Complex.lean::koszulComplex.ofList, exactAt_of_isRegular, zeroHomologyOfListLinearEquiv — PR #34913 constructs the finite free Koszul complex on a list, proves positive-degree exactness for a regular sequence, and identifies H₀ with the quotient by the generated ideal; this is exactly the source free resolution of A/(x).
Searched: leanprover-community/mathlib4 PR #34913 head=c7780ed427bbed31ee0c430a5594ed5ea4c7d5b5
Theorem: Theorem 19.1 (Auslander-Buchsbaum)
For Noetherian local A and nonzero finite M of finite projective dimension, projdim_A M+depth M=depth A.
Formalized. Mathlib/RingTheory/Depth/AuslanderBuchsbaum.lean::AuslanderBuchsbaum — The theorem is explicitly the Auslander–Buchsbaum formula pd M + depth M = depth A for finite M of finite projective dimension over a Noetherian local ring.
Searched: leanprover-community/mathlib4 PR #26215 head=fbbf6add2600af0c6046b367cd16729dc6e94e61
Lemma: Lemma 2
For a ring A and n>0, the conditions “all A-modules have projective dimension ≤n”, “all finite A-modules have projective dimension ≤n”, “all modules have injective dimension ≤n”, and Ext_A^{n+1}(M,N)=0 for all M,N are equivalent.
Formalized. Mathlib/RingTheory/GlobalDimension.lean::globalDimension_le_tfae, globalDimension_eq_sup_projectiveDimension_finite — The PR defines left global dimension by the supremum of projective dimensions and gives the finite-module/ideal-quotient criteria. It uses projective dimension, hence the standard Ext characterization, matching Matsumura 19.1.
Searched: leanprover-community/mathlib4 PR #29802 head=9c971a554fb6265f06b80bc62c7b314f4f2d33ec
Definition: global dimension
gl.dim A is the supremum of projective dimensions of all A-modules; by Lemma 2 it is the maximum over finite modules, and for Noetherian local (A,m,k), gl.dim A=projdim_A k.
Not formalized. The project already defines globalDimension, and PR #29802 proves the supremum-over-finite-modules result. Its residue-field equality is proved under regular-local hypotheses, whereas Matsumura’s U006 states gl.dim A = pd_A(k) for an arbitrary Noetherian local ring. Strict bundle semantics therefore leaves U006 unmatched.
Theorem: Theorem 19.2 (Serre)
For a Noetherian local ring A, the following are equivalent: A is regular; gl.dim A=dim A; gl.dim A<∞.
Formalized. Mathlib/RingTheory/RegularLocalRing/AuslanderBuchsbaumSerre.lean::IsRegularLocalRing.of_globalDimension_lt_top; Mathlib/RingTheory/RegularLocalRing/GlobalDimension.lean::IsRegularLocalRing.globalDimension_eq_ringKrullDim — These theorems give A regular local ↔︎ gl.dim A<∞ and in the regular case gl.dim A=dim A, exactly the three equivalent conditions in Matsumura 19.2.
Searched: leanprover-community/mathlib4 PR #29802 head=9c971a554fb6265f06b80bc62c7b314f4f2d33ec
Theorem: Theorem 19.3 (Serre)
If A is regular local and P is prime, then A_P is regular local.
Formalized. Mathlib/RingTheory/RegularLocalRing/Localization.lean::IsRegularLocalRing.of_isLocalization, isRegularRing_of_localization_maximal_isRegularLocalRing — The PR proves localization of a regular local ring at a prime is regular local, and more generally regularity is preserved by localization, exactly Theorem 19.3.
Searched: leanprover-community/mathlib4 PR #29802 head=9c971a554fb6265f06b80bc62c7b314f4f2d33ec
Definition: regular ring
A regular ring is a Noetherian ring whose localisation at every prime is regular local; it suffices to test maximal ideals.
Formalized. Mathlib/RingTheory/RegularLocalRing/Defs.lean::IsRegularRing, isRegularRing_iff — IsRegularRing is a Noetherian ring whose localization at every prime is regular local, exactly Matsumura’s definition; maximal-local testing is the equivalent local formulation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 19.4
Every regular ring is normal.
Not formalized. PR #39510 proves every regular local ring is a UFD, and PR #29802 gives regular localization, so normality is derivable with pinned UFD-integrally-closed facts. No checked source-shaped declaration/assembly was found in a single compatible branch, so this row is conservatively unmatched.
Theorem: Theorem 19.5
If A is regular, then A[X] and AX are regular.
Not formalized. Pinned P proves polynomial and finite-variable multivariate-polynomial stability of regular rings. PR #34913 proves the power-series result for regular local rings, not Matsumura’s full regular-ring statement. The bundled polynomial+formal-power-series theorem remains unmatched.
Lemma: Lemma 3 (Schanuel)
Given exact sequences 0→K→P→M→0 and 0→K′→P′→M→0 with P,P′ projective, one has K⊕P′≅K′⊕P.
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Lemma: Lemma 4 (generalised Schanuel)
For two finite projective resolutions of the same length, alternating direct sums of their projective terms are isomorphic in the generalized Schanuel relation.
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Definition: finite free resolution and Euler number
An FFR is a finite free resolution. If M has one, χ(M)=Σ_i(-1)^i rank F_i is independent of the chosen FFR, localises unchanged, and equals rank M when M is free.
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Theorem: Theorem 19.6
If (A,m) is local and every finite subset E⊂m has a common nonzero annihilator, then every A-module admitting an FFR is free. For Noetherian A this hypothesis is equivalent to m∈Ass(A), or depth A=0.
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Theorem: Theorem 19.7
For any ring A, every module M admitting an FFR has χ(M)≥0.
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Theorem: Theorem 19.8 (Auslander-Buchsbaum)
For Noetherian A and M with an FFR, the following are equivalent: ann(M)≠0; χ(M)=0; ann(M) contains an A-regular element.
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Theorem: Theorem 19.9 (Vasconcelos)
For Noetherian local A and proper I with finite projective dimension, I is generated by an A-sequence iff I/I² is free over A/I.
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Definition: Lech-independent sequence
x_1,…,x_n are independent in Lech’s sense if Σa_ix_i=0 with a_i∈A implies every a_i∈(x_1,…,x_n); equivalently their classes form a basis of I/I² for I=(x_i).
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Corollary: Lech independence in regular local rings
In a regular local ring, every Lech-independent finite sequence in the maximal ideal is an A-sequence.
Not formalized. Projective/free module and homological-complex infrastructure exist, but targeted pinned/current/open/external searches found no source-shaped theorem with the stated finite-free-resolution/Euler-characteristic content.
Theorem: Theorem 20.1
A Noetherian domain is a UFD iff every height-one prime ideal is principal.
Formalized. Mathlib/RingTheory/Ideal/UFD.lean::UniqueFactorizationMonoid.iff_forall_isPrincipal_of_height_eq_one — For a Noetherian domain, the pinned theorem is exactly the equivalence between unique factorization and principality of every height-one prime ideal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 20.2
If A is a Noetherian domain, S is generated multiplicatively by prime elements, and A_S is a UFD, then A is a UFD.
Formalized. Mathlib/GroupTheory/MonoidLocalization/UniqueFactorization.lean::UniqueFactorizationMonoid.of_isLocalization — Pinned Mathlib proves the stronger theorem that localization of any unique-factorization monoid at an arbitrary submonoid is again a UFM. This immediately covers Matsumura’s submonoid generated by prime elements.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma: Lemma 1
If A is a domain and an ideal a is stably free of rank one, i.e. a⊕An≅A{n+1}, then a is principal.
Not formalized. Pinned stably-free and Picard/invertible-module APIs give constituent facts, but no checked declaration states that a nonzero rank-one ideal that is stably free must be principal under the source hypotheses.
Definition: rank over a domain
For finite M over a domain A with fraction field K, rank M=dim_K(M⊗_A K). A torsion-free finite rank-one module embeds into K and is isomorphic to an ideal.
Not formalized. Pinned rank/localization APIs prove rank is fraction-field dimension, but no checked theorem says every finite torsion-free rank-one module over a domain is isomorphic to an ideal of A. The definition half alone does not cover the row.
Theorem: Theorem 20.3 (Auslander-Buchsbaum)
Every regular local ring is a UFD.
Formalized. Mathlib/RingTheory/RegularLocalRing/UFD.lean::IsRegularLocalRing.uniqueFactorizationMonoid — PR #39510 proves every regular local ring has unique factorization. The inspected file contains no sorry/admit; as an open PR it is a reference-port route.
Searched: leanprover-community/mathlib4 PR #39510 head=a277a2ff8ecab34f00ad3e962eb7cbd18a35de02
Proposition: Kaplansky stable-ideal product theorem
If A is a domain and ⊕{i=1}^r I_i≅⊕{i=1}^r J_i for ideals I_i,J_i, then I_1⋯I_r≅J_1⋯J_r; the source points to Appendix C for a proof.
Not formalized. No checked pinned/current/open/external declaration matches the stated ideal-theoretic theorem. Mathlib’s UniqueFactorizationDomain/Kaplansky.lean is a different Kaplansky factorization criterion and is not credited by name similarity.
Theorem: Theorem 20.4
If A is a Noetherian domain in which every finite module has an FFR, then A is a UFD.
Not formalized. No checked pinned/current/open/external declaration matches the stated ideal-theoretic theorem. Mathlib’s UniqueFactorizationDomain/Kaplansky.lean is a different Kaplansky factorization criterion and is not credited by name similarity.
Definition: gcd and lcm in a domain
The usual divisibility universal properties define gcd and lcm in a domain; e is an lcm of a,b exactly when (e)=(a)∩(b).
Formalized. Mathlib/Algebra/GCDMonoid/Basic.lean::GCDMonoid, gcd_dvd_left, gcd_dvd_right, dvd_gcd, lcm_dvd_iff, gcd_mul_lcm — GCDMonoid packages gcd/lcm universal divisibility properties up to associates; gcd_mul_lcm is exactly gcd(u,v)·lcm(u,v) ~ uv. Principal-ideal sum/intersection are the divisibility lattice translations.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma: Lemma 2
If an lcm of a,b exists in a domain, then a gcd exists.
Formalized. Mathlib/Algebra/GCDMonoid/Basic.lean::isGCDMonoid_iff_exists_lcm, gcdMonoidOfLCM — The pinned theorem/constructor says precisely that a commutative cancellative monoid with zero admitting lcms admits a GCD-monoid structure, hence gcds.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Counterexample: gcd need not imply lcm
In a Noetherian non-UFD domain one can choose an irreducible nonprime a and x so that gcd(a,x)=1 but (a)∩(x) is not principal, hence no lcm exists.
Not formalized. No checked declaration realizes the source monoid/ring example showing gcd existence need not imply lcm existence.
Proposition: arbitrary intersections of principal ideals in a UFD
In a UFD, any intersection of principal (even principal fractional) ideals is principal, with prime exponents given by the componentwise suprema.
Not formalized. Finite lcm/principal-intersection arithmetic is available, but no checked theorem states that an arbitrary nonzero intersection of principal ideals in a UFD is principal.
Theorem: Theorem 20.5
A domain is a UFD iff principal ideals satisfy ACC and every pair of elements has an lcm.
Not formalized. Pinned WfDvdMonoid is equivalent to ACC on principal ideals and lcm existence yields GCDMonoid, but no checked declaration packages Matsumura’s exact two-condition iff with UFD.
Theorem: Theorem 20.6
If A is regular and u,v∈A, then uA∩vA is a projective ideal.
Not formalized. No checked declaration proves uA∩vA projective in an arbitrary regular ring under Matsumura’s hypotheses.
Theorem: Theorem 20.7
Every projective ideal in a UFD is principal.
Not formalized. Picard/invertible and UFD APIs give adjacent results, but no checked theorem states the source projective-ideal principality result.
Theorem: Theorem 20.8
If A is both regular and a UFD, then AX is a UFD.
Counterexample: UFD need not be preserved by formal power series
The source records that there exist UFDs A for which AX is not a UFD.
Not formalized. No checked Lean example realizes the source counterexample showing A UFD does not imply AX UFD.
Definition: divisor group and divisor class group of a Krull ring
For height-one primes p of a Krull ring A, D(A) is the free abelian group on them; div(a)=Σ_p v_p(a)p for a∈Frac(A)^*. Principal divisors form F(A), and C(A)=D(A)/F(A). One has A a UFD iff C(A)=0.
Not formalized. Pinned ClassGroup is the invertible-fractional-ideal/Picard class group of a domain, not Matsumura’s free abelian group on height-one primes modulo principal divisors for a general Krull ring. No compatible Weil-class-group interface was found.
Definition: rank of a finite projective module and Picard group
For finite projective M, p↦rank_{A_p}M_p is locally constant on Spec A; rank-r means it is constantly r. Pic(A) is the abelian group of isomorphism classes of finite projective rank-one modules under tensor product, with dual module giving inverses; Pic(A)=0 for local A.
Formalized. Mathlib/RingTheory/PicardGroup.lean::Pic, Module.Invertible, Module.Invertible.finite, Module.Invertible.projective, Subsingleton — Pic R is the group of invertible module classes; invertible modules are finite projective and locally free of rank one, tensor product is the group law, and the Picard group of a local ring is subsingleton/trivial.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Comparison: Picard group via invertible fractional ideals
For a domain, finite projective rank-one modules identify with invertible fractional ideals modulo principal fractional ideals.
Formalized. Mathlib/RingTheory/ClassGroup/Basic.lean::ClassGroup; Mathlib/RingTheory/PicardGroup.lean::ClassGroup.equivPic — Pinned ClassGroup is invertible fractional ideals modulo principal ideals, and ClassGroup.equivPic gives the canonical equivalence with the Picard group, exactly the domain statement in U039.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Pic(A) embeds in C(A) for Krull rings
For a Krull ring, assigning div(I)=Σ_p v_p(I)p embeds the group of invertible fractional ideals into D(A), hence Pic(A) into C(A). For regular rings all height-one primes are invertible and C(A)=Pic(A).
Not formalized. The required Weil divisor class group/general Krull-ring or geometric class-group machinery is absent from P/current/open compatible sources; pinned ideal ClassGroup is not a substitute for the source Weil group.
Comparison: algebraic-geometric divisor and Picard groups
For a normal irreducible variety V, the source compares D(V), principal divisors, linear equivalence, C(V), Cartier divisors and Pic(V), and identifies the affine case with the class/Picard groups of its Krull coordinate ring; for smooth V, Weil and Cartier divisor classes agree.
Not formalized. The required Weil divisor class group/general Krull-ring or geometric class-group machinery is absent from P/current/open compatible sources; pinned ideal ClassGroup is not a substitute for the source Weil group.
Definition: projectively normal variety
For projective V with homogeneous coordinate ring A, V is projectively (arithmetically) normal when A is integrally closed; this is stronger than normality of all local rings.
Not formalized. The required Weil divisor class group/general Krull-ring or geometric class-group machinery is absent from P/current/open compatible sources; pinned ideal ClassGroup is not a substitute for the source Weil group.
Theorem: Grothendieck-Samuel UFD criterion
If R is regular local, P is generated by an R-sequence, A=R/P, and A_p is a UFD for every p of height below three, then A is a UFD.
Not formalized. The required Weil divisor class group/general Krull-ring or geometric class-group machinery is absent from P/current/open compatible sources; pinned ideal ClassGroup is not a substitute for the source Weil group.
Theorem: class groups under polynomial and power-series extension
The source records C(A)≅C(A[X]) for every Krull ring and C(A)≅C(AX) for every regular ring.
Not formalized. The required Weil divisor class group/general Krull-ring or geometric class-group machinery is absent from P/current/open compatible sources; pinned ideal ClassGroup is not a substitute for the source Weil group.
Example: cyclic divisor class group example
For A=k[X,Y,Z]/(Z^n-XY), char k=0, the height-one prime (x,z) satisfies n[p]=div(x); the source records C(A)≅Z/nZ, so A is not a UFD.
Not formalized. The required Weil divisor class group/general Krull-ring or geometric class-group machinery is absent from P/current/open compatible sources; pinned ideal ClassGroup is not a substitute for the source Weil group.
Definition: Koszul invariants epsilonp(A)
For Noetherian local (A,m,k), choose a minimal basis x_1,…,x_n of m and put epsilon_p(A)=dim_k H_p(x;A). These numbers are independent of the chosen minimal basis; epsilon_1(A)=0 iff A is regular.
Not formalized. PR #34913 defines only epsilon1 from first Koszul homology of the Koszul algebra. Matsumura U046 defines all ε_i and their regular-local vanishing characterization, so the full source invariant family is absent.
Definition: minimal regular presentation and relation number
If A=R/a with (R,n) regular local and a⊆n², call this a minimal regular presentation. For finite M over local R, mu_R(M)=dim_{R/n}(M/nM) is the minimal number of generators; in a minimal regular presentation epsilon_1(A)=mu_R(a).
Formalized. Mathlib/RingTheory/CompleteIntersection/Basic.lean::epsilon1, epsilon1_eq_spanFinrank, exist_isRegularLocalRing_surjective_adicCompletion_ker_le — The PR constructs a regular local presentation of the completion, defines ε₁ intrinsically from Koszul H₁, and proves for a regular presentation quotient that ε₁ equals the minimal generator number of the kernel, establishing independence and the source relation number.
Searched: leanprover-community/mathlib4 PR #34913 head=c7780ed427bbed31ee0c430a5594ed5ea4c7d5b5
Theorem: Theorem 21.1
For a regular local ring R and ideal a⊆n² with A=R/a, epsilon_1(A)=mu_R(a)≥dim R-dim A=embdim A-dim A. Equality holds iff a is generated by an R-sequence.
Formalized. Mathlib/RingTheory/CompleteIntersection/Basic.lean::epsilon1_add_ringKrullDim_ge, IsCompleteIntersectionLocalRing, isCompleteIntersectionLocalRing_def — The inequality ε₁+dim A≥embdim A is explicit, and IsCompleteIntersectionLocalRing is defined by equality, exactly Matsumura 21.1.
Searched: leanprover-community/mathlib4 PR #34913 head=c7780ed427bbed31ee0c430a5594ed5ea4c7d5b5
Definition: complete intersection local ring
A Noetherian local ring A is a complete intersection (c.i.) ring when epsilon_1(A)=embdim A-dim A.
Formalized. Mathlib/RingTheory/CompleteIntersection/Basic.lean::IsCompleteIntersectionLocalRing, isCompleteIntersectionLocalRing_def — The PR’s local complete-intersection class is exactly equality in the ε₁/embedding-dimension inequality, matching the source definition.
Searched: leanprover-community/mathlib4 PR #34913 head=c7780ed427bbed31ee0c430a5594ed5ea4c7d5b5
Theorem: Theorem 21.2
For Noetherian local A: in a regular presentation A=R/a, A is c.i. iff a is generated by an R-sequence; equivalently its completion is a quotient of a complete regular local ring by an ideal generated by a regular sequence. The property is preserved and detected by completion.
Formalized. Mathlib/RingTheory/CompleteIntersection/Basic.lean::quotient_isCompleteIntersectionLocalRing_iff, adicCompletion_isCompleteIntersectionLocalRing_iff, quotient_isCompleteIntersectionLocalRing — The PR proves a quotient of a regular local ring is CI iff the kernel generators form a regular sequence and proves maximal-adic completion invariance, exactly the source presentation/completion characterization.
Searched: leanprover-community/mathlib4 PR #34913 head=c7780ed427bbed31ee0c430a5594ed5ea4c7d5b5
Theorem: Theorem 21.3
Every complete intersection local ring is Gorenstein.
Formalized. Mathlib/RingTheory/CompleteIntersection/Gorenstein.lean::IsCompleteIntersectionLocalRing.isGorenstein — PR #41103 proves exactly that every complete-intersection local ring is Gorenstein.
Searched: leanprover-community/mathlib4 PR #41103 head=cb5e638c184221996aa2100f6cbb7074a55795bb
Corollary: regular implies c.i. implies Gorenstein implies Cohen-Macaulay
For Noetherian local rings there is a chain of implications: regular => complete intersection => Gorenstein => Cohen-Macaulay.
Formalized. Mathlib/RingTheory/CompleteIntersection/Gorenstein.lean::IsRegularLocalRing.isCompleteIntersection, IsCompleteIntersectionLocalRing.isGorenstein; Mathlib/RingTheory/Gorenstein/CohenMacaulay.lean::IsGorensteinLocalRing.isCohenMacaulay — The PR branch contains each implication in Matsumura’s chain, with the final Gorenstein⇒Cohen–Macaulay theorem imported from the Gorenstein stack.
Searched: leanprover-community/mathlib4 PR #41103 head=cb5e638c184221996aa2100f6cbb7074a55795bb
Theorem: localisation of complete intersections
If A=R/(x_1,…,x_r) with R regular and x_i an R-sequence, then every A_p is a complete intersection. The source records Avramov’s theorem that this localization property holds for every complete intersection local ring.
Not formalized. No open/current declaration was found proving that every prime localization of a complete-intersection local ring is complete intersection. The inspected CI PR supplies quotient/completion characterizations but not this localization theorem.
Definition: Andre homology and cohomology interface
The source introduces Andre homology/cohomology groups H_n(A,B,M), H^n(A,B,M) for a ring A, A-algebra B and B-module M, as functorial invariants used to characterize regularity and complete intersections.
Not formalized. Pinned/current/open Mathlib and GitHub-wide Lean search found no André–Quillen/cotangent-complex homology framework matching the source units.
Theorem: Andre characterizations of regular and complete-intersection homomorphisms
The source records the homological criteria: vanishing of appropriate Andre homology in positive degrees characterizes regularity/formal smoothness, while vanishing from degree at least three characterizes complete intersections.
Not formalized. Pinned/current/open Mathlib and GitHub-wide Lean search found no André–Quillen/cotangent-complex homology framework matching the source units.