commutative algebra status

Stream: maths

[Neil Epstein]

Hi. I'm brand new to this, having heard an online talk by K Buzzard a week ago.

I was wondering: How much has been coded in lean4 and mathlib4 on the following:

• content of Atiyah-Macdonald
• Cohen Structure Theorem(s) for complete Noetherian local rings
• first 3 chapters of Bruns-Herzog (regular sequences, Koszul complexes, Cohen-Macaulay rings and modules, Gorenstein rings, regular rings)

Many thanks,
-Neil

[Andrew Yang]

Hi! Mathlib has no dimension theory, but everything else in Atiyah-Macdonald (except primary decomposition) should be in mathlib.

[Utensil Song]

One way to find out more specifics is to type an informal definition or statement in https://www.moogle.ai/ , check if anything in the search result looks like what you want, then search them in Mathlib4 doc and follow links to other type/definitions/theorems to see which module of Mathlib that part ends up in.

[Johan Commelin]

@Neil Epstein Concerning the Cohen Structure Theorem: I don't think we have anything, but we have "complete", "Noetherian", and "local", so that's a start :smiley:
Concerning item 3: I think we have a little bit about regular sequences (not 100% sure) and @Amelia Livingston worked on Koszul complexex. I don't think we have anything about Cohen-Macaulay or Gorenstein.

[Junyan Xu]

a start on dimension theory is #6277

[Scott Morrison]

If anyone wanted to add links to theorem numbers in Atiyah-Macdonald in the doc-strings of relevant theorems, that would be a wonderful contribution, and perhaps a good way to self-answer the question here!

[Eric Wieser]

In the same vein, it would be great if someone could teach doc-gen4 about references.bib too!

[Kevin Buzzard]

@Neil Epstein for questions about specific theorems, just type the theorem name into moogle.ai and see what it finds. I would really love to see Cohen structure theorem in lean. It's a fundamental result in commutative algebra and doing commutative algebra in lean is really fun once you get the knack of things. Why not write a blueprint? Would probably lead to an interesting paper, Exp Math told me they were interested in taking more formalisation papers.

[Neil Epstein]

Problem is, lots of theorems don't have names. Like for instance, when it comes to completion, you really need inverse limits (which are what category theorists call limits, as opposed to colimits). So for instance, we need the theorem that says that a short exact sequence of inverse systems leads to a left-exact sequence of inverse limits, which is exact if the third system is 'surjective'.

[Joël Riou]

Neil Epstein said:

Problem is, lots of theorems don't have names. Like for instance, when it comes to completion, you really need inverse limits (which are what category theorists call limits, as opposed to colimits). So for instance, we need the theorem that says that a short exact sequence of inverse systems leads to a left-exact sequence of inverse limits, which is exact if the third system is 'surjective'.

Here, the keyword would be "Mittag-Leffler". See https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/CofilteredSystem.html which contains some related material; even though the actual statement is not yet in mathlib, most of the ingredients for a formalization of the statement are ready.