uniform split

Stream: maths

[Patrick Massot]

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]

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

[Johannes Hölzl]

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

Thank you very much for investigating

[Patrick Massot]

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]

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

[Mario Carneiro]

it's like the option coe

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

This will prevent it from being used more than once

[Patrick Massot]

Nice trick!

[Kevin Buzzard]

That's an interesting comment!

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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

[Johan Commelin]

We now have both

[Johannes Hölzl]

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]

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]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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]

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]

yes

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

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]

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]

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

[Sebastien Gouezel]

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

[Patrick Massot]

they are

[Sebastien Gouezel]

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]

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]

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

[Sebastien Gouezel]

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]

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)