Question about `Valued.is_topological_valuation`

Stream: maths

[Jiang Jiedong]

Hi everyone,

I am confused by the field is_topological_valuation in the definition of the class Valued.

It says ∀ (s : Set R), s ∈ nhds 0 ↔ ∃ (γ : Γ₀ˣ), {x : R | Valued.v x < ↑γ} ⊆ s. Don't we need γ to be inside the image of the valuation map?

Consider the following examples (where I will write valuation additively):
Let $v_p : \mathbb{Q}_p \to \mathbb{Z} \cup \{-\infty\}$ be the usual $p$-adic valuation,
Let $v_p' : \mathbb{Q}_p \to \mathbb{Z} \oplus \mathbb{Z} \cup \{-\infty\}$ be the map sending $x$ to $(0,v_p(x))$. ($0$ is still sent to $- \infty$.) Here, $\mathbb{Z} \oplus \mathbb{Z}$ is equipped with the lexicographic order.

Then these two valuations are equivalent, but is_topological_valuation will force them to have two different topologies. The first one is equipped with the usual $p$-adic topology. But the second one, by choosing $\gamma = (1,0)$, a value that no element could possibly have, $\{x : \mathbb{Q}_p | v_p' (x) > γ\}$ is just the singleton $\{0\}$. This means $\mathbb{Q}_p$ is equipped with the discrete topology in the second case.

Is this intended? Are there any applications that we do need to set the topology for the second valuation as discrete topology? It seems quite confusing to me that the topology changes just because the target of the valued group changes. Thank you for any comments or suggestions!

[Patrick Massot]

This is definitely a typo. Compare with http://virtualmath1.stanford.edu/~conrad/Perfseminar/refs/wedhornadic.pdf, Definitions 1.22 and 5.39 that are meant to be the source of this construction.

[Filippo A. E. Nuccio]

I think that in the whole set-up $\Gamma$ is thought of as being the value group, which is not in your (extremely nice!!!) example.

[Patrick Massot]

Wedhorn has an explicit notation for this. He starts with a group Γ and then uses Γ_v.

[Filippo A. E. Nuccio]

Oh, I see.

[Patrick Massot]

That notation is part of Definition 1.22, at the very end.

[Patrick Massot]

The confusing thing is that v is denote by |·| in that early definition.

[Filippo A. E. Nuccio]

Well, but indeed then 5.39 is for $\Gamma_v$ not for $\Gamma$, right?

[Filippo A. E. Nuccio]

I mean, the $\gamma$ used to define open nhbds of $0$ is an element of $\Gamma_v$.

[Patrick Massot]

Right, that’s why I wrote that the mathlib version is a typo.

[Filippo A. E. Nuccio]

Probably we could add a field to the Valued class insisting that v be surjective?

[Filippo A. E. Nuccio]

Insisting that $\Gamma$ is the value group would be a nightmare.

[Filippo A. E. Nuccio]

FWIW insisting that a $\mathbb{Z}_{m0}$-valued valuation is surjective is precisely the way we have with @María Inés de Frutos Fernández to define "discrete valuations", precisely because we need to fix a normalization.

[Patrick Massot]

Why not simply modifying the problematic field?

[Filippo A. E. Nuccio]

The problem is that to modify it you need to impose that $\Gamma$ has some special property, namely being the value group, no? But this can be cumbersome, because in many examples what you have is just an iso between your value group and, say, $\mathbb{Z}$ or multiplicative ($\mathbb{Z}$) or the like. If you let $\Gamma$ be anything, you end up with Jiang's counterexample... while the only property that might be really useful is that the valuation always surjects onto the value group, and if this is enough you can just add this Prop-valued field.

[Filippo A. E. Nuccio]

Or perhaps I misunderstand your question?

[Jiang Jiedong]

@Filippo A. E. Nuccio Maybe another possible solution with fewer changes involved is that we change
∀ (s : Set R), s ∈ nhds 0 ↔ ∃ (γ : Γ₀ˣ), {x : R | Valued.v x < ↑γ} ⊆ s
into
∀ (s : Set R), s ∈ nhds 0 ↔ ∃ (y : R), {x : R | Valued.v x < Valued.v y} ⊆ s

[Filippo A. E. Nuccio]

I see your point, and I agree that your suggestion is closer to the current status. On the other hand, it would change many proofs a lot, since to prove that something is a nhbd of $0$ you would be looking for a term in R rather than in Γ₀ˣ. So, a proof that went around producing some $\gamma$ and then had a use γ would need to be changed completely in order to produce a r : R and then have a use r. Also, it is in a sense further away from the idea of being a "topological valuation" because it does not really allow you to "move from R to Γ₀ˣ" (I am aware that mathematically the two are equivalent, especially if enforcing surjectivity ; but I am trying to reflect about the potential impact on the formalization).

[Jiang Jiedong]

I agree that if we choose to modify it in this way, many proofs will change a lot. But maybe it is more aligned with the literature? On the other hand, if we require the valuation to be surjective, that would also change all the places where we construct ‘Valued’ instances. One thing that could happen is that when dealing with map and comap of the valued instances, if one tried to define a valued instance in a subfield of a valued field, the value group would be some subtype that is specialized for this subfield only. Another thing is that it is almost impossible to have NNReal as the value group, which has many nice calculation properties.

[Filippo A. E. Nuccio]

I see what you mean, good point. Let me think about it a bit.

[Patrick Massot]

Yes, this is the modification I had in mind. Of course it will change a lot of proofs, but this is not surprising since the mathematical content changed. The current definition is not what we want.

[Jiang Jiedong]

I think we have to be more careful here. According to Wedhorn's notes, the neighbourhoods of $0$ is defined using $\{x | v(x) < \gamma\}$ for $\gamma \in \Gamma_v$, where $\Gamma_v$ is the groupification of $\text{im} (v) \backslash \{0\}$, but may not equal to $\text{im} (v) \backslash \{0\}$.

So it might still result in a different topology if we use this
∀ (s : Set R), s ∈ nhds 0 ↔ ∃ (y : R), y ≠ 0 ∧ {x : R | Valued.v x < Valued.v y} ⊆ s
as the new definition of is_topological_valuation when R is not necessarily a field.

And if we require the valuation $v$ to be surjective, we would lose rings whose image under the valuation map is only a monoid with zero, but not a group with zero.

So maybe the most reasonable solution is strictly following the definition in Wedhorn's notes? Define $\Gamma_v$ first, then define topology using this $\Gamma_v$.

[Filippo A. E. Nuccio]

The problem with defining kt with $\Gamma_v$ is that we cannot put a Valued instance, for instance, on a DVR using its usual $\mathbb{Z}_{m,0}$-valued valuation, we could only use the $K^\times/R\cup\{0\}$-valued one.

[Jiang Jiedong]

Sorry I did not make myself clear enough. I think we can still use instances (such as Zm0 on DVR) for valued. But for the relation between topology and valuation, we require that the $\gamma$ in ∀ (s : Set R), s ∈ nhds 0 ↔ ∃ (γ : Γ₀ˣ), {x : R | Valued.v x < ↑γ} ⊆ s further lies in the subgroup generated by $\text{im } v \backslash \{0\}$.

[Filippo A. E. Nuccio]

Oh I see!

[Filippo A. E. Nuccio]

This seems much more reasonable.

[Filippo A. E. Nuccio]

IMHO this is the right approach to take, but before going for a potentially painful PR I would like to hear @María Inés de Frutos Fernández and @Adam Topaz and @Antoine Chambert-Loir 's opinions.

[Adam Topaz]

This is a complicated question. On the one hand, I agree that this could be seen as an issue (but I'm not convinced that it should be changed, as I explain below). On the other hand, I don't think we should assume that $\gamma$ lies in the subgroup generated by the image. Indeed, a fairly common case is to consider real-valued valuations even for fields where the valuation is not necessarily surjective. In such cases it would be convenient to keep the definition as is (e.g. to relate it to the topology induced by the associated absolute value).

Note also that $\Gamma$ is an out-param in this class, and yes, if someone adds a problematic Valued K Gamma instance then that is indeed a problem, but I don't see this as being too different from someone adding a problematic topology instance or group instance, etc. It's up to the user to ensure that "canonical" instances are indeed "canonical".

[Filippo A. E. Nuccio]

The problem I see is that in @Jiang Jiedong 's example the two valuations are equivalent yet they yield different topologies, and this is problematic. I do not think this is the same as putting a crazy topology on a group, it seems deeper. On the other hand, I do not get the point of your example with fields endowed with a non-surjective, real-valued valuation (eg. fraction fields of DVR, say). In that case, a basis of nhbds of 0 is also generated by elements whose valuation is less than an integer, not only less than a certain real, so it seems to work (to me, at least). Or did I misunderstand your idea?

[Kevin Buzzard]

Equivalent categories can have different concepts of equality but we use equality in category theory sometimes. Is this the same phenomenon?

[Filippo A. E. Nuccio]

I do not know, but would you agree that equivalent valuations should induce the same topology? So, the fact that through the pattern valuation -> Valued -> topological space we can start off with equivalent valuations and end up with different topologies (like the $p$-adic and the discrete) is problematic?

[Kevin Buzzard]

I don't know if I agree with that statement. Equivalent valuations aren't equal.

[Filippo A. E. Nuccio]

But don't they induce the same topology almost by def?

[Kevin Buzzard]

Not according to mathlib!

[Filippo A. E. Nuccio]

@Jiang Jiedong BTW: What do you exactly mean when you say that your valuations in the example are equivalent? According to Wikipedia, for instance, this would need that the groups where they take values are isomorphic....

[Kevin Buzzard]

Equivalence of valuations is a thing, it means v1(a)<=v1(b) iff v2(a) <= v2(b). And right now it's the case (of I understood things correctly) that equivalent valuations can indeed induce different topologies.

[Filippo A. E. Nuccio]

Remains the question as whether this is wanted or not...

[Jiang Jiedong]

I don't think equivalent valuations should induce different topologies...

If we choose the definition as in Wedhorn's notes (and Huber's papers I think?), equivalent valuation will induce the same topology. I think the equivalence of valuations should be something like equivalence in category theory, most of the important properties should be invariant under this equivalence.

[Jiang Jiedong]

In my point of view, the "canonicity" of valuation is by itself up to the equivalence of valuation. In the case of finite extensions of $\mathbb{Q}_p$, there are already two common choices of valuations. The first one has the value of uniformizer equal to 1, and the second has the value of $p$ equal to 1 (even without discussing what is the type of value group).

[Jiang Jiedong]

However, there is always a canonical topology on these valued rings, that should not be affected by the choice of specific valuations inside the equivalent class. (In fact, in Neukirch's textbook, the equivalence of valuation is defined as they induce the same topology!)

[Kevin Buzzard]

I agree with all of this, and I agree that our definition is a little fishy, however it does seem to be more general than what is in the literature. Right now my instinct is to add a warning to the docstring. But if you want to take on the refactor then go for it!

[Filippo A. E. Nuccio]

But we do not want to work with equivalence classes of valuations, I believe. It is much easier to work with parametric ones, that are free to take values in different places and with different normalizations. (sorry, this message was sent before Kevin's, but my connection went down)

[Kevin Buzzard]

I don't really know what we want to do, and this is why the conversation is so nebulous. Right now the valuations I'm using are rank 1 and take values in Zm0 so the entire question is moot. Do we actually have a use case where this issue is relevant?

[Jiang Jiedong]

Yes, I shall explain some more about why I want this property "equivalent valuations induce the same topology" to be true.

[Jiang Jiedong]

I believe for valued instance on the extension $L$ that ramified infinitely over $\mathbb{Q}_p$ (such as $\mathbb{Q}_p^\text{alg}$), we would choose the normalization such that $v p = 1$. No matter what normalization we choose, the relation between the valuations on $L = \mathbb{Q}_p^\text{alg}$ and a general finite extension $K$ of $\mathbb{Q}_p$ cannot be "the restriction of valuation from $L$ to $K$ equals to the valuation on $K$", it will be an equivalence of valuations.

But if the topology is defined like the current setup, there is nothing I can get about the relation between topology on $K$ and the topology on $L$ if I only know about the restriction of valuation is equivalent.

[Jiang Jiedong]

I met this question when I was doing Krasner's lemma. What I wanted to do is, if I change the valuation on $K$ to this restriction of valuation from $L$ to $K$, the topology remains the same on $K$ and $K$ is still complete if it is complete at the beginning.

Then I can use the theorem of uniqueness of norm extension formalized by Maria Ines if I translate the rank one valuations to norms.

[Jiang Jiedong]

Kevin Buzzard said:

But if you want to take on the refactor then go for it!

I am happy to take on the refactor if it is a refactor that mathlib will accept. :working_on_it:

[Kevin Buzzard]

Ultimately I do not know a use case for the definition we currently have, and I agree that it is confusing. I would definitely be open to merging a PR refactoring this.

[Patrick Massot]

I think I wrote the current definition and I definitely did not intend to use a definition that is different from the informal one seen in Wedhorn and Bourbaki. I am in favor of fixing this.

[María Inés de Frutos Fernández]

Jiang Jiedong said:

I met this question when I was doing Krasner's lemma. What I wanted to do is, if I change the valuation on $K$ to this restriction of valuation from $L$ to $K$, the topology remains the same on $K$ and $K$ is still complete if it is complete at the beginning.

Then I can use the theorem of uniqueness of norm extension formalized by Maria Ines if I translate the rank one valuations to norms.

Could you expand on why this gave you trouble? In this case, you are working with rank one valuations, so the topology on K induced by either version of the valuation should be the same as the topology induced by the corresponding norm, right?

[Kevin Buzzard]

Right, the only problem should be when the image of the valuation doesn't contain arbitrarily small positive elements, this is why I was confused about whether it mattered in practice (you'd have to spefically have managed to create a rank n valuation with image in a rank n+1 group-with-zero).

[Jiang Jiedong]

María Inés de Frutos Fernández said:

In this case, you are working with rank one valuations, so the topology on K induced by either version of the valuation should be the same as the topology induced by the corresponding norm, right?

Yes, you are right. What I am dealing with is essentially rank-one valuations. So in the end, I can prove the equality of topology using the current definition. However, I need to prove something nontrivial and use special properties of rank one case, which could follow the definition directly and have a more general form if we instead use Wedhorn's notes.

theorem topology_eq {K L : Type*} {ΓK ΓL : outParam Type*} [Field K] [Field L]
    [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL]
    [Algebra K L] [vK : Valued K ΓK] [vL : Valued L ΓL]
    (h : vK.v.IsEquiv <| vL.v.comap (algebraMap K L)) [vK.v.RankOne] [vL.v.RankOne] :
    vK.toUniformSpace = (Valued.mk' (vL.v.comap (algebraMap K L))).toUniformSpace := sorry
    -- current definition, needs some Archimedean property of NNReal.

theorem topology_eq' {K : Type*} {ΓK ΓK': outParam Type*} [CommRing K]
    [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓK']
    (v : Valuation K ΓK) (v' : Valuation K ΓK') (h : v.IsEquiv v') :
    (Valued.mk' v).toUniformSpace = (Valued.mk' v').toUniformSpace := sorry
    -- easy if we use Wedhorn's definition.

[Adam Topaz]

Suppose you have Algebra K L and v : Valued L Gamma. With your proposed change, how do you propose to construct a restriction of type Valued K Gamma (in such a way so that the map K -> L is continuous)?

[Jiang Jiedong]

Adam Topaz said:

Suppose you have Algebra K L and v : Valued L Gamma. With your proposed change, how do you propose to construct a restriction of type Valued K Gamma (in such a way so that the map K -> L is continuous)

I understand your point here. I don't think it is mathematically correct (according to literature) to have this K -> L continuous? The counterexample is already given here by myself.

[Adam Topaz]

Yes, I agree (that was my point). I think that Valued should be left as is for precisely this reason. I think we should rather rethink how we talk about extensions of valued fields.

[Jiang Jiedong]

We will have this map K -> L continuous, if we put the comap of valuation on K using current definition in mathlib.

[Jiang Jiedong]

I see.

[Adam Topaz]

To add a bit more detail: if we have Algebra K L and Valued L Gamma, then it's perfectly natural to restrict to obtain Valued K Gamma, and since Valued includes a topology, it's only natural for the map K -> L to be continuous.

[Jiang Jiedong]

OK, so this is a decision about whether to divert from the literature here. I don't mean diversion is a bad choice. Could I ask if you have met such situations before and what are your past decisions (if they exist) based on?

[Adam Topaz]

We already diverted by bundling a topology into Valued as far as I’m concerned

[Adam Topaz]

I have my opinions on this, but I would rather defer to @María Inés de Frutos Fernández since she has worked extensively with this class

[Filippo A. E. Nuccio]

Adam Topaz said:

To add a bit more detail: if we have Algebra K L and Valued L Gamma, then it's perfectly natural to restrict to obtain Valued K Gamma, and since Valued includes a topology, it's only natural for the map K -> L to be continuous.

I don't quite agree with this. If we have Algebra K L and Valued L Gamma then we might want that Valued K Gamma is re-normalized or not (I am speaking about the 'valuation' part of Valued). Since the Valued instance fixes this once and for all, we would need to agree once and for all that in every $p$-adic field the valuation of $p$ is $-1 \in \mathbb{Z}_{m,0}$ and thus uniformizers get smaller and smaller valuation as the ramification increases. Leaving some flexibility here seems more suited, no?

[Filippo A. E. Nuccio]

With @Antoine Chambert-Loir we have just opened #14752 to address the problem.