## 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

#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/

#### 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 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.

Last updated: May 10 2021 at 19:16 UTC