Zulip Chat Archive

Stream: maths

Topic: complete_groups


view this post on Zulip Patrick Massot (Sep 26 2018 at 20:01):

I think the last file you didn't edit is the one you accidentally removed yesterday: complete_groups.lean. Currently it's only purpose is the proof of extend_Z_bilin which is the crucial ingredient to extend the multiplication of a topological ring to its Hausdorff completion. Note that the separation in extend_Z_bilin and extend_Z_bilin_key is mostly because the proof was too long to elaborate for Lean to be used interactively (at least on my computer). But also, the key part is actually where stuff happens while the rest is massaging information which is already there. I'd be curious to see whether you can simplify this (I don't mean turn everything into term mode, I mean actual Lean or maths simplification). This closely follows Bourbaki (I can send you the pdf in English if needed) except that the massaging is completely implicit in Bourbaki.

view this post on Zulip Patrick Massot (Sep 26 2018 at 20:05):

I would also be very curious to know, now that you're almost done reviewing and editing my work on completions and topological groups, whether you think my work has been useful for mathlib or whether it would have been quicker for you to start from scratch. I won't be sad anyway, because all this was an important part of my Lean training.

view this post on Zulip Johannes Hölzl (Sep 26 2018 at 20:10):

I have an electronic copy of Bourbaki General Topology, Ch. 1 -4 (from 1995).

Your work is useful for mathlib! While I renamed and refactored a lot of stuff, it is still helpful to have a developed theory. Then its not about how to prove some things, but more on how I think it fits into mathlib.

view this post on Zulip Johannes Hölzl (Sep 26 2018 at 20:14):

having finally the general top-ring completion would be very nice. One thing I was thinking about is that is_Z_bilin is a duplication of the is_bilinear_map in tensor product. But we can merge both (or replace is_Z_bilin) when Mario finishes his module rewrite.

view this post on Zulip Patrick Massot (Sep 26 2018 at 20:16):

Oh sure, is_Z_bilin was written very quickly in order to be able to state the theorem. It could be replaced very easily with anything else

view this post on Zulip Patrick Massot (Sep 26 2018 at 20:20):

I'll spend the next two days traveling, but hopefully we'll have ring completions next week!

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 08:14):

ring completions is finished. Using your extend_Z_bilin, then it was straight forward!

view this post on Zulip Patrick Massot (Sep 27 2018 at 08:41):

I'm reading that on my phone in a train so I may be wrong but it looks like you assume the topological ring is separated. This is cheating.

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 08:59):

Hm, I see.

view this post on Zulip Patrick Massot (Sep 27 2018 at 08:59):

I think I already wrote that but I can't see it. You also need my description of the separation relation for topological groups

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 08:59):

This is a reason why it was so easy :-)

view this post on Zulip Patrick Massot (Sep 27 2018 at 09:01):

No, the main reason is that all the difficulty is in extend_Z_bilin

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 09:01):

group_separation_rel is in https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/topological_structures.lean#L333

view this post on Zulip Patrick Massot (Sep 27 2018 at 09:02):

Yes this is the lemma I'm referring to

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 09:03):

so, can we proof that separation is a subring?

view this post on Zulip Patrick Massot (Sep 27 2018 at 09:03):

It ensures multiplication descends (lifts in CS language)

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 09:04):

hm, but maybe its easier to do the lifting the proper way. i.e. combine extend and quotient.lift

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 09:04):

yes, that's how the completion of the group structure works.

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 10:02):

So this construction is not the one in Bourbaki, or is it? Do you have a reference explaining the proof to show that multiplication lifts?

view this post on Zulip Patrick Massot (Sep 28 2018 at 20:28):

I'm back from traveling, so I can answer this question. This construction is almost the construction in Bourbaki except that, again, their construction of the Hausdorff completion of anything is slightly different: first they quotient by the separation relation, and they take the space of minimal Cauchy filters. When doing ring completions, they first make a separated ring as I explained, and then go to the space of minimal Cauchy filters. In our setup, we only need to construct a (functorial) isomorphism between completion (quotient separation_setoid a) and completion a. If I remember correctly, I did that carefully on paper but not yet in Lean. Then we'll be ready to chain our two constructions (going from separated assumption to the completion, relying on extend_Z_bilin and going from no assumption to separated using group_separation_rel)

view this post on Zulip Patrick Massot (Sep 28 2018 at 20:36):

More details about this separation stuff: in Bourbaki GT this is III.6.4 page 276 (English edition), the discussion after Proposition 5. Remember we know (from group_separation_rel) we want to quotient by the closure of zero. This closure is a two-sided ideal. Indeed left multiplication by any element is continuous so the image of closure of zero is contained in the closure of the image of zero, which is zero. Same works with right multiplication of course. Now assume x and x' are equivalent, and y and y' are equivalent. Hence x-x' and y-y' are in our ideal. Write xy = (x-x')*y + x'*(y-y')+x'y'. The first two terms in RHS are in our ideal, so x'*y' is equivalent to x*y. I'm too tired for Lean tonight, but I'll do that if you don't do it first.

view this post on Zulip Kenny Lau (Sep 28 2018 at 20:41):

there's an English edition?

view this post on Zulip Andrew Ashworth (Sep 28 2018 at 20:45):

translation published in 1966 by Hermann

view this post on Zulip Mario Carneiro (Sep 28 2018 at 20:53):

I discovered this as well last week

view this post on Zulip Patrick Massot (Sep 28 2018 at 20:54):

https://www.springer.com/us/book/9783540642411

view this post on Zulip Patrick Massot (Sep 28 2018 at 20:55):

The Hermann edition is probably hard to find nowadays

view this post on Zulip Patrick Massot (Sep 28 2018 at 20:55):

I mistakenly bought that volume in English (I noticed when I was back at home)

view this post on Zulip Patrick Massot (Sep 29 2018 at 21:08):

https://github.com/leanprover-community/mathlib/commit/65fe82ac32a956340ce990e3eed7b1e85772e7c0

view this post on Zulip Patrick Massot (Sep 29 2018 at 21:11):

@Johannes Hölzl

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 21:55):

Is this "completion of a topological ring is a topological ring"?

view this post on Zulip Johannes Hölzl (Sep 29 2018 at 22:28):

We have the "completion of a topological Hausdorff ring is a topological ring". This is the essential step to remove the Hausdorff.


Last updated: May 14 2021 at 19:21 UTC