quotient group is uniform

Stream: general

[Jireh Loreaux]

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]

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

[Patrick Massot]

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

[Jireh Loreaux]

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]

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]

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

[Jireh Loreaux]

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]

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]

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]

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]

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

[Oliver Nash]

Indeed Bourbaki seems not to. I could be wrong!

[Oliver Nash]

Hence only "suspect".

[Anatole Dedecker]

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]

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

[Anatole Dedecker]

Which we have! This is docs#uniform_space.metrizable_space

[Anatole Dedecker]

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]

Thanks Anatole!

[Jireh Loreaux]

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]

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]

(deleted)

[Jireh Loreaux]

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]

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

[Patrick Massot]

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]

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