maximal elements

Stream: general

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Sebastien Gouezel]

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]

What a subtle way to advertise a new PR!

[Sebastien Gouezel]

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

[Sebastien Gouezel]

And yes, very nice PR indeed :)

[Patrick Massot]

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

[Patrick Massot]

This is is still an amazing PR

[Kevin Buzzard]

#816

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

Yes, that's the next PR :)

[Sebastien Gouezel]

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

[Patrick Massot]

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

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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

[Patrick Massot]

http://www.structuredprocrastination.com/

[Mario Carneiro]

heh, this article definitely resonates with me

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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

[Mario Carneiro]

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

[Sebastien Gouezel]

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]

there are finite fields?

[Kevin Buzzard]

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]

there are finite fields?

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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]

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]

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 ${\vert f \cdot g\vert} \leq {\vert f\vert} \cdot {\vert g\vert}$ instead than the equality ${\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]

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

[Kevin Buzzard]

If we're talking about a field then in the presence of the other axioms I would guess $|fg|\leq|f||g|$ and $|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]

(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]

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]

Kevin Buzzard said:

If we're talking about a field then in the presence of the other axioms I would guess $|fg|\leq|f||g|$ and $|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]

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