Zulip Chat Archive

Stream: maths

Topic: topological groups/add_groups


view this post on Zulip Johan Commelin (Mar 11 2019 at 12:15):

Do we already have statements that say to topological group/add_group topologies are the same iff they have the same nhds of 1 (resp. 0)?

view this post on Zulip Patrick Massot (Mar 11 2019 at 13:47):

This kind if question should be easier to answer now (that was one of the goal of the reorganization PRs). You have exactly one file that could contain this lemma: topology/algebra/group. So the answer is no

view this post on Zulip Patrick Massot (Mar 11 2019 at 13:48):

However it follows very easily from stuff that is there, after you add a lemma which should be obviously in topology/basic.

view this post on Zulip Patrick Massot (Mar 11 2019 at 13:48):

import topology.algebra.group

lemma topological_space.eq_iff_nhds {α : Type*} (t t' : topological_space α)
 (h :  x, @nhds α t x = @nhds α t' x) : t = t' :=
begin
  apply topological_space_eq,
  ext s,
  change @is_open _ t s  @is_open _ t' s,
  simp only [is_open_iff_mem_nhds, h]
end

lemma topological_group.ext {G : Type*} [group G] (t t' : topological_space G)
  (tg : @topological_group G t _) (tg' : @topological_group G t' _)
  (h : @nhds G t 1 = @nhds G t' 1) : t = t' :=
topological_space.eq_iff_nhds t t' $ λ x, by
  rw [ @nhds_translation_mul_inv G t _ _ x ,  @nhds_translation_mul_inv G t' _ _ x ,  h]

view this post on Zulip Patrick Massot (Mar 11 2019 at 13:49):

Of course it's a bit annoying to see all those @ but the type class system is not convenient when you want to discuss different topologies on a given type

view this post on Zulip Patrick Massot (Mar 11 2019 at 13:51):

The first lemma is part of a bigger hole in the API. I think we don't have the lemma telling you that, under suitable conditions, a map from α to filter α is nhds for a (unique) topology on α

view this post on Zulip Johan Commelin (Mar 11 2019 at 14:11):

Thanks for these lemma's Patrick. They are now in for_mathlib/topology :grinning:

view this post on Zulip Johannes Hölzl (Mar 11 2019 at 14:37):

topological_space.eq_iff_nhds is called eq_of_nhds_eq_nhds

view this post on Zulip Patrick Massot (Mar 11 2019 at 14:41):

oops, it accidentally went to topology/order where I wasn't looking for it...

view this post on Zulip Patrick Massot (Mar 11 2019 at 14:42):

ooh, it's because you indeed proved it using the order on topologies

view this post on Zulip Patrick Massot (Mar 11 2019 at 14:44):

Johannes, do you know if the construction of a topology from a suitable function from X to filter X is there?

view this post on Zulip Johannes Hölzl (Mar 11 2019 at 15:23):

mk_of_nhds

view this post on Zulip Johannes Hölzl (Mar 11 2019 at 15:24):

Then what you want is: nhds_mk_of_nhds which tells you that the neighbourhoods of mk_of_nhds are the right ones

view this post on Zulip Patrick Massot (Mar 11 2019 at 15:39):

I don't know why I can't find anything in mathlib today, but thanks!

view this post on Zulip Kevin Buzzard (Mar 11 2019 at 15:40):

https://github.com/leanprover-community/mathlib/issues/629

view this post on Zulip Kevin Buzzard (Mar 11 2019 at 15:41):

Johannes -- what will we do without you!

view this post on Zulip Patrick Massot (Mar 11 2019 at 15:43):

My memory is even worse than I feared. I just thought: why isn't this used in topology/algebra/group when constructing a group topology from a filter around zero? Answer: it is used there.

view this post on Zulip Patrick Massot (Mar 11 2019 at 16:11):

oops, I mistakenly pushed directly to mathlib master while I wanted to create a PR. This was a six lines addition, I hope it's fine

view this post on Zulip Patrick Massot (Mar 11 2019 at 16:12):

@Johannes Hölzl please don't hesitate to complain, I can still push corrections :blushing:

view this post on Zulip Johannes Hölzl (Mar 11 2019 at 16:33):

No problem, looks good to me.


Last updated: May 18 2021 at 07:19 UTC