Zulip Chat Archive

Stream: general

Topic: quotient group is uniform


Jireh Loreaux (Aug 31 2022 at 16:13):

Under what conditions is the quotient G ⧸ N of a uniform group G by a normal subgroup N itself a uniform group? Does mathlib know this somewhere? To un- #xy, I'm trying to prove that the quotient of a complete metrizable group G by a closed normal subgroup N is complete, and the first step in Bourbaki is to show that the quotient is metrizable so that you can reduce to the problem to Cauchy sequences. I would have a proof of metrizability modulo knowing that G / N is a uniform group, and then I can tackle completeness.

Jireh Loreaux (Aug 31 2022 at 16:59):

@Patrick Massot I figure you might know this off the top of your head.

Patrick Massot (Aug 31 2022 at 17:35):

We have docs#quotient_group.quotient.topological_space so it shouldn't be difficult.

Jireh Loreaux (Aug 31 2022 at 21:40):

Sorry, I don't understand why this is particularly easy. I'm not claiming it isn't, only that I don't see it.

Kevin Buzzard (Aug 31 2022 at 21:44):

Let me say something possibly stupid: the quotient has a topology making it a topological group and hence a uniform group. Does this help?

Kevin Buzzard (Aug 31 2022 at 22:01):

Oh this can't help because I don't know whether I'm using the left uniformity or the right one

Jireh Loreaux (Aug 31 2022 at 22:01):

It has a topology making it into a uniform_space (via docs#topological_group.to_uniform_space), but not into a docs#uniform_group, as mentioned in the docstring to the former (because of possibly different left and right uniformities). So sure you can get the uniform space structure for free I guess, but then I don't immediately see how to get the uniform group structure.

Jireh Loreaux (Aug 31 2022 at 22:05):

I started trying to construct it directly from the uniform structure on the prequotient, but I'm not yet too comfortable with uniformities in mathlib, so I got stuck; and maybe this isn't the right way to go anyway.

Jireh Loreaux (Aug 31 2022 at 22:06):

import topology.algebra.uniform_group

variables {G : Type*} [group G] [uniform_space G] [uniform_group G]
  (S : subgroup G) [is_closed (S : set G)] [subgroup.normal S]

instance quotient_group.quotient.uniform_space : uniform_space (G  S) :=
{ uniformity := (uniformity G).map (λ g, (quotient_group.mk' S g.fst, quotient_group.mk' S g.snd)),
  refl := filter.le_map $ λ s hs,
  begin
    simp only [filter.mem_principal, id_rel_subset, set.mem_image, prod.mk.inj_iff, prod.exists],
    intros gs,
    rcases quotient_group.mk_surjective gs with g, rfl⟩,
    exact g, g, refl_mem_uniformity hs, rfl, rfl⟩,
  end,
  symm := λ s hs, symm_le_uniformity hs,
  comp := sorry,
  is_open_uniformity := sorry }

instance quotient_group.quotient.uniform_group : uniform_group (G  S) := sorry

Oliver Nash (Sep 01 2022 at 07:21):

I had a PR related to this relatively recently which I closed because I turned out not to need it and I needed to focus on other things. I doubt it's useful but here it is anyway: #16011

I realise this does not address your actual question (I don't know the answer and haven't thought about it but I suspect the answer is "always")

Anatole Dedecker (Sep 01 2022 at 08:05):

I am not sure at all that the answer is "always". Bourbaki makes no claim about it, right?

Oliver Nash (Sep 01 2022 at 08:06):

Indeed Bourbaki seems not to. I could be wrong!

Oliver Nash (Sep 01 2022 at 08:06):

Hence only "suspect".

Anatole Dedecker (Sep 01 2022 at 08:10):

Looking at the proof of what Jireh wants in Bourbaki, they don’t seem to be using that the quotient is a uniform group. They basically use docs#topological_space.metrizable_space_of_t3_second_countable right?

Anatole Dedecker (Sep 01 2022 at 08:15):

Oh not really because apparently you only need the uniformity to be countably generated

Anatole Dedecker (Sep 01 2022 at 09:06):

Which we have! This is docs#uniform_space.metrizable_space

Anatole Dedecker (Sep 01 2022 at 10:19):

import topology.metric_space.metrizable_uniformity

open topological_space filter set
open_locale topological_space uniformity

lemma filter.map.is_countably_generated {α β : Type*} (l : filter α) [H : l.is_countably_generated]
  (f : α  β) : (map f l).is_countably_generated :=
begin
  unfreezingI {rw is_countably_generated_iff_exists_antitone_basis at *; rcases H with u, hu⟩},
  exact ⟨(image f)  u, hu.to_has_basis.map _, monotone_image.comp_antitone hu.antitone⟩⟩
end

lemma quotient_group.nhds_eq {G : Type*} [group G] [topological_space G]
  [topological_group G] {N : subgroup G}(x : G) : 𝓝 (x : G  N) = map coe (𝓝 x) :=
le_antisymm ((quotient_group.is_open_map_coe N).nhds_le x) continuous_quot_mk.continuous_at

lemma quotient_metrizable {G : Type*} [group G] [topological_space G] [metrizable_space G]
  [topological_group G] {N : subgroup G} [N.normal] [is_closed (N : set G)] :
  metrizable_space (G  N) :=
begin
  letI : uniform_space (G  N) := topological_group.to_uniform_space (G  N),
  haveI : is_countably_generated (𝓝 (1 : G  N)),
  { change is_countably_generated (𝓝 ((1 : G) : G  N)),
    rw quotient_group.nhds_eq,
    exact filter.map.is_countably_generated _ _ },
  haveI : is_countably_generated (𝓤 (G  N)),
  { refine comap.is_countably_generated _ _, },
  refine uniform_space.metrizable_space,
end

Jireh Loreaux (Sep 01 2022 at 15:44):

Thanks Anatole!

Jireh Loreaux (Sep 01 2022 at 15:46):

I was trying to use the is_countably_generated API, but the lemma I was trying to use for it needed uniform group.

Anatole Dedecker (Sep 01 2022 at 16:01):

I must admit that it was trickier than I expected, because neighborhoods in the quotient are not always the filter.map of neighborhoods in the original space. The thing that makes things work is really docs#quotient_group.is_open_map_coe

Anatole Dedecker (Sep 01 2022 at 16:02):

(deleted)

Jireh Loreaux (Sep 01 2022 at 16:05):

Yes, I saw that the fact that is was an open map was key too, but couldn't quite make it work. Also, fun fact, you only need to assume [first_countable_topology G] instead of [metrizable_space G] (for the same reason).

Anatole Dedecker (Sep 01 2022 at 16:07):

Oh yeah, I was following a lecture at the same time so I didn’t try too hard to minimize assumptions

Patrick Massot (Sep 01 2022 at 17:50):

Anatole Dedecker said:

Oh yeah, I was following a lecture at the same time so I didn’t try too hard to minimize assumptions

Don't you fear someone could tell your study program supervisor that you're playing video-games instead of focusing on lectures?

Anatole Dedecker (Sep 02 2022 at 09:47):

I know I know, but I just love filters and point-set topology way too much :grimacing:


Last updated: Dec 20 2023 at 11:08 UTC