hypotheses for a field property

Stream: maths

[Jireh Loreaux]

Under what hypotheses could I obtain the following theorem? I think nondiscrete_normed_field 𝕜 is not enough, but maybe I'm missing something. I believe is_R_or_C 𝕜 is sufficient, but overkill.

lemma {𝕜 : Type*} [normed_field 𝕜] (r : ℝ) (hr : 0 < r) : ∃ k : 𝕜, 1 - r < ∥k∥ ∧ ∥k∥ < 1 := sorry

[Kevin Buzzard]

docs#nondiscrete_normed_field

[Kevin Buzzard]

Right so the p-adics would be a nondiscrete normed field counterexample (|p|=1/p, no k if r<1-1/p)

[Kevin Buzzard]

What you want is what I'd probably call a non-discretely-valued field; we might not have it. It's a shame, there seem to be 2 uses of the word "discrete" going on here. If $v:K^*\to\R$ is a valuation (multiplicative, sending 1 to 1) or norm (additive, sending 1 to 0) then one could use the adjective "discrete" to indicate that the induced topology on v coming from the metric is discrete, or one could use it to indicate that the image of v in $\R$ is discrete, and the $p$-adics satisfy one but not the other. In BGR they say "nontrivial" for what we've called "nondiscrete", and say that the valuation is nondiscrete if the image is not discrete (which is what your question is about).

[Kenny Lau]

@Kevin Buzzard the BGR "nondiscrete" would correspond to the image being dense, right?

[Kevin Buzzard]

Right. A broad classification of additive subgroups of $\R$ is $\{0\}$, the infinite cyclic ones (one for each element of $\R_{>0}$) and then all the others are topologically dense.

[Anatole Dedecker]

You can at least replace is_R_or_C with being a normed algebra over the rationals, right ?

[Jireh Loreaux]

You mean in combination with nondiscrete_normed_field? Otherwise there's the zero algebra. Seems plausible but I don't see the proof.

[Anatole Dedecker]

Oh sorry I thought normed algebra implied that the algebra map was isometric, but it’s only an inequality

[Anatole Dedecker]

I’ve been fooled by this definition so much times 😅

[Jireh Loreaux]

It used to be isometric, but Eric refactored

[Anatole Dedecker]

Oh that’s why, I thought the fooling was the other way around

[Anatole Dedecker]

But wasn’t there a plan to also have the isometric version ? Or is it mostly useless ?

[Kevin Buzzard]

You don't want to ban the zero ring

[Jireh Loreaux]

IIRC, I think (a) you want the zero ring, and (b) you can recover the isomeric version with norm_one_class

[Eric Wieser]

That sounds right to me

[Eric Wieser]

I think there was a separate discussion by someone else about normed vs valued fields, and which one normed_field should be

[Yaël Dillies]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/normed_ring.20vs.20normed_field

[Junyan Xu]

normed_algebra over Q would not cover examples like the algebraic closure of p-adic fields, which are algebras over Q but not normed_algebras with the default (archimedean) norm on Q. The condition of interest is equivalent to the range of norm being dense in R>=0 and that's a nice lemma to have, but I'm not sure if either of the conditions should become a typeclass.

[Jireh Loreaux]

So, should we have a nondiscretely_valued_field (perhaps with another name)? I'm reasonably sure that I need this lemma to show that the multiplier algebra satisfies the C⋆-property.

[Eric Wieser]

I thought the claim in the other thread was that our existing docs#nondiscrete_normed_field is really describing a nondiscrete_valued_field

[Jireh Loreaux]

I'm not at all sure about naming, but I think the type class itself makes sense. If there is standard terminology for this, then great.

[Heather Macbeth]

@Jireh Loreaux How did we settle things with the lemma at the top of this thread? Is it true for nondiscrete_normed_field or does it require a new typeclass? I was trying to generalize the scalar field in docs#continuous_linear_map.op_norm_bound_of_ball_bound and decided this was what was needed.

[Heather Macbeth]

see branch#nondiscrete-normed-field-facts (optimistically named)

[Jireh Loreaux]

Kevin gave a counterexample. We need a new type class. I'm only waiting because I'm not sure what to call it.

[Antoine Chambert-Loir]

Jireh Loreaux said:

So, should we have a nondiscretely_valued_field (perhaps with another name)? I'm reasonably sure that I need this lemma to show that the multiplier algebra satisfies the C⋆-property.

If I may, the nondiscrete_normed_field terminology is really misleading.
In his book, Berkovich uses a periphrase “Assume that the valuation of k is nontrivial” which indicates nontrivial_normed_field would be better.

[Junyan Xu]

Kevin Buzzard said:

In BGR they say "nontrivial" for what we've called "nondiscrete", and say that the valuation is nondiscrete if the image is not discrete (which is what your question is about).

So now we have two votes in favor of a rename?

[Jireh Loreaux]

I'm in favor of a rename. I was duped into thinking the lemma at the top of the thread was true for the current nondiscrete_normed_field until I tried to prove it.

[Jireh Loreaux]

/poll Rename nondiscrete_normed_field to ...
nontrivial_normed_field
don't rename

[Heather Macbeth]

Happy to go with consensus here, thanks for thinking about it!

[Kevin Buzzard]

I am kind of the worst sort of person here. There are people doing functional analysis over R or C and I've done a bit of functional analysis in my time but over the p-adics, so keep looking over at what's going on and saying annoying things like "oh in p-adic land we do this a bit differently" but not actually ever doing any formalising, just moaning, which is basically me at my worst. Maybe I should get people working on p-adic functional analysis so we'll begin to notice these issues earlier

[Moritz Doll]

I appreciate the insights into p-adics (I've never learned anything about it). Also formalizing functional analysis is really fun and I don't want to bother with really subtle details about derivatives every day :grinning:

[Moritz Doll]

I have no strong feelings about the rename, but I agree that the current name might be a bit misleading.

[Sebastien Gouezel]

Let me just mention that the current naming nondiscrete_normed_field corresponds exactly to normed fields which are not discrete (i.e., in which 0 -- or any point -- is not isolated). But if everyone gets confused by this terminology then we can of course change it!

[Jireh Loreaux]

@Sebastien Gouezel, for me the main problem with the current name is that I'm not sure what to call "fields whose image under the norm is dense in ℝ", and it seems like both Heather and I will need that type class. So, I could be okay with nondiscrete_normed_field as is if there were a viable naming suggestion for the new class. On the other hand, as Antoine and Kevin suggested, it might be good to go with the naming in the literature.

[Jireh Loreaux]

@Kevin Buzzard personally, I don't mind your "moaning". For me, it's helpful to recognize when I'm not making my arguments/objects general enough, especially since in operator algebras ℂ is the only field in sight (even ℝ relegated to second class status unless we want to talk about order properties of selfadjoint elements).

[Kevin Buzzard]

I need to put my thoughts together about is_R_or_C. I will try to find the time later.

[Mario Carneiro]

I think nontrivial_normed_field is a bit misleading considering that nontrivial already means containing at least two points and on a cursory inspection of the claim I think that this is not the kind of triviality under consideration

[Mario Carneiro]

so I tend to agree with Sebastien Gouezel that nondiscrete_normed_field is more correct (we also use the word discrete for the top topology and that's exactly the kind of triviality we mean here)

[Mario Carneiro]

Jireh Loreaux said:

Sebastien Gouezel, for me the main problem with the current name is that I'm not sure what to call "fields whose image under the norm is dense in ℝ", and it seems like both Heather and I will need that type class.

How does this typeclass relate to nondiscrete_normed_field? Naming these as densely_normed_field modulo bikeshedding, it is clear to me that a discrete normed field is not densely normed, and it seems like ostrowski's theorem would say that a nondiscrete normed field is densely normed but perhaps there are some additional conditions like nontriviality (in the sense of having two points) to actually make this an equivalence

[Kevin Buzzard]

Waitwaitwait. Is Sebastien saying "it is standard in real analysis to name it this way" or is he saying "we made this name up, here is a logical reason why it's correct"? I thought the latter. I'm saying that it's standard in p-adic analysis to use "discrete" to mean "valuation has discrete image", e.g. "discrete valuation ring" or "discretely-normed field". This can't happen in real or complex analysis.

[Jireh Loreaux]

@Mario Carneiro, as Kevin mentioned at the top of the thread, the p-adics are a nondiscrete normed field which are not densely normed.

As for the confusion with nontrivial, I think this can be explained away by the fact that it's its own type class (as opposed to just stacking the two). I thought about this possible confusion.

Personally, I would prefer the nontrivial / nondiscrete pair in order to be consistent with the literature, but I would be okay with nondiscrete / densely (or similar) pair because it is more precise.

[Sebastien Gouezel]

Kevin Buzzard said:

Waitwaitwait. Is Sebastien saying "it is standard in real analysis to name it this way" or is he saying "we made this name up, here is a logical reason why it's correct"? I thought the latter. I'm saying that it's standard in p-adic analysis to use "discrete" to mean "valuation has discrete image", e.g. "discrete valuation ring" or "discretely-normed field". This can't happen in real or complex analysis.

I mean the latter.

What about the following names: normed_nondiscrete_field for a field which is not discrete (i.e., the norm does not take only the values 0, 1) and nondiscretely_normed_field for a field in which the norm takes dense values? I think they would lift the ambiguity.

[Johan Commelin]

How about nontrivially_normed_field for the former? And densely_normed_field for the latter?

[Sebastien Gouezel]

This also sounds great!

[Johan Commelin]

That means that the crazy number theorists with their p-adics can (ab)use discrete norms however they wish /s :stuck_out_tongue_wink:

[Sebastien Gouezel]

Yes, we can add discretely_normed_field to your naming scheme if needed. I think I like it!

[Jireh Loreaux]

Alright, I'm ready to make this happen, but I need to check the consensus, so let's try another poll. I will summarize the thread so that people who vote don't have to read the entire thing.

1. There is currently a type class nondiscrete_normed_field (so named because they are precisely the normed fields in which no point is isolated). For the moment we will call this type class X
2. We have need of a stronger type class on normed fields ensuring that the range of the norm is dense in ℝ. That these classes do not coincide can be shown by considering the $p$-adics. For the moment we will call this type class Y.
3. In the literature, X is sometimes called a nontrivial normed field (or a normed field for which the valuation is nontrivial), whereas for Y (perhaps confusingly for users of mathlib) they say the valuation is nondiscrete.
4. We definitely need to add a new type class for Y, which needs a name, and we need to consider renaming X depending on what we choose for Y. There have been some proposals above which I have tried to incorporate in the poll below. As always, feel free to add your own suggestions.

Pinging all the people who were involved in this thread at some point: @Sebastien Gouezel , @Johan Commelin , @Kevin Buzzard , @Oliver Nash , @Floris van Doorn , @Reid Barton , @Mario Carneiro , @Heather Macbeth , @Antoine Chambert-Loir , @Moritz Doll , @Junyan Xu , @Eric Wieser , @Yaël Dillies , @Anatole Dedecker , @Kenny Lau

[Jireh Loreaux]

/poll Names for type classes X / Y above
nondiscrete_normed_field / densely_normed_field
nontrivially_normed_field / densely_normed_field
nontrivially_normed_field / nondiscretely_normed_field
nontrivial_normed_field / nondiscrete_normed_field
normed_nondiscrete_field / nondiscretely_normed_field

[Kevin Buzzard]

Are the people who feel like "discrete" should mean "topology generated by |.| on source is discrete" precisely the people whose norms are archimedean, and those who feel that "discrete" should mean "image of |.| in target is discrete" precisely the people whose norms are nonarchimedean? I guess it is precisely this point (the choice of the fundamental relationship between norm and +) where the geometric ideas start to diverge (the continuum vs the profinite).

[Jireh Loreaux]

#15625 for the nondiscrete_normed_field → nontrivially_normed_field rename; densely normed fields should follow tonight or tomorrow.

[Yaël Dillies]

Argh, this will probably quite conflict with #15619

[Jireh Loreaux]

yeah, I just saw #15619, sorry. #15625 is on the queue now, so hopefully you can merge it in a few hours.

[Jireh Loreaux]

#15657 for the new densely_normed_field.

[Yaël Dillies]

Aaaah, conflicts :rofl:

[Jireh Loreaux]

They should be minor, and I expect yours to be merged first, so it will be my turn to resolve them.

[Jireh Loreaux]

@Heather Macbeth since you needed it: #15657 is merged now.