Zulip Chat Archive
Stream: maths
Topic: Ring completion
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.
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?
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
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
Patrick Massot (Dec 18 2018 at 14:21):
while still first getting rid of the separation issue
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
Johan Commelin (Dec 18 2018 at 14:23):
Cool! Congrats on completing this! :tada:
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
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?
Patrick Massot (Dec 18 2018 at 14:27):
It's part of my excuse for creating this mess
Patrick Massot (Dec 18 2018 at 14:28):
I mean this mess: instance : has_coe α (hcompletion α) := ⟨quotient.mk ∘ Cauchy.pure_cauchy ∘ quotient.mk⟩
Kevin Buzzard (Dec 18 2018 at 14:28):
If it works, it works :-)
Kenny Lau (Dec 18 2018 at 14:30):
you can't maintain a library by bodging...
Patrick Massot (Dec 18 2018 at 14:31):
It has a very clean interface since it solves a very clearly specified universal problem
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?
Patrick Massot (Dec 18 2018 at 14:33):
The transport idea was already a work-around actually
Patrick Massot (Dec 18 2018 at 14:56):
The big thing is at https://github.com/PatrickMassot/mathlib/commit/6dbdbbfe5304e85d95784f18d9a978ab129a84c8
Patrick Massot (Dec 18 2018 at 14:57):
That's 500 more lines to completion.lean
Patrick Massot (Dec 18 2018 at 14:59):
But some of them should move elsewhere, independently of the reorganization discussion
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
Patrick Massot (Dec 18 2018 at 15:04):
I'd like to get @Johannes Hölzl input before finishing restating stuff for hcompletion
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
Patrick Massot (Dec 18 2018 at 15:05):
I need them as assumption for many statements
Johannes Hölzl (Dec 18 2018 at 15:05):
Yes, there its okay
Patrick Massot (Dec 18 2018 at 15:05):
and the most important piece is the composition lemma
Patrick Massot (Dec 18 2018 at 15:05):
Patrick Massot (Dec 18 2018 at 15:06):
This is what make this so convenient
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 asmin_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.
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: Dec 20 2023 at 11:08 UTC