Residue fields should be of natural type and functorial

[swewers]

It would be great if the residue field k of a discrete valuation v_K on a field K would more or less obey the following two rules:

1. (Naturalness) The type of k if, whenever possible, the natural one. For instance, a finite field , a number field, or a function field (and not just a quotient field).
2. (Functoriality) If L/K is a field extension and v_L an extension of v_K to L, then the residue field k' of v_L is an extension of k (and therefore k should coerce into k').

I will now and then list instances in the MCLF code where this is not the case. There may also be examples where the two rules contradict each other.

TODO:

• [ ] Fix 25976 once #103 has been fixed upstream.

[saraedum]

Could you create an upstream trac ticket for this?

[swewers]

Ok, I will do it soon, but first I want to think more about it and in which situations it is relevant.

[saraedum]

Actually, I think both 1. and 2. should be checked by an automated test. Then we see immediately where this currently fails. There might be some cases where we don't think it's worth to fix it of course.

[saraedum]

I created https://trac.sagemath.org/ticket/25976 so I can push my test code somewhere. Please improve on the once we have figured out what we want exactly :)

[saraedum]

Functoriality is actually complicated: I don't want valuations to remember how they were constructed. This would create a lot of trouble (as a bad example, last time I checked, number fields remember a certain complex embedding, and this has bitten me several times already that seemingly identical objects are somehow distinct.)

Requiring k to coerce into k' in your example might also be complicated because if you create the same identical field k' in different ways, then there might be two different coercions from k to k' and that's of course not allowed in Sage.

If we absolutely need this information, then we'd need a variant of v.extension(L, embeddings=True) that returns an additional object that contains the relevant embeddings of the residue fields. But I think that we can mostly get away without that or with a method that reconstructs such things.

Anyway, let's see how my tests go first…

[swewers]

I understand. In many places, having the correct embedding of residue fields of extensions is crucial. An option like v.extension(L, embeddings=True) would be perfect for this. But you are right, in any place where one really needs this, one can reconstruct the embedding.

[swewers]

In connection to issue #103 I now realize that the type of the residue field of a valuation is maybe not so crucial. Crucial is the possibility to define an isomorphism between the residue field and a field of the 'natural type', and more generally embeddings of the residue field into quite arbitrary fields.

The typical example is that I have a curve X over a p-adic field K and a non-standard valuation v on the function field of X (extending the base valuation on K, residue field of dimension one). I think of v as a Type-II-point xi on the Berkovich space X^an. I want to have the option of realizing the residue field of v as a function field over the residue field of K, but also as a function field over any intermediate field between the residue field of K and the field of constants of this function field. All this is best done internally in the MCLF code and has nothing to do with the valuation code.

[saraedum]

I see. But I feel that large parts of this are not specific to MCLF but that there is a point in improving the possibilities to define morphisms and in particular embeddings and isomorphisms of finite fields and function fields (or their isomorphic counterparts that are really missing such functionality, namely fields of fractions and quotient rings.)