Zulip Chat Archive

Stream: maths

Topic: class vs def again


view this post on Zulip Patrick Massot (Jul 16 2018 at 21:10):

Variation on a well-known theme: should uniform continuity of a map f between uniform spaces a and b be a def or a class? Or should we bundle f and its uniform continuity? Currently we have a def and no bundling. As usual, this is all convenient to prove properties of individual maps, or compositions of two such maps. Now let's get functorial. I want to promote each such f to a map between the respective Hausdorff completions of a and b. Of course in math this would be called completion_lift f. This currently doesn't make sense in mathlib, we need a term h : uniform_continuous f. So we could write completion_lift f h. But f can be inferred from h, so common sense dictates it should be an implicit argument, and we end up with completion_lift h. And it looks weird. And it gets worse when stating and proving properties of completion_lift, especially functoriality that should read completion_lift f' ∘ f = (completion_lift f') ∘ completion_lift f but actually reads completion_lift (uniform_continuous.comp h h') = (completion_lift h') ∘ completion_lift h.

view this post on Zulip Patrick Massot (Jul 16 2018 at 21:11):

What should we do?

view this post on Zulip Patrick Massot (Jul 16 2018 at 21:26):

See https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/1e1fb6f6e6b03eb2e5d436851aaaa8e8fc3f1582/src/for_mathlib/completion.lean for the concrete situation

view this post on Zulip Patrick Massot (Jul 16 2018 at 21:30):

I had a lot of fun doing all this after proving the universal mapping property for completions. It was fun because it was really very close to a paper and pencil proof. But I wouldn't find it fun to do this ten times. I can't wait until we get nice abstract non-sense in mathlib. How far are we from merging @Scott Morrison PR? Has anyone heard from Scott recently?

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:07):

The last few times I've been asked this I advocated the bundled function approach and it's worked well thus far

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:10):

Question is then how to handle the existing code base? How to avoid duplicating too much stuff. I guess we still want to keep the current Prop

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:16):

Hm, good point. Is it possible to define completion_lift f without the continuity assumption?

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:16):

i.e. take a default value

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:16):

It depends on dense_embedding.extend we were discussing earlier today

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:17):

see https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/1e1fb6f6e6b03eb2e5d436851aaaa8e8fc3f1582/src/for_mathlib/completion.lean#L95-L96

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:18):

dense_embedding.extend doesn't require continuity

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:18):

oh, weird, a unique exists

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:19):

well, it doesn't require it until ext_e_eq

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:19):

unique exitsts are everywhere in this abstract nonsense business

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:19):

That's an important part of the universal property

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:19):

oh sure, but mathlib basically never uses it

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:20):

it always defines the unique thing with a concrete term

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:20):

that's because it lacks basic category theory support

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:20):

I don't want a definition with a concrete term, I want the abstract interface, as in my file

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:21):

no, there are plenty of places where math dictates a unique existence, it's just easier to work with terms

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:21):

If you look at scott's development I think he's done the same

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:22):

even the explicit construction of completion and to_completion will need to be complemented by a uniqueness up to unique iso result. This is my plan for tomorrow, as well as deducing that completion of a product is isomorphic to product of completions

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:22):

I'm sure Kevin can discuss his experiences with sqrt_exists

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:23):

Probably the best is to have an explicit term and a uniqueness lemma

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:23):

right

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:24):

the uniqueness lemma says something like x = my_thing <-> property

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:24):

I still don't know how to do that in this case. Because that de.ext is only half the construction. Then it must still descend to a quotient (lift to a quotient in Lean-speak)

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:24):

https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/1e1fb6f6e6b03eb2e5d436851aaaa8e8fc3f1582/src/for_mathlib/completion.lean#L99

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:25):

Still, you've constructed the term

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:25):

g in the proof

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:25):

this uses uniform continuity

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:25):

no, g needs compat

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:25):

right, it's defined by lift on the quotient

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:26):

I'm not asking you to prove the theorem without the assumption, or even do the construction without uniform continuity

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:27):

I want to see if you can do a similar thing to what I did for extend

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:27):

Then I don't understand what you suggest

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:27):

If A is empty, is completion A also empty?

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:27):

yes

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:27):

(I hope)

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:28):

In my mind it is certainly empty

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:28):

but I'm not an expert in zerology

view this post on Zulip Mario Carneiro (Jul 16 2018 at 22:31):

Then you can follow a similar proof to what I did. Define completion.extend f by cases on uniform_continuous f. If it is, do the regular thing. Otherwise, we can pick an arbitrary element of B by choice. We know it is nonempty because we are given an element of completion A so we can prove A is nonempty, so a : A means f a : B

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:36):

Oh. This is twisted

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:38):

I'll try that tomorrow, before moving on to products. It seems we don't have an instance for completion of a product of complete spaces, so there will be preparation work.

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:40):

If I'm lucky I'll even get a dense_embedding.extend without inhabitants in mathlib when I'll wake up :wink:

view this post on Zulip Patrick Massot (Jul 16 2018 at 22:41):

@Kevin Buzzard don't hesitate to have a look at the current state of https://github.com/PatrickMassot/lean-perfectoid-spaces/blob/completions/src/for_mathlib/completion.lean and comment. It's all for the perfectoid project.

view this post on Zulip Kevin Buzzard (Jul 17 2018 at 07:10):

Patrick I'm really grateful for all of this. The perfectoid project shouldn't be too hard to do. The hard part with schemes was proving that the structure presheaf on Spec(R) was a sheaf because this had all sorts of unexpected pitfalls. The analogous statement for adic spaces isn't true -- an affinoid adic space is defined to be an affinoid pre-adic space Spa(R) for which the structure presheaf happens to be a sheaf, so that is a huge hurdle that we don't have to deal with. Completions are, I think, the main technical issue left, and you are dealing with them. I will try and focus on continuous valuations.

view this post on Zulip Johan Commelin (Jul 19 2018 at 07:38):

Has anyone heard from Scott recently?

I haven't seen Scott here for a while. Maybe it's time for (winter?) holidays down under?

view this post on Zulip Patrick Massot (Jul 19 2018 at 09:12):

Maybe. He also doesn't answer emails.

view this post on Zulip Patrick Massot (Jul 19 2018 at 13:05):

His webpage revealed https://tqft.net/calendar/ which pretty clearly indicates winter vacations.

view this post on Zulip Johan Commelin (Jul 19 2018 at 14:40):

It also means he should be back next week (-;


Last updated: May 10 2021 at 08:14 UTC