order on prime_spectrum

Stream: maths

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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

[Damiano Testa]

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

[Johan Commelin]

Hmmm, they can't both be instances

[Adam Topaz]

Another +1 for this suggestion.

[Adam Topaz]

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

[Adam Topaz]

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

[Damiano Testa]

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]

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]

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]

Yes, I will avoid order dual... Ahaha

[Johan Commelin]

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

[Adam Topaz]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

I would vote for

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

[Kevin Buzzard]

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

[Adam Topaz]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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.

[Johan Commelin]

#6286

[Johan Commelin]

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]

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]

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]

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]

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

[Johan Commelin]

One returns an cardordinal, the other a nat

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

Touche

[Kevin Buzzard]

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

[Kevin Buzzard]

bingo

[Kevin Buzzard]

I would be happy proving that it had dimension 37.

[Damiano Testa]

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]

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

[Kevin Buzzard]

and depth

[Kevin Buzzard]

and height

[Damiano Testa]

Is upper semicontinuity already defined in mathlib?

[Aaron Anderson]

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]

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

[Aaron Anderson]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Aaron Anderson]

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]

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]

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]

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

[Kevin Buzzard]

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]

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