Chapter 4. Homological Dimension
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 11 definitions, 11 theorems, 6 propositions, 4 lemmas, 13 corollaries, 7 examples, 3 constructions, 1 convention, 2 notations and 28 other statements.
Of the 86 statements checked against Lean, 14 are formalized somewhere and 72 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 72 | 84% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 11 | 13% | Mathlib states and proves it. |
| in another Lean project | 2 | 2% | Some other Lean development has it; using it means porting that code. |
| in lean-categories | 1 | 1% | This repository states and proves it. |
| checked in total | 86 |
- Project-first search was performed at repo HEAD
f90173886bc881c2d43c0a7eb2d9fe7f110ac9a5.LeanCategories/Homological/GlobalDimension.leanowns the right global and injective-global suprema and proves the division-ring global-dimension-zero example; it explicitly does not implement weak/flat dimension.LeanCategories/Homological/IsQuasiFrobenius.leanexactly owns U017.LeanCategories/Homological/IsHereditary.leanowns the right-hereditary predicate but not the full comparison bundle in U027 nor the global-dimension theorem U028. No project implementation of Koszul complexes, Cohen–Macaulay/Gorenstein theory, von Neumann regular rings, or local cohomology comparisons closes the remaining rows. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. The positive P routes were declaration-probed successfully in the project environment. P supplies semisimple rings/Wedderburn–Artin/Maschke (U014–U015), polynomial scalar extension (U035), commutative-local and noncommutative Jacobson/Nakayama theory (U039–U041), finite-projective local freeness (U042), lifting freeness through a regular element (U044), the same-ring projective-dimension formula for quotienting a module by a regular element (U046), local/residue-field conventions (U047), and the regular-local definition/cotangent-space characterization (U048). - The chapter retains Weibel’s arbitrary-associative-ring convention until the source explicitly specializes. This matters for U001–U013 and the first change-of-rings blocks. P/H
Module.Flatand the Ext-form Baer theorem discussed below are commutative-base interfaces; a commutative specialization is not credited for an arbitrary-ring row. In particular, current Mathlib’sModuleCat.injective_iff_subsingleton_ext_quotient_oneis under[CommRing R], whereas U013 is stated for arbitrary associative rings and left ideals. P has the arbitrary-ring Baer extension criterion but not its Ext quotient reformulation, and targeted external search found no noncommutative Ext-form owner, so U013 remains unmatched. - Current Mathlib was rechecked immediately before promotion at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f. H addsMathlib/Algebra/Category/ModuleCat/Ext/Baer.leanand module-category projective/injective-dimension transport/localization files, but these do not fill the arbitrary-ring global/weak-dimension theory, residue-field Ext/Tor criteria, Auslander–Buchsbaum, Koszul, Gorenstein, or regular-local-UFD gaps.Mathlib/Algebra/Homology/LocalCohomology.leanstill explicitly lists equivalence with right-derived torsion, Koszul-limit, and Čech constructions as future work.Mathlib/RingTheory/RegularLocalRing/Defs.leanstill explicitly lists localization of regular local rings as TODO. - Mathlib PR
[#26218](https://github.com/leanprover-community/mathlib4/pull/26218)was rechecked open at head2a84ea75981e352045999fd11bc7ef6b8fab549fimmediately before promotion. ItsMathlib/RingTheory/Depth/Basic.lean,Depth/Rees.lean, andCohenMacaulay/Basic.leandefine depth via Ext, prove the regular-sequence/Rees characterizations, and define local Cohen–Macaulayness. These exact revision-specific files own U050 and U055 and are recorded asreference-port, never as pinned Mathlib. The related polynomial-CM PR[#28599](https://github.com/leanprover-community/mathlib4/pull/28599)is also still open at headfb96036190226357c7ee4450b46e9419df085bc5; it was inspected but does not by itself close another whole C04 row. - The current
tom111/BEI-leanhead5b3ddff1ffac4a12d16da43df6fc443501f4d680contains downstream/backported Cohen–Macaulay files corresponding to those open Mathlib PRs. Because the upstream open PRs are the revision authority, no C04 route is attributed to the downstream copy. - Koszul/DG search was refreshed on 2026-09-06. Current
TauCetiProject/TauCeti@37146f896b5c2969797ee836c8723bacf549d0f7(Apache-2.0) hasTauCeti.IsDGAlgebrawith square-zero differential and the graded Leibniz rule, but no checked graded-commutative-algebra predicate completing U071. Currentkbuzzard/xena@268b3bab45ba8fbed09b45cbbdc80a3813f73b5econtains an older CDGA example with graded commutativity, but the current repository exposes no license file, so it is not an acceptable reference-port source. No checked external Koszul complex/resolution/limit development matching U068–U075 or U080–U084 was found. - Auslander–Buchsbaum/regular-local-UFD search was also refreshed. Current
Brian-Nugent/Nugent_Lean@0c86a5f27b2b4cc13c54584815af8f6b6eab9c73advertises the relevant regular-local criterion/UFD endpoint, butLeanMath/RLR=UFD/Testing.leanstill contains multiple unresolvedsorryholes and the repository tree exposes no license file. It is not a proved or acceptable mapping route. Targeted current/external search found no completed replacement for U063–U067. - Semisimple theory is not used to over-credit ring-dimension rows. P proves every module over a semisimple ring projective and injective, but U016 additionally bundles ring global dimension, Tor/weak dimension, and arbitrary-ring flatness. Since the corresponding ring-dimension APIs are not formalized in the source generality, U016 remains unmatched under strict bundle semantics. The same rule is applied throughout to change-of-rings, hereditary, and regular-local rows: adjacent ingredients do not count without a checked whole-row theorem or assembly.
Ndenotes dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, open PRs, indexed GitHub search, and the relevant external repositories above. A commutative-only specialization of an arbitrary-ring theorem, an incomplete/sorry-containing development, unlicensed code, or a subset of a multi-clause source bundle is not credited.
Definitions 4.1.1 — Projective, injective, and flat dimensions
For a right R-module A, pd(A), id(A), and fd(A) are the minimum lengths of projective, injective, and flat resolutions respectively, or infinity if no finite such resolution exists.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P owns projectiveDimension and injectiveDimension, but neither project nor P/H defines flat dimension for Weibel’s arbitrary associative-ring modules; the three-definition bundle is incomplete.
Global Dimension Theorem 4.1.2 — Equivalent definitions of right global dimension
The suprema of injective dimensions, projective dimensions, pd(R/I) over right ideals, and degrees d with some Ext_R^d(A,B) nonzero agree; their common value is r.gl.dim(R).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — LeanCategories defines suprema of projective/injective dimensions, but no checked project/P/H/current/external theorem proves the four source suprema agree, including quotient ideals and nonzero Ext degrees.
Definition/comparison — Left global dimension and comparison with right global dimension
Defines l.gl.dim(R) analogously; it equals r.gl.dim(R) for commutative rings and also for left-and-right noetherian rings, with Osofsky’s bound under generator-cardinality hypotheses.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — The project owns only right global dimension. No checked left-global-dimension owner or left/right equality theorem with the source Noetherian/cardinality comparisons was found.
Tor-dimension Theorem 4.1.3 — Equivalent definitions of Tor/weak dimension
The suprema of flat dimensions on either side, flat dimensions of quotient modules by one-sided ideals, and degrees d with some Tor_d^R(A,B) nonzero agree; the common value is Tor-dimension (weak dimension).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P/H lack flat dimension and arbitrary-ring balanced Tor, so none of the source weak-dimension suprema/equivalences is represented as a whole.
Example 4.1.4 — Dimensions of fields, Z, and Z/m
Fields have global and Tor dimension 0; Z has both equal to 1; if p² divides m, Z/m has both dimensions infinite.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — The project proves global dimension zero for division rings, but the row also computes both global and Tor dimensions of ℤ and ℤ/m, including the infinite case; those computations are not formalized.
Reusable comparison — Flat versus projective dimension
For every module fd(A)≤pd(A), hence Tor-dim(R)≤r.gl.dim(R); equality need not hold for individual modules (e.g. Q over Z).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Projective modules are flat only in the available commutative flatness layer, while the source is arbitrary-ring and also includes the strict ℚ/ℤ comparison; no whole-row owner was found.
Proposition 4.1.5 — Noetherian rings: finite-generation dimensions and ring dimensions agree
If R is right noetherian, fd(A)=pd(A) for finitely generated A, and Tor-dim(R)=r.gl.dim(R).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P/H have commutative finitely-presented-flat/projective results, but the source right-Noetherian arbitrary-ring equality fd=pd and ring weak/global equality are not formalized.
pd Lemma 4.1.6 — Characterizations of bounded projective dimension
pd(A)≤d iff all Ext_R^n(A,B) vanish for n>d, iff Ext_R^{d+1}(A,B)=0 for all B, iff every d-th syzygy in a projective resolution is projective.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P defines projective dimension by Ext vanishing and proves the first two Ext criteria, but no checked declaration/assembly proves the source “every d-th syzygy in a projective resolution is projective” equivalence.
Example 4.1.7 — Projective dimension of Z/p over three base rings
For A=Z/p, pd is infinite over Z/p², zero over Z/p, and one over Z.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked calculation gives the three stated projective dimensions of ℤ/p over ℤ/p², ℤ/p, and ℤ.
id Lemma 4.1.8 — Characterizations of bounded injective dimension
id(B)≤d iff Ext_R^n(A,B)=0 for all n>d and all A, iff Ext_R^{d+1}(A,B)=0 for all A, iff the d-th cosyzygy in any injective resolution is injective.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P defines injective dimension by Ext vanishing and proves the first two Ext criteria, but no checked declaration/assembly proves the source d-th cosyzygy criterion.
Example 4.1.9 — Injective dimension of Z/p over three base rings
For B=Z/p, id is infinite over Z/p², zero over Z/p, and one over Z.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked calculation gives the three stated injective dimensions of ℤ/p.
fd Lemma 4.1.10 [OCR: 4.1.1o] — Characterizations of bounded flat dimension
fd(A)≤d iff Tor_n^R(A,B)=0 for all n>d and all left B, iff Tor_{d+1} vanishes for all B, iff every d-th syzygy in a flat resolution is flat.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P/H lack flat dimension and the arbitrary-ring Tor-resolution layer required for all three source equivalences.
Lemma 4.1.11 — Baer criterion in Ext form
A left R-module B is injective iff Ext_R^1(R/I,B)=0 for every left ideal I.
Not formalized. partial: P Module.Baer.iff_injective; H Mathlib/Algebra/Category/ModuleCat/Ext/Baer.lean::ModuleCat.injective_iff_subsingleton_ext_quotient_one for commutative rings — P has Baer’s extension criterion for arbitrary rings, and H adds the Ext-quotient equivalence only under [CommRing R]. Weibel’s row is for an arbitrary associative ring and left ideals, so the current theorem is too narrow; targeted external search found no noncommutative Ext-form owner.
Definition 4.2.1 — Semisimple ring
R is right semisimple when every right ideal is a direct summand of R, equivalently R is the direct sum of its minimal ideals.
Formalized. Mathlib/RingTheory/SimpleModule/Basic.lean::IsSemisimpleRing; IsSemisimpleRing.isSemisimpleModule — IsSemisimpleRing R is semisimplicity of the regular module; the pinned semisimple-module API gives the direct-summand/minimal-simple decomposition characterizations used by the source.
Searched: P
Named comparison — Wedderburn classification and Maschke example for semisimple rings
Semisimple rings are finite products of matrix rings over division rings; right and left semisimplicity agree and such rings are noetherian. For finite G, k[G] is semisimple when the characteristic of k does not divide the order of G.
Formalized. IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing; isSemisimpleRing_mulOpposite_iff; Noetherian instances; Mathlib/RepresentationTheory/Maschke.lean — Pinned Wedderburn–Artin gives finite products of matrix rings over division rings and left/right symmetry; the same semisimple API gives Noetherianity, and Maschke supplies the finite group-algebra example.
Searched: P
Theorem 4.2.2 — Characterizations of semisimple rings
Semisimplicity is equivalent to global dimension 0, every module projective, every module injective, and—under noetherianity—every module flat or Tor-dimension 0.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Pinned semisimple theory proves every module projective/injective, but the row also identifies ring global/Tor dimensions and arbitrary-ring flatness; those dimension notions/theorems are not all available.
Definition 4.2.3 — Quasi-Frobenius ring
A ring is quasi-Frobenius when it is left and right noetherian and R is injective as both a left and right module over itself.
Formalized. LeanCategories/Homological/IsQuasiFrobenius.lean::LeanCategories.Homological.IsQuasiFrobenius — The project predicate is exactly left/right Noetherianity plus self-injectivity of the regular module on both sides.
Searched: repo HEAD
Theorem 4.2.4 — Faith–Walker characterizations of quasi-Frobenius rings
Quasi-Frobenius is equivalent, on either side, to every projective module being injective and to every injective module being projective.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked project/P/H/current/external implementation of the Faith–Walker equivalence between quasi-Frobenius, projective→injective, and injective→projective modules was found.
Definition 4.2.5 — Frobenius algebra
A finite-dimensional k-algebra R is Frobenius when R≅Hom_k(R,k) as right R-modules; such algebras are quasi-Frobenius.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No acceptable Lean owner defines a finite-dimensional Frobenius algebra by the right-module dual isomorphism and proves the quasi-Frobenius consequence. Mathlib’s RingTheory/Frobenius.lean concerns Frobenius elements, not Frobenius algebras.
Proposition 4.2.6 — Finite group algebras are Frobenius
For a finite group G and field k, k[G] is a Frobenius algebra, via the coefficient-of-identity pairing.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked theorem constructs the coefficient-of-identity self-duality of a finite group algebra as a Frobenius algebra.
Vista 4.2.7 — Gorenstein rings and dimension-zero comparison
For commutative noetherian R, Gorenstein means id_R(R)<∞; in the stated comparison, quasi-Frobenius rings are precisely dimension-zero Gorenstein rings, with the local annihilator criterion recorded.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P/H/current indexed search found no commutative Gorenstein-ring predicate/theorem bundle matching the finite self-injective-dimension definition and dimension-zero quasi-Frobenius comparison.
Definition — Von Neumann regular ring
R is von Neumann regular if for every a∈R there exists x∈R with axa=a.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked project/P/H/current/external definition of von Neumann regular rings in the source sense ∀a, ∃x, a*x*a=a was found.
Reusable comparison — Commutative von Neumann regular versus semisimple
A commutative ring is von Neumann regular iff it is reduced and has Krull dimension zero; a commutative semisimple ring is a finite product of fields.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Without a von Neumann-regular owner, the reduced + Krull-dimension-zero characterization is not represented; semisimple finite-product-of-fields is only the adjacent half.
Lemma 4.2.8 — Finitely generated ideals in von Neumann regular rings
If R is von Neumann regular, every finitely generated right ideal is eR for an idempotent e; hence it is projective and a direct summand of R.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked source-general theorem gives idempotent generation/projectivity of finitely generated right ideals in von Neumann regular rings.
Theorem 4.2.9 — Characterizations of von Neumann regular rings
R is von Neumann regular iff Tor-dim(R)=0, iff every R-module is flat, iff R/I is projective for every finitely generated ideal I.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — The source equivalence uses arbitrary-ring flatness/Tor dimension plus quotient projectivity; no checked whole bundle exists in P/H/current/external work.
Reusable comparison — Tor dimension can be strictly smaller than global dimension
Noetherian von Neumann regular rings are semisimple, but non-noetherian examples show Tor-dim(R)<gl.dim(R) can occur.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked non-Noetherian von Neumann regular example or strict weak/global-dimension comparison was found.
Definition 4.2.10 — Hereditary ring
R is right hereditary if every right ideal is projective; commutative hereditary domains are Dedekind domains, and PIDs and semisimple rings are examples.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — LeanCategories owns the right-hereditary predicate, but the same row also packages the Dedekind-domain characterization and PID/semisimple examples; no checked whole-row assembly was found.
Theorem 4.2.11 — Hereditary iff global dimension at most one
R is right hereditary iff r.gl.dim(R)≤1.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — LeanCategories defines right hereditary and right global dimension, but no checked theorem identifies hereditary rings with right global dimension ≤1.
General Change of Rings Theorem 4.3.1 — Projective dimension under restriction of scalars
For f:R→S and an S-module A, pd_R(A)≤pd_S(A)+pd_R(S).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked project/P/H/current/external theorem proves the arbitrary-ring restriction-of-scalars bound pd_R A ≤ pd_S A + pd_R S.
Example 4.3.2 — Strictness in the general change-of-rings bound
If R is a field and pd_S(A)≠0, the general change-of-rings inequality is strict.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — The strictness example depends on the missing general change-of-rings theorem and no separately formalized example was found.
Reusable comparison — Regular quotient as equality case
Highlights S=R/xR for a nonzerodivisor x as an important case where the change-of-rings bound becomes an equality.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Pinned regular-element projective-dimension results are commutative-local and do not establish the source arbitrary central quotient equality case.
First Change of Rings Theorem 4.3.3 — Projective dimension after quotient by a nonzerodivisor
If x is central and a nonzerodivisor on R, and nonzero A is an R/x-module with finite pd_{R/x}(A), then pd_R(A)=1+pd_{R/x}(A).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked arbitrary-ring first change-of-rings equality between pd_R A and pd_{R/x} A was found.
Example 4.3.4 — Finite-dimension hypothesis in first change of rings is necessary
pd_{Z/4}(Z/2)=∞ while pd_Z(Z/2)=1, so the first change-of-rings conclusion fails without finite pd over the quotient.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked explicit ℤ/4 versus ℤ projective-dimension counterexample is formalized.
Second Change of Rings Theorem 4.3.5 — Quotient dimension when x is regular on A
If x is central and a nonzerodivisor on both R and A, then pd_R(A)≥pd_{R/x}(A/xA).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked second change-of-rings inequality comparing projective dimensions over R and R/x was found.
Notation/construction — Polynomial extension A[x]
For an R-module A, writes A[x]=R[x]⊗_R A as an R[x]-module.
Formalized. Mathlib/Algebra/Polynomial/Module/TensorProduct.lean::PolynomialModule.polynomialTensorProductLEquivPolynomialModule — Pinned Mathlib identifies R[X] ⊗[R] A with the polynomial module A[X], exactly the source scalar-extension construction and coefficient action.
Searched: P
Corollary 4.3.6 — Polynomial extension preserves projective dimension
pd_{R[x]}(A[x])=pd_R(A) for every R-module A.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P constructs polynomial extension of modules, but no checked theorem identifies pd_{R[X]}(A[X]) with pd_R(A).
Theorem 4.3.7 — Global dimension of a polynomial ring
gl.dim(R[x_1,…,x_n])=n+gl.dim(R), with the one-variable proof using the canonical two-term induced-module resolution of any R[x]-module.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Neither project nor P/H exports ring global-dimension behavior under polynomial extension; the canonical two-term induced-module resolution theorem is also absent.
Corollary 4.3.8 — Hilbert syzygy theorem
For a field k, k[x_1,…,x_n] has global dimension n; thus the (n−1)-st syzygy of every module is projective.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked Hilbert-syzygy/global-dimension theorem for polynomial rings was found.
Nakayama’s Lemma 4.3.9 — Nakayama lemma for a commutative local ring
For nonzero finitely generated B over local (R,m), B≠mB; more generally B=A+mB implies A=B.
Formalized. Mathlib/RingTheory/Nakayama.lean::Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator; Submodule.le_of_le_smul_of_le_jacobson_bot; IsLocalRing.maximalIdeal_le_jacobson — Specializing the Jacobson forms to the maximal ideal of a commutative local ring gives both B≠mB for nonzero finite B and B=A+mB ⇒ A=B.
Searched: P
Definition — Jacobson radical
J={r∈R : 1-rs is a unit for every s∈R} is a two-sided ideal, called the Jacobson radical.
Formalized. Mathlib/RingTheory/Jacobson/Radical.lean::Ring.jacobson; Mathlib/RingTheory/Jacobson/Ideal.lean::TwoSidedIdeal.jacobson; TwoSidedIdeal.mem_jacobson_iff — Pinned Mathlib has the Jacobson radical for arbitrary rings as a two-sided ideal with the standard unit characterization, equivalent to the source sign convention.
Searched: P
General Version of Nakayama’s Lemma 4.3.10 — Nakayama lemma with the Jacobson radical
For nonzero finitely generated B and the Jacobson radical J of R, B≠JB.
Formalized. Mathlib/RingTheory/Jacobson/Radical.lean::Submodule.FG.jacobson_smul_lt; Submodule.FG.eq_bot_of_le_jacobson_smul — The pinned file explicitly labels the latter as Nakayama for modules over noncommutative rings; for nonzero finitely generated B, Jacobson multiplication is a strict submodule, hence B≠JB.
Searched: P
Proposition 4.3.11 — Finitely generated projectives over local rings are free
Every finitely generated projective module over a commutative local ring is free.
Formalized. Mathlib/RingTheory/LocalRing/Module.lean::Module.free_of_flat_of_isLocalRing; Module.Flat.of_projective — A finitely generated projective module is flat, and pinned local-ring theory proves every finite flat module over a commutative local ring is free.
Searched: P
Third Change of Rings Theorem 4.3.12 — Equality of projective dimensions under regular reduction
For commutative noetherian local (R,m), finitely generated A, and x∈m a nonzerodivisor on both A and R, pd_R(A)=pd_{R/x}(A/xA).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P proves projective-dimension change under quotienting a module by a regular element over the same ring, but not the source equality with projective dimension over the quotient ring R/x.
Lemma 4.3.13 — Lifting freeness across a regular element
Under the hypotheses in the third change-of-rings theorem, if A/xA is free over R/x, then A is free over R.
Formalized. Mathlib/RingTheory/Regular/Free.lean::Module.free_quotSMulTop_iff_free — For a finite-presentation module and a regular element in the Jacobson radical, freeness modulo the element is equivalent to freeness. Source Noetherian finite hypotheses imply finite presentation.
Searched: P
Reusable comparison — Generalized third change-of-rings theorem
The third change-of-rings theorem remains valid for right noetherian R when x is central and lies in the Jacobson radical.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — The generalized noncommutative right-Noetherian/Jacobson-radical third change-of-rings theorem is not represented by P/H/current/external work.
Corollary 4.3.14 — Projective dimension of A/xA over R
Under the local noetherian regular-element hypotheses and pd_R(A)<∞, pd_R(A/xA)=1+pd_R(A).
Formalized. Mathlib/RingTheory/Regular/ProjectiveDimension.lean::ModuleCat.projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular — Under the source commutative Noetherian local regular-element hypotheses, pinned Mathlib gives pd_R(A/xA)=pd_R(A)+1; it does not require the source’s extra finiteness of pd_R(A).
Searched: P
Convention — Local rings and residue fields in §4.4
Throughout the section, local ring means commutative noetherian local ring with unique maximal ideal m; k=R/m denotes its residue field.
Formalized. IsLocalRing; IsNoetherianRing; IsLocalRing.maximalIdeal; Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean::IsLocalRing.ResidueField; residue — Pinned Mathlib has exactly the commutative Noetherian local-ring data, maximal ideal, and quotient residue field used throughout §4.4.
Searched: P
Definitions 4.4.1 — Krull dimension, embedding dimension, and regular local ring
dim(R) is maximal prime-chain length; emb.dim(R)=dim_k(m/m²); a local ring is regular when dim(R)=emb.dim(R).
Formalized. Mathlib/RingTheory/RegularLocalRing/Defs.lean::IsRegularLocalRing; isRegularLocalRing_iff; IsRegularLocalRing.iff_finrank_cotangentSpace — Pinned regular local rings are Noetherian local rings with minimal-generator/cotangent-space dimension equal to Krull dimension, exactly the source definition.
Searched: P
Examples 4.4.2 — Standard regular local rings
Dimension-zero regular local rings are fields; dimension-one ones are DVRs; formal power-series and localized polynomial rings at their homogeneous maximal ideals give regular local rings of dimension n; smooth local coordinate rings are regular.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P covers fields/DVRs and polynomial regularity pieces, but not the full source example bundle including power-series and smooth-local examples.
More Definitions 4.4.3 — Regular sequences, grade, and Cohen–Macaulay rings
Defines an A-regular sequence in m by successive nonzerodivisor conditions, grade G(A) as maximal length, and Cohen–Macaulay local rings by G(R)=dim(R).
Formalized. leanprover-community/mathlib4#26218@2a84ea75981e352045999fd11bc7ef6b8fab549f::Mathlib/RingTheory/Depth/Basic.lean; Depth/Rees.lean; CohenMacaulay/Basic.lean — The open PR defines module/ideal/local depth by Ext, proves the regular-sequence supremum/Rees characterization, and defines Cohen–Macaulay local rings by depth = dimension. P separately owns regular sequences. The PR remains open, so this is revision-specific reference material.
Searched: PR #26218
Examples 4.4.4 — Cohen–Macaulay versus regular local examples
Gives dimension-zero and one-dimensional examples separating Cohen–Macaulayness from regularity, including kx²,x³.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked realization of the cusp/nonregular CM examples and the stated non-CM examples was found.
Proposition 4.4.5 — Regular local rings are domains
Every regular local ring is an integral domain.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked theorem states that a regular local ring is a domain in the source form.
Corollary 4.4.6 — Regular local rings are Cohen–Macaulay via parameter sequences
If R is regular local and x_1,…,x_d map to a basis of m/m², they form an R-regular sequence and G(R)=dim(R).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P lacks Cohen–Macaulay; PR #26218 defines CM/depth but has no theorem IsRegularLocalRing → IsCohenMacaulayLocalRing or source regular-sequence construction.
Standard Facts 4.4.7 — Associated-prime facts used for grade
If every element of m is a zerodivisor on finitely generated A, then k embeds in A; when G(A),G(R)>0 one can choose x∈m∖m² regular on both, and a regular x lowers Krull dimension by one.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — PR #26218 contains associated-prime/depth infrastructure, but no checked whole theorem gives all three source clauses, especially a maximal-ideal element regular simultaneously on A and R.
Theorem 4.4.8 — Grade via Ext from the residue field
Every maximal A-regular sequence has length G(A), and G(A) is the least n with Ext_R^n(k,A)≠0.
Formalized. leanprover-community/mathlib4#26218@2a84ea75981e352045999fd11bc7ef6b8fab549f::Mathlib/RingTheory/Depth/Basic.lean::ModuleCat.moduleDepth_eq_iff; IsLocalRing.depth_eq_sSup_length_regular; Mathlib/RingTheory/Depth/Rees.lean::ModuleCat.exists_isRegular_tfae — The open PR identifies depth/grade with the least nontrivial Ext degree and with the supremum/attained lengths of regular sequences, matching the source local finite-module characterization.
Searched: PR #26218
Reusable comparison — Injective dimension as the top nonzero Ext from k
For finitely generated A over a local ring, id(A) is the largest n with Ext_R^n(k,A)≠0; the following theorem supplies the cited criterion.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked theorem identifies finite injective dimension with the top nonzero Ext_R^n(k,A) degree.
Theorem 4.4.9 — Injective dimension detected by the residue field
For local R and finitely generated A, id(A)≤d iff Ext_R^n(k,A)=0 for all n>d.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked criterion id(A)≤d ↔︎ Ext_R^n(k,A)=0 for all n>d was found in P/H or current Baer/injective-dimension files.
Corollary 4.4.10 — Gorenstein local rings are Cohen–Macaulay
If id_R(R)<∞, then G(R)=id_R(R)=dim(R), and Ext_R^q(k,R) is nonzero exactly in degree dim(R).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked Gorenstein-local theorem identifies self-injective dimension, grade/depth, Krull dimension, and the single nonzero residue-field Ext degree.
Proposition 4.4.11 — Projective dimension detected by Tor with the residue field
For finitely generated A over local R, pd(A)≤d iff Tor_{d+1}^R(A,k)=0; thus pd(A) is the largest d with Tor_d^R(A,k)≠0.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — The source projective-dimension criterion is via Tor with the residue field; P/H lack the needed source-general Tor theorem.
Corollary 4.4.12 — Global dimension of a local ring
For local R, gl.dim(R)=pd_R(k), where k=R/m.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — The project defines right global dimension, but no checked local theorem reduces it to the projective dimension of the residue field.
Corollary 4.4.13 — Global dimension under a regular quotient
For local R and a nonzerodivisor x∈m, either gl.dim(R/xR)=∞ or gl.dim(R)=1+gl.dim(R/xR).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked theorem gives the source alternative gl.dim(R/x)=∞ or gl.dim(R)=1+gl.dim(R/x).
Grade 0 Lemma 4.4.14 [statement truncated in extraction] — Finite projective dimension at grade zero
The extracted statement is truncated after its hypotheses; the surviving proof establishes that if G(R)=0 and finitely generated A has finite projective dimension, then pd(A)=0 (so A is projective/free).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked Grade-0 finite-projective-dimension lemma was found; the frozen source row is itself truncated, so no stronger statement is inferred.
Theorem 4.4.15 — Auslander–Buchsbaum equality
For local R and finitely generated A with pd(A)<∞, G(R)=G(A)+pd(A).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No completed Lean proof of Auslander–Buchsbaum was found. The Nugent external hit advertises this material but its relevant endpoint file contains sorry holes and is not a usable formalization.
Main Theorem 4.4.16 — Regular local iff finite global dimension
A local ring is regular iff gl.dim(R)<∞; then G(R)=dim(R)=emb.dim(R)=gl.dim(R)=pd_R(k).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked Auslander–Buchsbaum–Serre theorem identifies finite global dimension, regularity, and the common numerical dimension.
Corollary 4.4.17 — Regular local rings are Gorenstein and Cohen–Macaulay
A regular ring in the section’s local sense is both Gorenstein and Cohen–Macaulay.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Gorenstein is absent from P/H and the open CM PR does not supply the source regular-local → Gorenstein theorem.
Corollary 4.4.18 — Localization preserves regularity
If R is regular local and p is prime, R_p is regular local; more generally the proof shows localizations have finite global dimension.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — RegularLocalRing/Defs.lean explicitly lists localization of regular local rings as TODO; current H still has no replacement theorem.
Theorem 4.4.19 — Regular local rings are UFDs
Every regular local ring is a unique factorization domain.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No completed acceptable proof that regular local rings are UFDs was found; the direct Nugent candidate has unresolved sorry goals and no repository LICENSE file.
Construction — Koszul complex
For central x∈R, K(x) is 0→R→^x R→0 in degrees 1,0 with generator e_x; for a finite central sequence x=(x_1,…,x_n), K(x) is the total tensor product K(x_1)⊗…⊗K(x_n).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P/H contain regular sequences and homological complexes but no algebraic Koszul-complex construction for a central sequence.
Notation 4.5.1 — Koszul homology and cohomology
For an R-module A, H_q(x,A)=H_q(K(x)⊗_R A) and Hq(x,A)=Hq(Hom_R(K(x),A)).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Without the Koszul complex, the source Koszul homology/cohomology definitions are not represented.
Construction/comparison — Exterior-algebra description of the Koszul complex
K_p(x) is free on wedge symbols and identifies with ΛpRn; the differential is the alternating contraction by x, with K(x,y) displayed explicitly.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked exterior-algebra realization and contraction differential for the Koszul complex was found.
DG-Algebras 4.5.2 — Graded algebras and differential graded algebras
Defines graded and graded-commutative R-algebras; a DG-algebra has d²=0 and d(ab)=d(a)b+(-1)^p a d(b) for a in degree p.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Tau Ceti (Apache-2.0) defines DG algebras with square-zero differential and graded Leibniz, but does not package the row’s graded-commutative algebra condition. The older Xena CDGA example has that condition but its current repository exposes no license file; no acceptable whole-row route exists.
Lemma 4.5.3 — Künneth formula for a one-element Koszul factor
For a chain complex C and x∈R, 0→H_0(x,H_q(C))→H_q(K(x)⊗C)→H_1(x,H_{q-1}(C))→0 is exact.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked one-element Koszul Künneth short exact sequence was found.
Corollary 4.5.4 — Acyclicity of Koszul homology on a regular sequence
If x is a regular sequence on A, H_q(x,A)=0 for q≠0 and H_0(x,A)=A/xA.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked theorem proves Koszul acyclicity on a regular sequence.
Corollary 4.5.5 — Koszul resolution
If x is an R-regular sequence and I=(x_1,…,x_n), K(x) is a finite free resolution of R/I; hence Tor and Ext against R/I are computed by Koszul homology/cohomology.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked Koszul free-resolution theorem exists in P/H/current/external search.
Application 4.5.6 — Scheja–Storch Koszul proof of Hilbert syzygy
For R=F[x_1,…,x_n], the regular sequence y_i−x_i in a doubled polynomial ring yields a canonical length-n free resolution of every R-module (after the identified copy), proving gl.dim(R)=n.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked Scheja–Storch Koszul proof of Hilbert syzygy was found.
Definition 4.6.1 — Local cohomology with respect to a finitely generated ideal
For finitely generated I in commutative R, H_I0(A)={a:Ii a=0 for some i}=colim Hom(R/I^i,A); define H_Iq=RqH_I^0, equivalently colim Ext_Rq(R/Ii,A).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — P defines localCohomology as the colimit of Ext groups, but the file explicitly lists equivalence with the right-derived torsion functor as future work; the source definition bundle is incomplete.
Generalization 4.6.2 — Cohomology with supports
For closed Z⊂X, H_Z^0(X,F) is global sections supported on Z and H_Z^n its right derived functors; on Spec(R), this extends H_I^n, with the stated punctured-spectrum long exact sequence and cohomology comparison.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked derived sections-with-support functor and punctured-spectrum long exact comparison matching the source row was found.
Theorem 4.6.3 — Grade detected by local cohomology
For commutative noetherian local (R,m) and finitely generated A, G(A) is the least n with H_m^n(A)≠0.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked theorem identifies grade/depth with the least nonzero local-cohomology degree.
Application 4.6.4 — Two-dimensional local domains and Hm^1
For a two-dimensional local domain, identifies Hom_R(m^i,R) with m^{-i} in the fraction field and H_m^1(R) with C/R for C=∪m^{-i}; in the Cohen–Macaulay case this vanishes. The inline exercise clause at L3556 is not promoted.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked two-dimensional-domain calculation H_m^1(R) ≃ C/R was found.
Construction — Transition maps between Koszul complexes of powers
Natural maps K(x{i+1})→K(xi), tensorized over a sequence, induce a tower on Koszul homology and direct-system maps on Koszul cohomology after Hom(-,A).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No algebraic Koszul-complex owner exists, hence the power transition maps and induced (co)homology systems are absent.
Definition 4.6.5 — Koszul-limit local cohomology
Defines H_x^q(A)=colim_i Hq(xi,A).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — The Koszul-limit definition depends on U080 and is not formalized; Mathlib local cohomology lists the Koszul-limit characterization as future work.
Proposition 4.6.6 — Higher Koszul-homology towers are trivially Mittag–Leffler
For commutative noetherian R and finitely generated A, {H_q(x^i,A)} satisfies the trivial Mittag–Leffler condition for every q≠0.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked trivial Mittag–Leffler theorem for higher Koszul-homology towers was found.
Corollary 4.6.7 — Koszul-limit local cohomology vanishes on injectives in positive degree
For commutative noetherian R and injective E, H_x^q(E)=0 for q≠0.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked positive-degree vanishing theorem for Koszul-limit local cohomology on injectives was found.
Theorem 4.6.8 — Derived and Koszul constructions of local cohomology agree
For commutative noetherian R, x=(x_1,…,x_n), I=(x), and every A, H_Iq(A)≅H_xq(A).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — Mathlib LocalCohomology.lean explicitly lists equivalence with the limit of Koszul homology as future work, so the comparison theorem is absent.
Corollary 4.6.9 — Vanishing range for local cohomology
For noetherian local R, H_m^q(A) can be nonzero only for G(A)≤q≤dim(R); if R is Cohen–Macaulay, H_m^q(R)≠0 exactly for q=dim(R).
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked grade-to-dimension local-cohomology vanishing range or Cohen–Macaulay concentration theorem was found.
Application 4.6.10 — Hartshorne example: cohomological obstruction to two equations
For I=(x_1,x_2)∩(y_1,y_2) in C[x_1,x_2,y_1,y_2], H_I3(R)≅H_m4(R)≠0; hence the union of the two coordinate planes meeting at a point cannot be cut out by only two equations.
Not formalized. partial: adjacent dimension/commutative-algebra infrastructure — No checked Hartshorne coordinate-planes local-cohomology calculation/obstruction was found.