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

[Jujian Zhang]

Hilbert-Serre theorem is done here. It builds modulo linter error

[Andrew Yang]

What's the status on dimension theory? How far are we from having depth and Hilbert-Serre and Krull's height theorem in mathlib?
@Jujian Zhang @Fangming Li (John) @Brendan Seamas Murphy

[Andrew Yang]

I might try to add some results about regular local rings and its connection to smooth algebras if there aren't existing code on it.

[Brendan Seamas Murphy]

We could do just the defintion of depth/regular local rings imminently, since regular sequences exist. See Mathlib/RingTheory/Regular/. I was waiting on it because I wanted get the homological algebra sorted first, but then I got too busy irl to work on Lean stuff

[Brendan Seamas Murphy]

Not sure what the status of Hilbert-Serre or the hauptidealsatz are

[Andrew Yang]

Okay great!
But we might need the other stuff to get the equivalence between the regular sequence definition and the $\dim(R) = \dim_{k}(m/m^2)$ definition right?

[Brendan Seamas Murphy]

Yes, that's what I recall

[Brendan Seamas Murphy]

I was more focused on getting depth sensitivity of the koszul complex, the last time I thought about this stuff

[Andrew Yang]

Yeah that would be very useful too. Hope you have time to come back to this :)

[Andrew Yang]

If I use the $\dim(R) = \dim_{k}(m/m^2)$ definition I think I can still get smooth => regular & regular + dim 1 <=> DVR, which might be enough for me.

[Brendan Seamas Murphy]

Good luck! I definitely intend to, I'm just teaching a course for the first time and struggling to get anything else done

[Brendan Seamas Murphy]

I should have more time in about a month

[Kyle Trinh]

Hello, I am looking to get the height of ideals formalized, and was wondering if anyone in this thread has many any progress on that since Nov 2024.

[Johan Commelin]

Since then we had the following contribution to mathlib

rss-bot said:

feat(KrullDimension): concrete calculations (mathlib4#19210)

Part of https://github.com/leanprover-community/mathlib4/pull/15524. This adds concrete calculations of the height and Krull Dimension for Nat, Int, WithTop, WithBot and ENat.

From the Carleson project.

Authored-by: nomeata (commit)

and a thread specifically about the dimension of Dedekind rings: #mathlib4 > Dedekind ring

[Yaël Dillies]

TLDR @Andrew Yang has a series of PRs about dimension theory

[Andrew Yang]

I have a formalization of Krull's height theorem in Lean3 3 years ago and I'm trying to port it.
It is currently stuck on @Junyan Xu 's #17908 that implies artinian <=> noetherian of dim 1 though.

For FLT I also have some results on depth but not much.

But we still don't have regular local rings and it would be very nice to have them.

[Kevin Buzzard]

Oh unfortunately this traces back to #17930 with the dreaded slowdowns. Maybe it's time to get to the bottom of that.

[Junyan Xu]

There is #20421 (#count_heartbeats for all decls) which should make slowdown diagnosis much easier, but I haven't tried it on #17930 yet. (Since some shortcut instances makes some decls faters and some slower, it's particularly important to get an overall picture of the effect of every change.)

[Junyan Xu]

I've remarked here that since the slowdown is similar to the slowdown from another recently merged PR #19108 (several seconds), we should also give #17930 a green light, since it's no less important to talk about quotients by two-sided ideals freely than to allow derivatives to work on TVSs.

[Kevin Buzzard]

Yes I am actively trying to figure out how to give #17930 a green light. Maybe you want to skip the refactor, just fix the conflicts, and we ask @Michael Stoll to run his timing tools on the PR as it stands?

[Michael Stoll]

Just to clarify: What my script can do is to provide a more detailed overview of possibly relevant timing changes, given the information from the speed center. (All the information can be seen there as well, but you'd have to scroll through everying and extract it manually.) So I can run it as soon as !bench has produced output for the desired comparison.

[Junyan Xu]

It would be nice if you could run it on #20140 !

[Michael Stoll]

Done!

[Junyan Xu]

Thanks! The results you posted don't seem to show more than what the bot posts though. (The bot has been away for sometime but gladly now returned in time.)

[Michael Stoll]

The bot is basically running a very similar script; the main difference is that it does so automatically (when it is working). @Damiano Testa may know more.

[Damiano Testa]

Yes, I translated the script that Michael wrote in magma to a Lean script for the bot, staying as close as possible to the original source.

[Damiano Testa]

I think that it should be working now: there was a small adjustment to be made recently, but I hope it is running now.

[Junyan Xu]

Andrew Yang said:

I have a formalization of Krull's height theorem in Lean3 3 years ago and I'm trying to port it.
It is currently stuck on Junyan Xu 's #17908 that implies artinian <=> noetherian of dim 1 0 though.

The result is now included in #21451, which probably needs to be broken down, and we probably want to use RingKrullDimZero in #20108 / #20096 (by convention it would better be named Ring.DimensionLEZero).

(Thanks to @Kevin Buzzard and @Johan Commelin for getting #17930 into mathlib!)

[Andrew Yang]

I opened #21452 to replaced the old RingKrullDimZero PR because the latter is rotten beyond repair.

[Andrew Yang]

Not sure why it should be in the Ring namespace while ringKrullDim lives in root but I don't mind either way.

[Andrew Yang]

@Junyan Xu Does your PR imply that if A is a finite type algebra over some field K, then A is an artinian ring iff A is finite over K?

[Andrew Yang]

I can't figure out a way to use it directly so I opened #21791 for it.

[Arnav Dandu]

We're trying to define depth in terms of supremum of lengths of regular sequences, but we're having an issue with the zero ideal case. The idea was to case check on $I$, returning infinity if its the zero ideal and the supremum otherwise, but it looks like checking if $I = 0$ is not decidable in general. I feel that it could be if $R$ is Noetherian though since $I$ would be finitely generated. Have issues similar to this come up before?

[Andrew Yang]

1. Just use letI := Classical.propDecidable
2. I thought if I = 0 then depth_I(M) would be 0? (Unless when M = 0)

[Kevin Buzzard]

Yes this is commutative algebra, you don't have to worry about whether something is decidable.

[Arnav Dandu]

Great, the propDecidable works. As for depth_I(M), yes that is the correct condition, I misread. We checked if top = bot in M and that worked. Thanks!

[Junyan Xu]

I think you can just check Subsingleton M?