topological groups/add_groups

Stream: maths

[Johan Commelin]

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]

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]

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

[Patrick Massot]

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]

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]

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]

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

[Johannes Hölzl]

topological_space.eq_iff_nhds is called eq_of_nhds_eq_nhds

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Johannes Hölzl]

mk_of_nhds

[Johannes Hölzl]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Johannes -- what will we do without you!

[Patrick Massot]

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]

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]

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

[Johannes Hölzl]

No problem, looks good to me.