Zulip Chat Archive

Stream: maths

Topic: complete_groups

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.

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.

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.

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.

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

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!

Johannes Hölzl (Sep 27 2018 at 08:14):

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

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.

Johannes Hölzl (Sep 27 2018 at 08:59):

Hm, I see.

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

Johannes Hölzl (Sep 27 2018 at 08:59):

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

Patrick Massot (Sep 27 2018 at 09:01):

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

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

Patrick Massot (Sep 27 2018 at 09:02):

Yes this is the lemma I'm referring to

Johannes Hölzl (Sep 27 2018 at 09:03):

so, can we proof that separation is a subring?

Patrick Massot (Sep 27 2018 at 09:03):

It ensures multiplication descends (lifts in CS language)

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

Johannes Hölzl (Sep 27 2018 at 09:04):

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

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?

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)

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.