Zulip Chat Archive

Stream: maths

Topic: Ring completion


view this post on Zulip Patrick Massot (Dec 18 2018 at 14:16):

@Johannes Hölzl I think I just completed the topological ring completion project. Remember where we got stuck last time: we could define a ring structure on completion a assuming that a was a separated topological ring, see https://github.com/leanprover/mathlib/blob/master/analysis/topology/completion.lean#L1168. We could also construct a ring structure on quotient (separatation_setoid a), see https://github.com/leanprover/mathlib/blob/master/analysis/topology/quotient_topological_structures.lean#L204. I did that by leveraging the algebraic quotient construction, using that the separation relation for uniform groups is the same as the left coset relation for the closure of zero. This meant fighting the system to use an equivalence relation equality to relate the quotients. Then I constructed https://github.com/leanprover/mathlib/blob/master/analysis/topology/completion.lean#L710-L711 completion (quotient $ separatation_setoid a) ≃ completion α which I hoped to use to glue the preceding two constructions and get a ring structure on completion α. But this meant fighting Lean again, for lack of transport of structure along this equiv.

view this post on Zulip Johannes Hölzl (Dec 18 2018 at 14:18):

Yes, I remember. How did you solve it. Or did you copy the structure and wrote down the transport for each rule?

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:19):

So I backtracked completely. I defined a ring structure on sep_quot α := quotient (separatation_setoid a) directly, using the link between the separation relation and the closure of zero only in the lemma proving that multiplication descends to the quotient. And then I defined hcompletion α := completion (sep_quot α). This looks really weird because remember completion α := quotient (separation_setoid $ Cauchy α), so we use the separation relation twice. But it works very smoothly

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:21):

Remember how Bourbaki does it: they replace Cauchy α with the space of minimal Cauchy filters on α. And they define the completion as min_cauchy (quotient $ separatation_setoid a). That's how they avoid the double quotient

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:21):

while still first getting rid of the separation issue

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:22):

I didn't start that road because I saw you did everything with non-minimal Cauchy filters. And of course all three constructions solve the same universal problem, so there are uniquely isomorphic

view this post on Zulip Johan Commelin (Dec 18 2018 at 14:23):

Cool! Congrats on completing this! :tada:

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:24):

The messy thing with my construction is that completion α becomes a purely intermediate thing, still with a rather large theory, which needs to be restated for hcompletion

view this post on Zulip Kevin Buzzard (Dec 18 2018 at 14:26):

Is "Bourbaki did it this way" an argument for or against "Lean should do it this way", or are they just independent things?

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:27):

It's part of my excuse for creating this mess

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:28):

I mean this mess: instance : has_coe α (hcompletion α) := ⟨quotient.mk ∘ Cauchy.pure_cauchy ∘ quotient.mk⟩

view this post on Zulip Kevin Buzzard (Dec 18 2018 at 14:28):

If it works, it works :-)

view this post on Zulip Kenny Lau (Dec 18 2018 at 14:30):

you can't maintain a library by bodging...

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:31):

It has a very clean interface since it solves a very clearly specified universal problem

view this post on Zulip Kevin Buzzard (Dec 18 2018 at 14:32):

Is one of the the issues that we need to transport theorems along isomorphisms and this is still not yet possible, so we fudge our way around it?

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:33):

The transport idea was already a work-around actually

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:56):

The big thing is at https://github.com/PatrickMassot/mathlib/commit/6dbdbbfe5304e85d95784f18d9a978ab129a84c8

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:57):

That's 500 more lines to completion.lean

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:59):

But some of them should move elsewhere, independently of the reorganization discussion

view this post on Zulip Patrick Massot (Dec 18 2018 at 15:01):

It includes using def function.comp₂ (f : α → β → γ) (g : γ → δ) : α → β → δ := λ x y, g (f x y) and its companions def continuous₂ (f : α → β → γ) := continuous (function.uncurry f) etc to nicely handle functions of two variables (like addition and multiplication), as was mentioned in another thread

view this post on Zulip Patrick Massot (Dec 18 2018 at 15:04):

I'd like to get @Johannes Hölzl input before finishing restating stuff for hcompletion

view this post on Zulip Johannes Hölzl (Dec 18 2018 at 15:04):

I think continuous₂ and uniform_continuous₂ should be fully transparent, without any rules about them. So only use them when writing down concrete instances

view this post on Zulip Patrick Massot (Dec 18 2018 at 15:05):

I need them as assumption for many statements

view this post on Zulip Johannes Hölzl (Dec 18 2018 at 15:05):

Yes, there its okay

view this post on Zulip Patrick Massot (Dec 18 2018 at 15:05):

and the most important piece is the composition lemma

view this post on Zulip Patrick Massot (Dec 18 2018 at 15:05):

https://github.com/PatrickMassot/mathlib/commit/6dbdbbfe5304e85d95784f18d9a978ab129a84c8#diff-f7d0385aaa9b17579cee0f2af9cc9135R120

view this post on Zulip Patrick Massot (Dec 18 2018 at 15:06):

This is what make this so convenient

view this post on Zulip Patrick Massot (Dec 18 2018 at 17:31):

Remember how Bourbaki does it: they replace Cauchy α with the space of minimal Cauchy filters on α. And they define the completion as min_cauchy (quotient $ separatation_setoid a). That's how they avoid the double quotient

I just checked, and actually the above is not quite correct. It seems that minimal Cauchy filters are already separated.

view this post on Zulip Patrick Massot (Dec 18 2018 at 17:34):

So this is a really more economical way of building the Hausdorff completion. But they don't solve problem of factorizing morphisms into complete spaces (not hausdorff complete spaces), whereas we do it.


Last updated: May 09 2021 at 09:11 UTC