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