## Stream: maths

### Topic: class vs def again

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

#### Patrick Massot (Jul 16 2018 at 21:11):

What should we do?

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

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

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

#### Mario Carneiro (Jul 16 2018 at 22:16):

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

#### Mario Carneiro (Jul 16 2018 at 22:16):

i.e. take a default value

#### Patrick Massot (Jul 16 2018 at 22:16):

It depends on dense_embedding.extend we were discussing earlier today

#### Mario Carneiro (Jul 16 2018 at 22:18):

dense_embedding.extend doesn't require continuity

#### Mario Carneiro (Jul 16 2018 at 22:18):

oh, weird, a unique exists

#### Patrick Massot (Jul 16 2018 at 22:19):

well, it doesn't require it until ext_e_eq

#### Patrick Massot (Jul 16 2018 at 22:19):

unique exitsts are everywhere in this abstract nonsense business

#### Patrick Massot (Jul 16 2018 at 22:19):

That's an important part of the universal property

#### Mario Carneiro (Jul 16 2018 at 22:19):

oh sure, but mathlib basically never uses it

#### Mario Carneiro (Jul 16 2018 at 22:20):

it always defines the unique thing with a concrete term

#### Patrick Massot (Jul 16 2018 at 22:20):

that's because it lacks basic category theory support

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

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

#### Mario Carneiro (Jul 16 2018 at 22:21):

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

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

#### Mario Carneiro (Jul 16 2018 at 22:22):

I'm sure Kevin can discuss his experiences with sqrt_exists

#### Patrick Massot (Jul 16 2018 at 22:23):

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

right

#### Mario Carneiro (Jul 16 2018 at 22:24):

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

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

#### Patrick Massot (Jul 16 2018 at 22:24):

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

#### Mario Carneiro (Jul 16 2018 at 22:25):

Still, you've constructed the term

#### Mario Carneiro (Jul 16 2018 at 22:25):

g in the proof

#### Patrick Massot (Jul 16 2018 at 22:25):

this uses uniform continuity

#### Patrick Massot (Jul 16 2018 at 22:25):

no, g needs compat

#### Mario Carneiro (Jul 16 2018 at 22:25):

right, it's defined by lift on the quotient

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

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

#### Patrick Massot (Jul 16 2018 at 22:27):

Then I don't understand what you suggest

#### Mario Carneiro (Jul 16 2018 at 22:27):

If A is empty, is completion A also empty?

yes

(I hope)

#### Patrick Massot (Jul 16 2018 at 22:28):

In my mind it is certainly empty

#### Patrick Massot (Jul 16 2018 at 22:28):

but I'm not an expert in zerology

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

#### Patrick Massot (Jul 16 2018 at 22:36):

Oh. This is twisted

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

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

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

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

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

#### Patrick Massot (Jul 19 2018 at 09:12):

Maybe. He also doesn't answer emails.

#### Patrick Massot (Jul 19 2018 at 13:05):

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

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