## Stream: maths

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

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

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

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


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

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

#### Johan Commelin (Mar 11 2019 at 14:11):

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

#### Johannes Hölzl (Mar 11 2019 at 14:37):

topological_space.eq_iff_nhds  is called eq_of_nhds_eq_nhds

#### Patrick Massot (Mar 11 2019 at 14:41):

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

#### Patrick Massot (Mar 11 2019 at 14:42):

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

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

#### Johannes Hölzl (Mar 11 2019 at 15:23):

mk_of_nhds

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

#### Patrick Massot (Mar 11 2019 at 15:39):

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

#### Kevin Buzzard (Mar 11 2019 at 15:40):

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

#### Kevin Buzzard (Mar 11 2019 at 15:41):

Johannes -- what will we do without you!

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

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

#### Patrick Massot (Mar 11 2019 at 16:12):

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

#### Johannes Hölzl (Mar 11 2019 at 16:33):

No problem, looks good to me.

Last updated: May 18 2021 at 07:19 UTC