Zulip Chat Archive

Stream: general

Topic: maximal elements


Patrick Massot (Mar 13 2019 at 15:31):

I'm again mathlib-blind. Who can help me find maximal elements of a poset, and their API?

Mario Carneiro (Mar 13 2019 at 15:39):

I don't think we have anything for that. Usually we just write out the condition, e.g. zorn

Patrick Massot (Mar 13 2019 at 15:40):

I can't believe Johannes missed an opportunity to write a general order API

Sebastien Gouezel (Mar 13 2019 at 15:51):

I was surprised I had to add several lemmas on orders and unions for #PR816. It seems there is no end to what will be ever needed about this.

Patrick Massot (Mar 13 2019 at 15:52):

What a subtle way to advertise a new PR!

Sebastien Gouezel (Mar 13 2019 at 15:53):

Almost half of the PR is about orders and general lemmas, in fact!

Sebastien Gouezel (Mar 13 2019 at 15:53):

And yes, very nice PR indeed :)

Patrick Massot (Mar 13 2019 at 15:57):

It may have helped to cut the PR in two pieces. The order stuff could be reviewed completely independently

Patrick Massot (Mar 13 2019 at 15:57):

This is is still an amazing PR

Kevin Buzzard (Mar 13 2019 at 15:57):

#816

Kevin Buzzard (Mar 13 2019 at 15:58):

seemed like the easiest way to get my browser to go to it

Kevin Buzzard (Mar 13 2019 at 16:00):

So we're on the way to the open mapping theorem?

Sebastien Gouezel (Mar 13 2019 at 16:00):

Yes, that's the next PR :)

Sebastien Gouezel (Mar 13 2019 at 16:02):

Especially, the last lemma of #816 is written directly for this.

Patrick Massot (Mar 13 2019 at 16:02):

I'm a bit lost in all your work. What happened to the Gromov-Hausdorff distance, is it merged in mathlib?

Sebastien Gouezel (Mar 13 2019 at 16:04):

Not submitted to mathlib yet, because it builds on not-yet merged PRs (#743 completion of metric spaces, #732 inductive limit of metric spaces).

Patrick Massot (Mar 13 2019 at 16:05):

Ok, this is what I thought. So you began another thread of PR to keep you busy?

Sebastien Gouezel (Mar 13 2019 at 16:05):

You know the power of procrastination: I had to refer a paper, so I decided to do the open mapping theorem instead.

Patrick Massot (Mar 13 2019 at 16:06):

http://www.structuredprocrastination.com/

Mario Carneiro (Mar 13 2019 at 17:31):

heh, this article definitely resonates with me

Sebastien Gouezel (Mar 15 2019 at 16:17):

It turns out that the open mapping theorem requires the base field to have an element with norm different from 1 (exercise: construct a counter-example over F_2 with the trivial norm). There are three options:

  • add this as an assumption to the theorem
  • add a typeclass about this, and check that R, C and p-adics are instances of this typeclass
  • add this to the very definition of normed_field, since it makes no sense anyway to use a normed field with all elements of norm 1.

My preferred option is clearly the third one, but I would like to have your opinion on this (especially, maybe I am missing some applications of stupid normed fields).

By the way, In Bourbaki, they call this "corps valué non-discret", which collides nicely with the definition of "discrete field" in Lean.

Johan Commelin (Mar 15 2019 at 16:27):

Does Bourbaki say anything about "corps valué discret" and why they might be interesting?

Sebastien Gouezel (Mar 15 2019 at 17:01):

No, in nontrivial theorems they always use "corps valué non-discret" and I did not find anything about "corps valué discret"

Mario Carneiro (Mar 15 2019 at 17:38):

I think the trivial norm is as much a norm as the discrete metric is a metric

Sebastien Gouezel (Mar 15 2019 at 17:55):

Sure. We could have a typeclass normed_field and a typeclass nondiscrete_normed_field extending it. But if there are absolutely no applications of normed_field, then what is the point of complicating uselessly the typeclass graph, which is already complicated enough? This is really different from metric spaces, where one uses routinely finite metric spaces.

Mario Carneiro (Mar 15 2019 at 18:19):

there are finite fields?

Kevin Buzzard (Mar 15 2019 at 18:53):

I think the trivial norm is as much a norm as the discrete metric is a metric

Actually the theory becomes quite different for non-trivial norms. The book "non-archimedean analysis" by Bosch, Guentzer and Remmert, which I read from cover to cover as a post-doc, starts with the words "let k be a field complete with respect to a non-trivial non-archimedean norm", and this non-triviality hypothesis is never dropped. I was skeptical (like Mario is now) -- surely the results are going to be true in the case where the norm is trivial, but just uninteresting. But actually the non-triviality really plays an important role -- it enables one to scale vectors so they have norm at most 1. A fundamental result about Banach spaces is that a map between them is continuous if and only if it is bounded. The proof crucially needs an element of non-trivial norm, and indeed turns out to be false for vector spaces over fields with trivial norm, because there is no topology so everything is continuous, but things are not in general bounded. Because a huge amount of the theory depends on this foundational result, I suspect that this is why the non-triviality of the norm is introduced right from the outset in BGR.

Sebastien Gouezel (Mar 15 2019 at 19:26):

there are finite fields?

Yes, there are finite fields, but you will never use them as normed fields.

Kevin Buzzard (Mar 15 2019 at 19:27):

Every single example I've seen of a trivial norm on a field is to say "oh look, this lemma works even if the norm is trivial, and it turns into a standard algebraic fact which we all knew, and which we probably assumed in the middle of the proof of the lemma"

Kevin Buzzard (Mar 15 2019 at 19:28):

However in the perfectoid project it is essential that we allow trivial valuations.

Kevin Buzzard (Mar 15 2019 at 19:29):

The difference is that we are doing ring theory not field theory perhaps

Sebastien Gouezel (Mar 15 2019 at 19:29):

Ha, that's an argument in favor of keeping the current normed_field. Then I will go for the solution nondiscrete_normed_field as a typeclass.

Johan Commelin (Mar 15 2019 at 19:30):

Oooh, but given one of those valuations, you still can't build a normed_field... they are too general.

Johan Commelin (Mar 15 2019 at 19:31):

Our valuations take values in some arbitrary lin.order.comm.group

Kevin Buzzard (Mar 15 2019 at 20:02):

Yes, we have already written a 1000 line valuation API where a valuation goes from a general commutative ring into a fairly general linearly ordered monoid (for example the nonnegative reals under multiplication)

Jan-David Salchow (Mar 17 2019 at 12:13):

I ran into the issue that I needed a normed_field to be non-discrete in showing that derivatives are unique #830 as well.

Jan-David Salchow (Mar 17 2019 at 12:14):

So I'm wondering, should we really have normed_field and nondiscrete_normed_field, or would potentially_discrete_normed_field and normed_field be better?

Sebastien Gouezel (Mar 17 2019 at 12:31):

The standard math terminology is really nondiscrete normed field, so I would rather keep it is at is now to avoid surprises to users. But I don't have a very strong opinion on this.

Nicolò Cavalleri (Jul 09 2021 at 11:43):

I happen to see this discussion now and actually I was used to say "valued field" for what is now a normed field in mathlib and "normed field" for the same thing except for requiring the inequality fgfg{\vert f \cdot g\vert} \leq {\vert f\vert} \cdot {\vert g\vert} instead than the equality fg=fg{\vert f \cdot g\vert} = {\vert f\vert} \cdot {\vert g\vert}. This is also the convention used in nLab. Is @Sebastien Gouezel 's convention more common?

Sebastien Gouezel (Jul 09 2021 at 12:47):

I think you're right that the standard terminology is "valued field" when there is equality for the norm of a product.

Kevin Buzzard (Jul 09 2021 at 12:52):

If we're talking about a field then in the presence of the other axioms I would guess fgfg|fg|\leq|f||g| and fg=fg|fg|=|f||g| are equivalent? For commutative rings they can differ. I might be wrong though -- does someone know an example of a field with the <= axiom where = fails?

Kevin Buzzard (Jul 09 2021 at 12:55):

(I'm only thinking vaguely -- the reason |fg|<=|f||g| shows up is because this is true for the sup norm for functions on a space, but if the functions on a space are a field then the space only has one point so you get equality)

Kevin Buzzard (Jul 09 2021 at 12:59):

Maybe Q_p with the modified norm |0|m=0, |x|m=1 if 0<|x|<=1 and |x|m=|x| if |x|>1 is an example?

Nicolò Cavalleri (Jul 09 2021 at 13:40):

Kevin Buzzard said:

If we're talking about a field then in the presence of the other axioms I would guess fgfg|fg|\leq|f||g| and fg=fg|fg|=|f||g| are equivalent? For commutative rings they can differ. I might be wrong though -- does someone know an example of a field with the <= axiom where = fails?

I am not sure about this, but if they were equivalent shouldn't we require the weaker one?

Adam Topaz (Jul 09 2021 at 14:16):

The terminology in the following is what I consider as standard: https://en.wikipedia.org/wiki/Berkovich_space


Last updated: Dec 20 2023 at 11:08 UTC