Regular local rings

Stream: mathlib4

[Jarod Alper]

At the University of Washington, we are starting a small formalization project on regular local rings. The main goal is to gain more experience working with Lean, but it would be nice if we could also contribute to Mathlib.

Regular local rings are currently not defined in Mathlib. The plan is to start with the proof that regular local rings are domains, and then move on to some other relatively straightforward facts relating regular local rings and regular sequences. If we become more ambitious, it would be fun to formalize the Auslander-Buchsbaum-Serre theorem that regular local rings are characterized by finite global dimension, a result that we just covered in my graduate commutative algebra class.

If there are some people actively working on regular local rings, please let me know so that we can pivot to a different project.

[Kevin Buzzard]

@Nailin Guan is your group thinking about this?

[Thomas Browning]

I do know that @Brendan Seamas Murphy added regular sequences to mathlib a while ago (docs#RingTheory.Sequence.IsRegular), but I don't think anything further has been done in mathlib, at least.

[Jarod Alper]

Yes, I had seen that. In a comment, it says "TODO: Koszul regular sequences, H_1-regular sequences, quasi-regular sequences, depth." So we would ideally add Koszul complexes and this material as well.

[Brendan Seamas Murphy]

Yes! I am just about finishing up my semester and will get back to this in ~2 weeks

[Brendan Seamas Murphy]

Also, @Jack J Garzella and some others were working on Koszul complex stuff, but I'm not sure how far they got

[Michał Mrugała]

Here is a thread where Nailin was talking about formalizing some results about Cohen Macaulay rings and regular sequences in relation to Ext: #mathlib4 > Cohen Macaulay rings. There is a link to a github repo, so you should be able to check what's been done so far.

[Nailin Guan]

Kevin Buzzard said:

Nailin Guan is your group thinking about this?

Currently, no, I'll ask our professor about it. But we are trying to formalize Koszul complex too, maybe @Yongle Hu know more clearly about the situation. Maybe we should find another place for more detailed discussion about Koszul.

[Jz Pan]

Great work! Maybe in my Iwasawa project I need to use regular local rings, but maybe not (possibly I can use Noetherian integrally closed local rings instead).

[Filippo A. E. Nuccio]

I think that regular local rings are the right setting for many results about Iwasawa algebras, and I'd like to get a better grasp of this project.

[Filippo A. E. Nuccio]

@Jarod Alper do you have a repo with your work?