dimension of a ring / topological space

Stream: maths

[Kevin Buzzard]

A discussion with my PhD student Jujian Zhang about how to define the dimension of a ring made me realise that arguably the "correct" target type for such a declaration is with_bot cardinal! For the empty ring probably has Krull dimension -infinity. I encouraged him to create a nat-valued definition but, in contrast to other "garbage in, zero out" definitions I've seen in mathlib, this one has both features of nat_degree (degree of 0 is -infty but let's call it 0) and finrank (dimension of infinite-dimensional space is +infinity but let's call it zero). This was initially funny, but it got a bit annoying when we wanted to give a name to the predicate meaning "the answer being returned is actually mathematically meaningful" -- we thought it would be "is_finite_dimensional" or some such thing, but with this zero ring nonsense it seems that a quotient of a finite-dimensional ring might not be finite-dimensional, and a subset of a finite-dimensional (in the weird alg geom sense of descending sequences of possibly non-closed points) might not be finite-dimensional.

On the other hand, when I started looking through the books I found that a lot of people (even Matsumura!) seemed to be a bit unclear about what the dimension of the 0 ring was, and contained statements of the form "Artinian rings are 0-dimensional" (something which I've believed for years but now am slightly confused about, because I'm pretty sure the zero ring is Artinian). Is there an argument which says that the zero ring is 0-dimensional? Right now I'm a bit more convinced by the -infinity definition but I think I'm open to being persuaded that 0 is also a good answer -- I'm just not going a good job of convincing myself right now. The sup of the empty set of naturals is 0, if this helps, but the sup of the empty set of integers is not. Usually I feel like I'm quite clear on this kind of empty-set-ology question but here I seem to have confused myself.

[Mario Carneiro]

Is this a case where considering the relation "degree at most n" or possibly "degree less than n" is more profitable than literally having a "degree" function?

[Kevin Buzzard]

Well funnily enough right now the only instances we have of this in mathlib are "dimension <= 0" and "dimension <= 1"

[Adam Topaz]

Should we have a “krull dimension type” similar to cardinals and ordinals, where the krull dimension of arbitrary powers takes values? And get naturals out of this type, again similar to card/ords?

[Adam Topaz]

Maybe it would just be the type of cardinals at the end of the day…

[Adam Topaz]

Powers = posets (stupid autocomplete)

[Kevin Buzzard]

My point is that it would not be cardinals, it would be with_bot cardinals precisely because of the empty poset. Unless someone convinces me otherwise.

[Adam Topaz]

But there are instances where getting a precise cardinal makes sense

[Adam Topaz]

Like the dimension of a vector space as the krull dim of the poset of subspaces

[Kevin Buzzard]

Yes but you don't care about them when you're proving things about algebraic varieties and it would just be a mess. So I could imagine one "proper" one taking values in with_bot (cardinals) and which nobody ever used, and then the useful one taking values in nat.

[Kevin Buzzard]

We already have module.rank taking values in cardinals, but vector spaces can't be empty :-)

[Adam Topaz]

Here’s one: the lattice of relatively algebraically closed subextensions of some field extension is the transcendence degree, and we probably want that to be a cardinal for various reasons (e.g from model theory), and we also want to relate that to dims of algebraic varieties

[Adam Topaz]

I guess I’m proposing a general notion of krull dimension for posets (maybe posets with a bottom, to avoid empty nonsense)

[Eric Wieser]

Kevin Buzzard said:

We already have module.rank taking values in cardinals, but vector spaces can't be empty :-)

Presumably we would need a similar with_bot approach to talk about the dimensions of affine subspaces, which can be?

[Reid Barton]

Here is what Jacob Lurie writes in HTT section 7.2.4. The Heyting dimension generalizes the Krull dimension for noetherian spaces.

We next define the dimension of a Heyting space. The definition is recursive. Let α be an ordinal.
A Heyting space X has Heyting dimension ≤ α if and only if, for any compact open subset U ⊆ X, the
boundary of U has Heyting dimension < α (we note that the boundary of U is also a Heyting space); a
Heyting space has Heyting dimension < 0 if and only if it is empty

[Reid Barton]

It seems to be understood that a space has Heyting dimension $< \alpha$ if either it is empty, or it has Heyting dimension $\le \beta$ for some $\beta < \alpha$.

[Reid Barton]

In general all the notions of dimension seem to agree that the empty space has dimension $< 0$. For example $H^0(X, A) = 0$ if $X$ is empty, and we can also refine any open cover of the empty space to one in which the intersection of more than 0 of the sets is empty.

[Reid Barton]

For homotopy dimension it's literally the first example

Example 7.2.1.2. An ∞-topos X is of homotopy dimension ≤ −1 if and only if X is equivalent to the trivial ∞-category ∗ (the ∞-topos of sheaves on the empty space ∅).

[Reid Barton]

Really all these degree/dimension functions should be taking values in the collection of upwards-closed subsets of nat (or ordinal or cardinal or whatever), and we are just used to identifying that with {-1, 0, 1, ..., infty} via classical logic

[Sophie Morel]

I agree that the zero ring (or the empty scheme) should have negative dimension. Making the dimension $-\infty$ would be more logical if we want the formula for the dimension of a tensor product (resp. a product) to hold (for nice enough objects).
Funnily enough, I ran into this exact same problem a few days ago when I wanted to define the dimension of an abstract simplicial complex (I am formalizing stuff about abstract simplicial complexes for some project I have): I realized that I wanted the dimension function to have values in $\mathbb{N}\cup\{-\infty,+\infty\}$. So I looked for the definition of Krull dimension in mathlib to see how they had handled it and realized it wasn't there; then I looked at the definition of rank and realized they wouldn't have this problem because modules are always nonempty. Then I decided that I didn't feel like writing up all the basic properties of $\mathbb{N}\cup\{-\infty,+\infty\}$ like mathlib already does for $\mathbb{N}\cup\{+\infty\}$ and that both empty and infinite-dimensional complexes would have dimension 0, but that's an unsatisfactory solution. So I'll be quite interested to see what your student does, Kevin.

[Sophie Morel]

Of course the dimension of an abstract simplicial complex is just the dimension of the poset of its faces, so Adam's suggestion of defining a general notion of Krull dimension of posets would solve that problem too. Except that I would argue against forcing the posets to have bottoms, because trying to avoid "empty nonsense" would just make things more artificial in the applications to rings/simplicial complexes.

[Sebastien Gouezel]

There is also the notion of topological dimension, which is standard since the 40's and defined inductively as follows:

• the empty space has dimension -1.
• a space has dimension ≤ n if any two disjoint closed sets can be separated by a set of dimension ≤ n - 1.

The spaces of dimension 0 are the nonempty totally disconnected spaces.

[Kevin Buzzard]

My first ring theory course defined a ring to be nonzero and it was a fiasco because you could now not quotient out a ring by a general ideal.

For things like polynomial degree the advantage of the nat-valued def is that you don't have to deal with funny types where a+b=a+c doesn't imply b=c, and the cost (having to prove that various things are nonzero occasionally) seems to be worth paying (we already pay this sort of cost in field theory when dividing, and people are used to it). I use polynomial.nat_degree much more than polynomial.degree when teaching. As Reid says, the concept you often want is "degree <= n" anyway. With varieties I'm less sure that this is true in practice though. I was amused when Maria Ines explained why she was having to prove that the integers of a number field were not a field for her work on adeles. The issue is that fields are Dedekind domains in mathlib but that there are theorems (like "Dedekind domain embeds into product of completions at all height one primes) which are false for fields. I asked David Helm whether he thought fields should be Dedekind domains and his reply was "I don't even think they should be principal ideal domains", an opinion which shocked me at the time but I can see his point. There are definitely times when you want to develop a theory of 1-dimensional objects as opposed to objects of dimension <= 1.

[Mario Carneiro]

Kevin Buzzard said:

There are definitely times when you want to develop a theory of 1-dimensional objects as opposed to objects of dimension <= 1.

sure, but these could just be <=1 dimensional objects that are not <=0 dimensional

[Sophie Morel]

I think the point is to find the definitions that will cause the least pain down the road. If it means that fields have to Dedekind domains, so be it, though I don't much like it.
Ugh, this reminds me of a discussion about whether the zero ring should be considered Gorenstein. (I would say "no". Feel free to debate endlessly.)

[Johan Commelin]

Mathlib introduced notions like preconnected and preirreducible to mean "empty or actually (connected/irreducible)". Maybe a similar strategy might work here?

[Kevin Buzzard]

Fortunately mathematicians had the insight to not let 1 be a prime, but we can't really go for preDedekind domain because all the books let fields be Dedekind domains

[Adam Topaz]

Reid Barton said:

It seems to be understood that a space has Heyting dimension $< \alpha$ if either it is empty, or it has Heyting dimension $\le \beta$ for some $\beta < \alpha$.

This seems to have a similar flavor to some definitions of rank in model theory (like Morley rank for example)

[Yaël Dillies]

Let me mention it because nobody seems to have made the link, but "upwards-closed subsets of nat" is upper_set ℕ.

[Antoine Chambert-Loir]

Kevin Buzzard said:

A discussion with my PhD student Jujian Zhang about how to define the dimension of a ring made me realise that arguably the "correct" target type for such a declaration is with_bot cardinal! For the empty ring probably has Krull dimension -infinity.(...) The sup of the empty set of naturals is 0, if this helps, but the sup of the empty set of integers is not. Usually I feel like I'm quite clear on this kind of empty-set-ology question but here I seem to have confused myself.

image.png

[Antoine Chambert-Loir]

Now, my feeling is that chains should be considered as well-ordered subsets of the relevant ordered set, and that the supremum should be considered in with_bot ordinal. On the other hand, I don't believe anything has been developed in this context.

[Antoine Chambert-Loir]

(Same for length of modules : here, I know there is some literature, in particular, it is known that taking submodules or quotients can give different answers…)

[Kevin Buzzard]

Ha! Is this from your book?

[Yaël Dillies]

You know you've been away for too long when you think "Exemples" is misspelt...

[Sophie Morel]

It's Bourbaki, Algèbre commutative VIII, the first example in section 1 subsection 3 (page 7 in my edition). For them the dimension of a ring is in $\mathbb{N}\cup\{-\infty,+\infty\}$.

[Kevin Buzzard]

Yeah, if you don't care about exactly how infinite your infinite-dimensional objects are then this seems to be the pragmatic choice.

[Antoine Chambert-Loir]

Sophie Morel said:

I think the point is to find the definitions that will cause the least pain down the road. If it means that fields have to Dedekind domains, so be it, though I don't much like it.
Ugh, this reminds me of a discussion about whether the zero ring should be considered Gorenstein. (I would say "no". Feel free to debate endlessly.)

From the same authors, the answer you can guess :
image.png

[Sophie Morel]

Is Bourbaki well-known for minimizing down-the-road pain ?

[Kevin Buzzard]

It's certainly true that it often makes the same design decisions as mathlib. The question is perhaps hard to answer. One point of view is that developing some theory of topological vector spaces just so you can do integration and prove basic things such as the fundamental theorem of calculus is perhaps maximising some down-the-road pain, but if you go further down the road you realise that actually you were minimising it after all.

[Antoine Chambert-Loir]

Du miel à mes oreilles, as we say in French.