## Stream: maths

### Topic: Ring completion

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): #### 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): https://github.com/PatrickMassot/mathlib/commit/6dbdbbfe5304e85d95784f18d9a978ab129a84c8#diff-f7d0385aaa9b17579cee0f2af9cc9135R120 #### 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 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.

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