Zulip Chat Archive

Stream: general

Topic: maximal elements


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 13 2019 at 15:40):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 13 2019 at 15:52):

What a subtle way to advertise a new PR!

view this post on Zulip Sebastien Gouezel (Mar 13 2019 at 15:53):

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

view this post on Zulip Sebastien Gouezel (Mar 13 2019 at 15:53):

And yes, very nice PR indeed :)

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 13 2019 at 15:57):

This is is still an amazing PR

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 15:57):

#816

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 15:58):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 16:00):

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

view this post on Zulip Sebastien Gouezel (Mar 13 2019 at 16:00):

Yes, that's the next PR :)

view this post on Zulip Sebastien Gouezel (Mar 13 2019 at 16:02):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 13 2019 at 16:06):

http://www.structuredprocrastination.com/

view this post on Zulip Mario Carneiro (Mar 13 2019 at 17:31):

heh, this article definitely resonates with me

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 15 2019 at 16:27):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 15 2019 at 18:19):

there are finite fields?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 19:28):

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 19:29):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 15 2019 at 19:31):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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