## Stream: maths

### Topic: order on prime_spectrum

#### Johan Commelin (Feb 17 2021 at 18:57):

Do people agree that it's a good idea to turn prime_spectrum R into a poset using the specialisation order?

#### Kevin Buzzard (Feb 17 2021 at 19:00):

My instinct is that this is a good idea. However when Jason and Giulia and I bundled both subgroups and normal subgroups in our development of group theory, things got a bit annoying. So another solution is to have is_prime on ideal R and get the induced poset structure.

#### Kevin Buzzard (Feb 17 2021 at 19:02):

But I think that in general I am a bundler, and for sure we need the prime_spectrum R type, there is certainly no argument for removing it, so why not put the poset structure on it? It is of a topological nature, right? P <= Q iff Q is in the closure of {P}, right?

#### Johan Commelin (Feb 17 2021 at 19:05):

Yeah, we could make it a def for arbitrary topological spaces, and make it an instance for prime_spec

#### Damiano Testa (Feb 17 2021 at 19:20):

I fully approve of this! Even more, specialization and generalization should both be readily accessible!

#### Johan Commelin (Feb 17 2021 at 19:21):

Hmmm, they can't both be instances

#### Adam Topaz (Feb 17 2021 at 19:21):

Another +1 for this suggestion.

#### Adam Topaz (Feb 17 2021 at 19:22):

The terminology that I'm used to is that "smaller" means "closer to the generic point".

#### Adam Topaz (Feb 17 2021 at 19:23):

So I guess that corresponds to $a \le b$ iff $b$ is a specialization of $a$.

#### Damiano Testa (Feb 17 2021 at 19:23):

Ok, I really really think that being able to work with an order and its dual is something that I need to understand better, then!

#### Damiano Testa (Feb 17 2021 at 19:25):

I guess which one of the convention on the order we adopt is secondary: in my mind, points are smaller than curves and so on, but their ideals go the opposite way. So it is simply a matter of remembering whether we think geometrically or algebraically

#### Johan Commelin (Feb 17 2021 at 19:26):

We can work with order_dual (prime_spectrum R) to get the other ordering... but I think you have already discovered that this isn't always an optimal experience.

#### Damiano Testa (Feb 17 2021 at 19:26):

Yes, I will avoid order dual... Ahaha

#### Johan Commelin (Feb 17 2021 at 19:27):

I also don't have a strong opinion on which order to choose

#### Adam Topaz (Feb 17 2021 at 19:28):

Damiano Testa said:

I guess which one of the convention on the order we adopt is secondary: in my mind, points are smaller than curves and so on, but their ideals go the opposite way. So it is simply a matter of remembering whether we think geometrically or algebraically

the way I think of it is in terms of valuations. A point on a surface is an equivalence class of flags of points on curves, hence it's "more" information than just a curve.

#### Damiano Testa (Feb 17 2021 at 19:28):

Since we are building stuff from the algebraic side, using ideals, it might make sense to have the order on points match the one on ideals?

#### Adam Topaz (Feb 17 2021 at 19:29):

And the generic point corresponds to the trivial valuation, hence it's "the smallest"

#### Kevin Buzzard (Feb 17 2021 at 19:30):

The correct solution is to choose one, and make order_dual work. Damiano had a bad experience with it, but if you're principled about whether (a : X) or (a : order_dual X) things work out -- this was my experience with multiplicative anyway. It's the moment you start abusing type equality that you get into problems.

#### Damiano Testa (Feb 17 2021 at 19:30):

Which incidentally matches the one that Adam suggests: minimal ideals correspond to irreducible components, maximal ideals to points

#### Kevin Buzzard (Feb 17 2021 at 19:31):

The CS people love abusing their type equality because it makes proofs look slicker, but order_dual should be irreducible and then abuse is banned.

#### Damiano Testa (Feb 17 2021 at 19:32):

I am happy to learn to use order dual and would really think that it can be used a lot. Not by me, at the moment, though!

#### Kevin Buzzard (Feb 17 2021 at 19:32):

I would vote for

inductive order_dual (X : Sort*)
| dual_of (x : X) : order_dual


#### Kevin Buzzard (Feb 17 2021 at 19:32):

and my understanding is that this is the preferred solution in Lean 4.

#### Adam Topaz (Feb 17 2021 at 19:33):

Wont this be terrible to work with if you want to take the order dual of the order dual (and have it "agree" with the original thing)?

#### Kevin Buzzard (Feb 17 2021 at 19:33):

Leaks are the problem, when accidentally you have a : X and b : order_dual X and a <= b and you have no idea what <= means. With the new inductive definition this literally cannot happen.

#### Kevin Buzzard (Feb 17 2021 at 19:34):

We have this with multiplicative and additive, and we just have equivs.

#### Kevin Buzzard (Feb 17 2021 at 19:35):

it's an order isomorphism, and we need a robust machinery for moving structures across isomophisms, and if we start writing principled code like this then eventually our wishes and dreams about what we actually want for such a tactic will become clearer. Right now Mario just shrugs his shoulders and says "well you seem to be managing so far".

#### Kevin Buzzard (Feb 17 2021 at 19:37):

Right now the problem is that definitional equality cannot be controlled, because part of the system works under the assumption that definitional equality is "the" equality, and then stuff of type order_dual X magically becomes of type X. This is, in my mind, an error.

#### Kevin Buzzard (Feb 17 2021 at 19:38):

I think X -> order_dual X is an invisible map, just like nat -> int is an invisible map and we've made some great tactics which now mean that for someone who has had experience with these matters, the map is no longer a problem.

#### Kevin Buzzard (Feb 17 2021 at 19:39):

Maybe we want an undual map if you are worried about duals of duals. But just saying "oh there will be problems with duals of duals so let's not do it" isn't the answer, as Damiano found out. We have this problem with category theory, and we have op and unop. We need to find an abstract problem and then solve it with tactics.

#### Damiano Testa (Feb 17 2021 at 19:49):

I think that the idea of the double-dual map is good! Part of the confusion (for me) is that it is not true that the dual of a dual is necessarily what you started with: in the context of vector spaces, this actually characterizes the finite-dimensional ones. So, I am in favour of keeping our mind straight about which order to consider. Besides, when thinking about specialization of points or inclusion of ideals, I think that there is little room for being confused about which side of the dual divide we are.

#6286

#### Johan Commelin (Feb 17 2021 at 20:03):

Now I hope there will be some lattice-theoretic machinery in place to give us the Krull dimension. @Aaron Anderson you're the expert here (-;

#### Aaron Anderson (Feb 17 2021 at 20:31):

I'll look into it. Coming up with some rudimentary definition of rank/height on posets should be fine, but there's some choices as to whether you want the ranks to be nats, enats, ordinals, cardinals... I'll have to do some reading.

#### Kevin Buzzard (Feb 17 2021 at 20:39):

Most mathematics goes on in a finite-dimensions or under other finiteness hypotheses, so my instinct would be to define nat_dimension which just returns 37 for infinite-dimensional objects. We also have the problem with the empty set, which has dimension -1, or possibly every natural. So maybe nat_dimension and a predicate is_finite_dimensional? Of course one could make the perfect type which takes in the correct concept of dimension in terms of cardinals or what have you, but after a while one has to consider things which are useful in practice rather than the abstract beautiful thing which takes values in enat or whatever and just annoys everyone because ring doesn't work.

#### Kevin Buzzard (Feb 17 2021 at 20:43):

My memory is that for various theorems relating depth and dimension, you could be clever and let stuff be infinite but actually the theorems are false in these cases anyway.

#### Johan Commelin (Feb 17 2021 at 20:48):

I could imagine that we will have krull_dim and krull_findim, just like for vector spaces.

#### Johan Commelin (Feb 17 2021 at 20:49):

One returns an cardordinal, the other a nat

#### Kevin Buzzard (Feb 17 2021 at 20:49):

We could do, but is there any theorem about infinite-dimensional rings which we will ever need/use?

#### Kevin Buzzard (Feb 17 2021 at 20:50):

And we still have problems with krull_dim (Spec(0)) even if we use cordinals.

Touche

#### Kevin Buzzard (Feb 17 2021 at 20:50):

Literally the only thing I know about infinite-dimensional rings is some counterexample of maybe Nagata -- an infinite-dimensional Noetherian...ring? Or something?

bingo

#### Kevin Buzzard (Feb 17 2021 at 20:51):

I would be happy proving that it had dimension 37.

#### Damiano Testa (Feb 17 2021 at 21:17):

I agree with Kevin: most interesting examples are finite-dimensional. And most of the next ones are locally finite dimensional.

But, if you are interested in a non-finite dimensional scheme, you are likely not going to take seriously what its dimension is.

#### Damiano Testa (Feb 17 2021 at 21:18):

Given how things work out in algebraic geometry, defining codimension might be useful as well

and depth

and height

#### Damiano Testa (Feb 17 2021 at 21:19):

Is upper semicontinuity already defined in mathlib?

#### Aaron Anderson (Feb 17 2021 at 22:03):

I buy that in algebra, we mostly care about finite dimensions or infinite dimensions, but if I define it for posets in general, a more general version might be nice.

#### Aaron Anderson (Feb 17 2021 at 22:04):

Also, I think I could define the cardinal version to literally be the sup of the cardinalities of all chains

#### Aaron Anderson (Feb 17 2021 at 22:08):

although I guess there isn't a fantastic API for turning that into an enat or a nat, is there?

#### Adam Topaz (Feb 17 2021 at 22:27):

I think the reasonable thing to do is what has been done for dimension of vector spaces.

#### Adam Topaz (Feb 17 2021 at 22:28):

I.e. define a dimension as a cardinal, then make a findim taking values in nat with value 0 (or 37) on something that is not finite dimensional, etc.

#### Adam Topaz (Feb 17 2021 at 22:30):

And maybe down the line one can redefine the dimension of a vector space in terms of the lattice of subspaces?

#### Aaron Anderson (Feb 17 2021 at 22:52):

Ok, the definition of finite_dimensional.findim is a composition of cardinal-valued dim with a cardinal-to-nat function that just returns 0 for infinite cardinals. I think my first step should be to separate out that cardinal-to-nat function, because that just sounds useful, and then I can use the same strategy to define the cardinal-valued and nat-valued heights of posets.

#### Kevin Buzzard (Feb 17 2021 at 22:54):

Fair enough. As long as there's a nat version which returns the right thing for nonempty finite- dimensional lattices i don't care what else there is

#### Kevin Buzzard (Feb 17 2021 at 22:55):

Thanks! This is all part of the slow but sure build-up of a serious commutative algebra library which I'm very excited about

#### Aaron Anderson (Feb 17 2021 at 22:58):

Bonus of this strategy: we get a fincard function (albeit one that's grotesquely noncomputable)

#### Kevin Buzzard (Feb 17 2021 at 23:19):

We never wanted it to be computable, we just want a painless way to take the size of something :-) There's a basic API for fincard somewhere, probably in the group theory game?

#### Kevin Buzzard (Feb 17 2021 at 23:21):

https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/finsum/basic.lean second half of the file

Last updated: May 18 2021 at 07:19 UTC