dimension function for schemes

Stream: mathlib4

[Johan Commelin]

https://stacks.math.columbia.edu/tag/02I9 defines the notion of a dimension function. This is in terms of the specialization order on a topological space. It needs the notion of immediate specialization, which is basically docs#CovBy. But CovBy and its API is not available for the specialization order if it isn't an instance.

This mostly plays a role in scheme theory. So I'm wondering, should a scheme X just have the specialization order as an instance by default? And do we want to make it an instance in terms of the existing definition? Or do we include the order as data in the definition of a scheme (together with an axiom that it is the specialization order) to enable forgetful inheritance?

[Adam Topaz]

I think this is a good idea. We already have docs#Topology.IsUpperSet which should be used

[Aaron Liu]

docs#Specialization equips a type with its specialization preorder.

[Adam Topaz]

To clarify, I think we should include the order and an IsUpperSet axiom. Maybe instead of building schemes on top of topological spaces we should make them on top of Alexanderov spaces?

[Adam Topaz]

Rather docs#AlexDisc

[Adam Topaz]

But we should make a variant of this category where objects include the preorder as well

[Adam Topaz]

Wait maybe these axioms are too strong for schemes?

[Adam Topaz]

Well I guess the question is whether generic points should be at the top or bottom

[Adam Topaz]

Because I think the default behaviour of IsUpperSet flips the order

[Adam Topaz]

Okay, sorry for rambling. What I said above is nonsense. Schemes aren't alexandrov, but (I think) limits of alexandrov spaces, which we can still write down in terms of preorders, but I don't think we have the infrastructure to do such things directly at the moment.

[Andrew Yang]

I think it is perfectly fine giving a X : Scheme the specialization topology, and I don't think we should include order in the definition of schemes. I have no example where the underlying set of schemes already come with an order except the affine case. But that is still breaking the PrimeSpectrum R/Spec R abstraction boundary.

[Adam Topaz]

Another place where such an order might arise "in nature" is if you want to identify the scheme-theoretic points of a curve with the valuation rings of its function field. In that case, the "space" of valuation rings will have a natural order which will agree with the specialization order. (More generally if $X$ is a separated proper variety, then you can identify $X$ with some quotient of the Zariski-Riemann space of the function field, which will end up having some natural order.)