dimension theory on noetherian local rings.

Stream: maths

[Andrew Yang]

I would like to start developing some dimension theory of noetherian local rings. In particular, I would like to have the following definitions

• height of ideals
• krull dimension of rings and modules
• regular sequences
• length and depth of modules
• Hilbert–Poincaré series and Hilbert polynomials
• (universally) catenary rings, Cohen-Macaulay rings, and regular local rings

Along with some fundamental results like Hilbert–Serre theorem, Krull's height theorem, and the (in)equalities linking different notions of size.
I will mainly be following Atiyah-Macdonald chpt. 11 and stacks project starting from stacks#00K4.
I am wondering if there are people who has attempted this before, has suggestions before I start, or is interested in collaborating on it.

[Damiano Testa]

For regular sequences, I had started working out the API of docs#is_regular having this in mind, but never continued. I hope that it can be useful!

[Kevin Buzzard]

Do we have "length of largest chain in this poset"?

[Andrew Yang]

There is an attempt at #15026. Though I think I will develop more theory to make sure that it suits my needs before I try to push it into master.

[Yaël Dillies]

That would be nice, because I'm still not quite sure of the design.

[Kevin Buzzard]

It's one of those situations where there are probably ways to deal with the case where the answer is infinity but actually in all the applications to commutative ring theory you only care about the finite case and all the ordinal or cardinal stuff you can do will just get in the way

[Kevin Buzzard]

So you'll definitely want something which returns 0 if there's unbounded chains. Note also that there are two ways for the answer to be infinity: you can either have an infinite chain or have arbitrarily large finite chains

[Andrew Yang]

I think we would need to reason that something is finite by showing it is less than some other finite thing, so I think it would be beneficial if all the values are in $\mathbb{N}\cup\{\infty\}$ and not let finiteness be an assumption to the inequalities.

[Kevin Buzzard]

One issue about enat is that tactics like ring work less well, but maybe you won't be applying ring to krull_dimension R

[Joël Riou]

I would think it is better to start developing the API taking into consideration that the dimension might be infinite. At some point (especially when the most important results are obtained about polynomial algebras over noetherian rings), it would become interesting to introduce instances like finite_krull_dimension R, and a ℕ-valued Krull dimension for these. This means that eventually some lemmas about equalities or inequalities of dimensions would have two versions: with or without the finite dimension assumption.

[Yaël Dillies]

Height of orders is more generally important so I would vouch for a ℕ version not restricted to finite_krull_dimension.

[Jack J Garzella]

One extremely important source for standard material on Commutative Algebra, which IMO is indispensable for going in this direction, is the book Cohen-Macaulay Rings by Bruns and Herzog. This is a real good source in particular for length/depth, regular sequences, and the Cohen-Macaulay-to-regular chain of inclusions (e.g. see here)

[Jack J Garzella]

If you read the appendix of Bruns-Herzog on dimension theory, you can discover that by choosing to follow Atiyah-MacDonald / stacks project is a nontrivial mathematical choice. There are two ways of developing dimension theory, one that starts with Krull's principal ideal theorem, and one that starts with hilbert polynomials. The stacks project does the hilbert polynomial one, along with Atiyah-MacDonald and Matsumura. However, Bourbaki and Bruns-Herzog, and even Hochster's notes seem to prefer the Krull's principal ideal version, which means that perhaps this route is worth considering.

Indeed, when I was thinking about doing dimension theory in Lean, I had the vague impression that trying to do Hilbert polynomials might be finicky and the principal ideal theorem route offers a quicker path to the theorems in algebraic geometry that I'm interested in. However, I am not an expert in Commutative Algebra nor am I an expert in how finicky Lean is with combinatorial polynomial identities. Perhaps the existence of free internet sources is also a factor, though hopefully Bourbaki is reasonably easy to get one's hands on.

[Johan Commelin]

cc @Antoine Chambert-Loir

[Andrew Yang]

Thanks for the insights! I also had a bit of doubt regarding the manipulation of polynomials, formal series, and gradations in lean, and it seems to be much easier if we went directly to Krull’s principal ideal theorem.
That said, we would definitely still want Hilbert polynomials in the future, so it might still be worth checking whether that path is indeed painful.

Another reason I did not follow Bourbaki is that there doesn’t seem to be an English version of Commutative algebra chapter 8. My minimal knowledge of French couldn't help me here.

[Jack J Garzella]

I ran into the english bourbaki problem as well--I wasn't able to find an online version, but I was able to check out a physical copy from my library which had an english version of all the chapters.

Bruns-Herzog also lists some other sources which follow the principal ideal theorem perspective in that appendix.

[Adam Topaz]

Ping @Michael Blyth