Zulip Chat Archive

Stream: maths

Topic: order on prime_spectrum


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Damiano Testa (Feb 17 2021 at 19:20):

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

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:21):

Hmmm, they can't both be instances

view this post on Zulip Adam Topaz (Feb 17 2021 at 19:21):

Another +1 for this suggestion.

view this post on Zulip Adam Topaz (Feb 17 2021 at 19:22):

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

view this post on Zulip Adam Topaz (Feb 17 2021 at 19:23):

So I guess that corresponds to aba \le b iff bb is a specialization of aa.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 17 2021 at 19:26):

Yes, I will avoid order dual... Ahaha

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:27):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Feb 17 2021 at 19:29):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:32):

I would vote for

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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:32):

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

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:34):

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

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 17 2021 at 20:02):

#6286

view this post on Zulip 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 (-;

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 17 2021 at 20:49):

One returns an cardordinal, the other a nat

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 20:50):

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

view this post on Zulip Johan Commelin (Feb 17 2021 at 20:50):

Touche

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 20:51):

bingo

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 20:51):

I would be happy proving that it had dimension 37.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 17 2021 at 21:18):

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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 21:18):

and depth

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 21:18):

and height

view this post on Zulip Damiano Testa (Feb 17 2021 at 21:19):

Is upper semicontinuity already defined in mathlib?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Feb 17 2021 at 22:58):

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

view this post on Zulip 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?

view this post on Zulip 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