Regular Rings

Stream: mathlib4

[Nailin Guan]

We have developed some basic theory about regular ring (&regular local ring). Including:
1: definition of regular local ring as a noetherian local ring with (maximalIdeal R).spanFinrank = ringKrullDim R
2: regular local ring is domain
3: regular system of parameters is regular sequence
4: definition of regular ring as every localization at prime is regular local ring
5: polynomial over regular ring is regular
Currently only 1 is sorry free in #28682
2 and 3 depend on some arguments from Krull heights theorem, in #28683
5 depend on the results developed in dimension of polynomial, in #28684

[Nailin Guan]

We are here to announce that we have proved every finitely generated module over regular local ring has finite projective dimension in #29534 via proving maximal Cohen Macaulay module over regular local ring is free in #29533.

[Nailin Guan]

The global dimension of regular local ring is equal to its krull dimension would follow easily with previously proven Auslander-Buchsbaum theorem. However we still haven't made a good definition of projective dimension and global dimension, this part is currently left as sorries.

[Nailin Guan]

We currently use the following definition:
global dimension

def HasGlobalDimensionLE (n : ℕ) : Prop :=
  ∀ (M : ModuleCat.{v} R), HasProjectiveDimensionLE M n

noncomputable def globalDimension : ℕ∞ :=
  sInf (({(n : ℕ) | HasGlobalDimensionLE.{u, v} R n}).image WithTop.some)

projective diemsion:

noncomputable def projectiveDimension (X : C) : WithBot ℕ∞ :=
  sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < i → HasProjectiveDimensionLT X i}

noncomputable def nonnegProjectiveDimension (X : C) : ℕ∞ :=
  sInf (({(n : ℕ) | HasProjectiveDimensionLT X n}).image WithTop.some)

[Jarod Alper]

Excellent progress, Nailin! Brian Nugent @Brian Nugent and I had worked on some related properties last Spring. See conversations #new members > First Mathlib PR @ 💬 and #mathlib4 > Regular local rings @ 💬

We had proved that regular local rings are domains and some related lemmas. Just yesterday I tried to submit a PR request for our work #231956 but the build failed. But maybe this is irrelevant now anyway given your work.

However, I still would like to get a better understanding of the PR process to mathlib. I don't have a good track record with git, but I did my best to follow all the instructions and I'm not sure why it failed. I may have forgotten to run lake exe mk_all or at least that is what my copilot is saying. And now that it has failed, I am not sure what to do (presuming this is still a worthy PR). Any suggestions?

[Junyan Xu]

This is the error:
image.png
The reason is that you added files to Mathlib but didn't update Mathlib.lean. lake exe mk_all is what you need to do.

[Nailin Guan]

I need to apologize here that I replace your work in some sense. However I am really needing these constructions and your old PR seems stop updating with some results about dimension already formalized in the later updates, sorry for that.

[Nailin Guan]

However I believe your lemmas about spanRank should be in mathlib anyway. These lemmas can be in a separate (and smaller) PR so it can be reviewed more easily.

[Nailin Guan]

A small update : definition of projective dimension and global dimension is ready in #29558 and global dimension of regular local ring is ready in #29534, finite projective dimension part is separated into #29557

[Nailin Guan]

I have a question here : I currently know two definitions of regular ring, localization at all primes/all maximal ideals is regular local ring. which definition do we prefer? The first trivially imply the second, however the second implies the first needs some highly nontrivial proof (it is in our plan but may not be able to be done within the comming few months). The current advantage of the second one is that regular local ring become regular ring natrually.

[Nailin Guan]

I am here to claim that we have the other side of Auslander-Buchsbaum-Serre criterion in #29796, so the problem above is not a problem any more! More APIs is developed in the coming PR #29802.

[Nailin Guan]

The dependency graph of all the related stuffs:
7f1110a5121d401a9fdb54b30fda7a60.jpg

[Nailin Guan]

I am sorry that I am busy working on pushing forward this project ignoring the review comments, I would come back to them after finishing cleanup of the project.

[Nailin Guan]

A small update
8f744c8a87ba77d66d4300c16494cd1e.jpg

[Christian Merten]

I have to say I am quite confused by your dependency graphs. Out of the 8 PRs you show as "ready for review", only 2 are really ready for review, the rest is awaiting author or a dependent PR.

[Nailin Guan]

Sorry, I only mean by sorry free, I should make it clear.
Also, I would try to address the comments these days, sorry for the delay.

[Nailin Guan]

A small fix:
dea711e74882c5ea0123eca7197c0e8f.jpg

[Nailin Guan]

I merged the branch of #27416 into my works and rearrage the PRs, now dependency is as following:
2b73e2a4381ad2143d0f72cbdfc4b223.jpg

[Kenny Lau]

wow that's a lot of PR's

[Nailin Guan]

These in total is about 6000 lines, some adds more than 500 lines compared to previous PRs so definitely need splitting, there would be more (
But anyway, we have ABS criterion in the end.