Zulip Chat Archive

Stream: maths

Topic: uniform split


Patrick Massot (Mar 03 2019 at 18:50):

I put a lot of work in splitting the uniform space + topological structure + completions mess, in https://github.com/leanprover-community/mathlib/tree/uniform_split But I'm stuck in type class hell. After two suspicious fix in exponential.lean and operator_norm.lean, I'm stuck again in bounded_continuous_map.lean. Clearly there is something wrong, and I can't find what. Help would be very much appreciated @Johannes Hölzl @Mario Carneiro

Patrick Massot (Mar 03 2019 at 18:51):

I'm afraid it wont' be possible to help without checking out the branch and try to make it compile

Johannes Hölzl (Mar 04 2019 at 11:58):

@Patrick Massot I think a problem is the has_coe α (completion α) instance for uniform space completions. At last comparing the type class searches for the old and new version it looks like it diverges at this point.

I don't know how the completion mechanism works exactly. But we have transitivity rules. Maybe this means the type class mechanism will try to find a compitions of α -> (completion α) -> (completion (completion α) ) -> .... I think we need to remove this completion. I guess we should remove this coercion.

Patrick Massot (Mar 04 2019 at 11:59):

Thank you very much for investigating

Patrick Massot (Mar 04 2019 at 11:59):

I managed to fix the build by providing an explicit instance term. But I shows once again that the type class mechanism is very brittle

Patrick Massot (Mar 04 2019 at 12:03):

I added https://github.com/leanprover-community/mathlib/blob/uniform_split/src/topology/bounded_continuous_function.lean#L263

Mario Carneiro (Mar 04 2019 at 12:03):

it's like the option coe

Patrick Massot (Mar 04 2019 at 12:04):

It's not a pretty line. But if it allows to keep has_coe α (completion α) it's fine

Mario Carneiro (Mar 04 2019 at 12:05):

you need to inhabit has_coe_t A (completion A) instead of has_coe A (completion A)

Mario Carneiro (Mar 04 2019 at 12:06):

This will prevent it from being used more than once

Patrick Massot (Mar 04 2019 at 12:07):

Nice trick!

Kevin Buzzard (Mar 04 2019 at 12:07):

That's an interesting comment!

Patrick Massot (Mar 04 2019 at 12:07):

Lunch is calling, please don't hesitate to review https://github.com/leanprover-community/mathlib/pull/787

Patrick Massot (Mar 04 2019 at 12:08):

I think this is a much more useful cleanup than the basic topology one, because the current organization is really crazy (and I'm talking about mess I very much contributed to create)

Kevin Buzzard (Mar 04 2019 at 12:09):

Patrick -- are you sure you even want a coercion? Kenny had a coercion from R to R[1/S] and IIRC did not even name the function, and all that happened was that Johan and I got frustrated that this completely fundamental map did not have a name. We both seemed very happy to apply the map explicitly when we needed it.

Kevin Buzzard (Mar 04 2019 at 12:09):

In the end the map was named of and it is not hard to write two letters.

Johan Commelin (Mar 04 2019 at 12:10):

We now have both

Johannes Hölzl (Mar 04 2019 at 12:10):

It looks like has_coe_t is not enough. I think it is only activated once, but then the type class search explodes. I'm in favor of removing this coercion.

Patrick Massot (Mar 04 2019 at 12:52):

it seems crazy to me to remove this coercion, especially since it's only current cost is one line in the middle of a proof

Patrick Massot (Mar 04 2019 at 12:53):

Anyway, I intend to redo this completion stuff from scratch, following Bourbaki. So we can keep the coercion for now, and I'll try to avoid it when I'll do the Bourbaki completion

Sebastien Gouezel (Mar 04 2019 at 13:02):

What is your motivation to redo completion from scratch? Are there some facts that are not yet proved, and that a different approach would make much easier to prove?

Patrick Massot (Mar 04 2019 at 13:10):

With the current construction, it's complicated to do the Hausdorff completion in two stages : first get something separated and then complete. Because the current construction quotients the space of all Cauchy filters to make it separated. If you start with something separated and take the space of all Cauchy filters then you loose separation, and you still need to quotient. So the map you get is a composition of three maps instead of two.

Patrick Massot (Mar 04 2019 at 13:11):

This is crucial for ring completion because extending the multiplication requires to first get a separated ring

Patrick Massot (Mar 04 2019 at 13:13):

I don't know where Johannes got this idea, but what Bourbaki does is to consider the space of minimal Cauchy filters. This way you get a complete Hausdorff space in one shot. I don't intend to delete the separate construction of the uniform structure on the space of all Cauchy filters, but it wouldn't be used in the construction of the Hausdorff completion anymore

Sebastien Gouezel (Mar 04 2019 at 13:16):

OK, I understand this would certainly be more elegant and more efficient. But haven't all the desired properties already been established in the current framework? I mean, once the construction is done, one just needs to use the API and one can forget about the construction -- unless you want some things to be defeq while they are not currently, maybe?

Patrick Massot (Mar 04 2019 at 13:18):

Ok, I fixed the type class issue with my latest commit. I completed the isolation of completions by a further file split.

Patrick Massot (Mar 04 2019 at 13:21):

Sébastien, I do have a branch where ring completions actually work in full generality (it's not in mathlib yet), but it's really a hack, and I fear this will bite us at some point. See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Ring.20completion for details

Sebastien Gouezel (Mar 04 2019 at 13:24):

OK, I just noticed that in mathlib the ring completion is only done for separated rings currently. And to push this to nonseparated rings you run into trouble, right?

Patrick Massot (Mar 04 2019 at 13:24):

yes

Patrick Massot (Mar 04 2019 at 13:25):

I don't know any way to extend multiplication to the completion if the ring is not separated.

Patrick Massot (Mar 04 2019 at 13:26):

What Bourbaki does to handle non separated ring is to first make them separated, and then take the (separated) completion of the separated ring.

Patrick Massot (Mar 04 2019 at 13:28):

One important point is to understand that the subcategory of complete (but not necessarily separated) uniform space is not a nice subcategory. Because you cannot extend by uniform continuity if the target space is not separated

Patrick Massot (Mar 04 2019 at 13:29):

Anyway, I think this reorganization was needed even without redoing completions. I hope it's ready for merge now. It's really painful to do this kind of work, but I hope it will pay in the long run

Sebastien Gouezel (Mar 04 2019 at 13:29):

So you will have in any case to prove the first step: go from the nonseparated case to the separated one. For the second step, you could either use the elegant approach of Bourbaki, or use the current formalization, right?

Patrick Massot (Mar 04 2019 at 13:38):

The first step is in https://github.com/leanprover-community/mathlib/blob/uniform_split/src/topology/uniform_space/separation.lean#L98. Using the current formalization for the second step is what is currently in my https://github.com/PatrickMassot/mathlib/commit/6dbdbbfe5304e85d95784f18d9a978ab129a84c8#diff-f7d0385aaa9b17579cee0f2af9cc9135R120 branch. But it leads to https://github.com/PatrickMassot/mathlib/commit/6dbdbbfe5304e85d95784f18d9a978ab129a84c8#diff-f7d0385aaa9b17579cee0f2af9cc9135R1728

Patrick Massot (Mar 04 2019 at 13:39):

In all cases type theory will never let use have definitional equality between the two steps process and the one step process

Sebastien Gouezel (Mar 04 2019 at 13:50):

Now I am completely confused. Aren't hcompletion and completion canonically isomorphic, but not defeq?

Patrick Massot (Mar 04 2019 at 13:53):

they are

Sebastien Gouezel (Mar 04 2019 at 13:55):

Then you could pull the ring structure from hcompletion to completion, and say that if \alpha is a topological ring then completion \alpha is a topological ring, and this gives you an API with only one step, not mentioning hcompletion at all?

Patrick Massot (Mar 04 2019 at 13:57):

This is exactly the strategy that made me think we need to be able to pull back topological ring structures under uniform space isomorphisms. But, for some reason, this seems to be a non-trivial operation in type theory. So doing the direct construction (following Bourbaki) seems simpler

Patrick Massot (Mar 04 2019 at 13:58):

I can already do everything as in my old completions_reloaded branch. I'm trying to do it better

Sebastien Gouezel (Mar 04 2019 at 14:02):

If you're convinced it will be better in the end, go ahead, but you have not really convinced me for now that you will really be saving energy in this way, instead of pulling back multiplication from hcompletion and checking the continuity (this is the only thing you have to pull back, right, everything else is already there?). This is probably because I don't know the gory details, of which you are certainly much more aware than me!

Patrick Massot (Mar 04 2019 at 14:10):

We'll see. It will probably depend how much I need to fight to get a nice space of minimal Cauchy filters. I'm not there yet. Even after merging this, I plan to first propose a bunch of modification to uniform_space.basic (I didn't want to mix reorganization and actual changes in the same PR)


Last updated: Dec 20 2023 at 11:08 UTC