Discrete subgroup of Hausdorff group is closed

Stream: Is there code for X?

[Oliver Nash]

I just wanted this result and discovered it seems to be missing:

import topology.algebra.group

-- TODO Bourbaki GT III § 2.2, Proposition 5 (page 227 of English translation).
@[to_additive] lemma subgroup.is_closed_of_discrete
  {G : Type*} [group G] [topological_space G] [topological_group G] [t2_space G]
  {H : subgroup G} (h : discrete_topology H) :
  is_closed (H : set G) :=
sorry

[Oliver Nash]

I won't have time to fill it in for at least a week so I thought I'd try see if I can tempt someone else to do it :-)

[Patrick Massot]

Indeed I don't think we have this..

[Anatole Dedecker]

What a nice timing, I’m taking a plane tomorrow so I was looking for something self-contained to do in the plane, and this looks perfect

[Patrick Massot]

Too late Anatole:

import topology.algebra.uniform_group

open_locale topological_space uniformity
open set filter

@[to_additive] lemma subgroup.is_closed_of_discrete
  {G : Type*} [group G] [topological_space G] [topological_group G] [t2_space G]
  {H : subgroup G} (h : discrete_topology H) :
  is_closed (H : set G) :=
begin
  obtain ⟨V, V_in, VH⟩ : ∃ V : set G, V ∈ 𝓝 (1 : G) ∧ V ∩ (H : set G) = {1},
  -- This should be a lemma about elements of a discrete set
  { have : ({1} : set H) ∈ 𝓝 (1 : H), -- Don't we have a lemma for this?
    { rw [mem_nhds_discrete],
      exact set.mem_singleton _},
    -- Now everything is obvious...
    rw [nhds_subtype, subgroup.coe_one, mem_comap] at this,
    rcases this with ⟨V, V_in, hV⟩,
    use [V, V_in],
    refine eq_singleton_iff_unique_mem.mpr ⟨⟨mem_of_mem_nhds V_in, H.one_mem⟩, _⟩,
    rintros y ⟨hy, hy'⟩,
    simp only [subset_singleton_iff, mem_preimage] at hV,
    have : (⟨y, hy'⟩ : H) = ⟨1, H.one_mem⟩ := hV ⟨y, hy'⟩ hy,
    simpa  },
  letI : uniform_space G := topological_group.to_uniform_space G,
  haveI : separated_space G := separated_iff_t2.mpr ‹_›,
  have : (λp:G×G, p.2 / p.1) ⁻¹' V ∈ 𝓤 G, from preimage_mem_comap V_in,
  apply is_closed_of_spaced_out this,
  intros h h_in h' h'_in,
  contrapose!,
  -- and now Lean should finish alone...
  rintro (hyp : h' / h ∈ V),
  have div_mem : h'/h ∈ (H : set G) := H.div_mem h'_in h_in,
  have : h'/h ∈ ({1} :set G) := VH ▸ set.mem_inter hyp div_mem,
  simp at this,
  symmetry,
  exact eq_of_div_eq_one this
end

There is a lot of remaining polishing to do (including either extracting lemmas or finding them in mathlib)

[Yaël Dillies]

Your have : ({1} : set H) ∈ 𝓝 (1 : H), -- Don't we have a lemma for this? would have better chances to exist were it written (1 : set H) ∈ 𝓝 (1 : H).

[Eric Rodriguez]

why would that be? it holds for all a

[Patrick Massot]

Yaël, this lemma has nothing to do with algebra.

[Yaël Dillies]

I doubt! I see groups in there.

[Adam Topaz]

this is true for any discrete space

[Adam Topaz]

E.g.

import topology.algebra.uniform_group

open_locale topological_space

lemma singleton_mem_nhds {X : Type*} [topological_space X]
  [discrete_topology X] (x : X) :
  {x} ∈ 𝓝 x :=
mem_nhds_discrete.mpr rfl

[Oliver Nash]

Marvellous; thank you all very much, especially Patrick!

[Oliver Nash]

@Patrick Massot Are you planning on PR -ing this?

[Oliver Nash]

I can do it if you prefer.

[Patrick Massot]

I'll try to find time for it (PRing takes a lot more time than forcing a proof as I did above)

[Oliver Nash]

Thanks!

[Patrick Massot]

I found docs#nhds_inter_eq_singleton_of_mem_discrete so it's actually easy

[Patrick Massot]

#16130