# Zulip Chat Archive

## Stream: maths

### Topic: topological groups/add_groups

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