feat(topology/algebra/mul_action2): quotient by a properly discontinu…

…ous group action is t2 (#10465)

We prove that the quotient of a Hausdorff (t2) locally compact space by a properly discontinuous group action is itself Hausdorff.

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>



Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

src/group_theory/group_action/basic.lean

@@ -170,6 +170,51 @@ def orbit_rel : setoid β :=
   iseqv := ⟨mem_orbit_self, λ a b, by simp [orbit_eq_iff.symm, eq_comm],
     λ a b, by simp [orbit_eq_iff.symm, eq_comm] {contextual := tt}⟩ }
 
+local attribute [instance] orbit_rel
+
+variables {α} {β}
+/-- When you take a set `U` in `β`, push it down to the quotient, and pull back, you get the union
+of the orbit of `U` under `α`.
+-/
+@[to_additive] lemma quotient_preimage_image_eq_union_mul (U : set β) :
+  quotient.mk ⁻¹' (quotient.mk '' U) = ⋃ a : α, ((•) a) '' U :=
+begin
+  set f : β → quotient (mul_action.orbit_rel α β) := quotient.mk,
+  ext,
+  split,
+  { rintros ⟨y , hy, hxy⟩,
+    obtain ⟨a, rfl⟩ := quotient.exact hxy,
+    rw set.mem_Union,
+    exact ⟨a⁻¹, a • x, hy, inv_smul_smul a x⟩ },
+  { intros hx,
+    rw set.mem_Union at hx,
+    obtain ⟨a, u, hu₁, hu₂⟩ := hx,
+    rw [set.mem_preimage, set.mem_image_iff_bex],
+    refine ⟨a⁻¹ • x, _, by simp only [quotient.eq]; use a⁻¹⟩,
+    rw ← hu₂,
+    convert hu₁,
+    simp only [inv_smul_smul], },
+end
+
+@[to_additive]
+lemma image_inter_image_iff (U V : set β) :
+  (quotient.mk '' U) ∩ (quotient.mk '' V) = ∅ ↔ ∀ x ∈ U, ∀ a : α, a • x ∉ V :=
+begin
+  set f : β → quotient (mul_action.orbit_rel α β) := quotient.mk,
+  rw set.eq_empty_iff_forall_not_mem,
+  split,
+  { intros h x x_in_U a a_in_V,
+    refine h (f (a • x)) ⟨⟨x, x_in_U, _⟩, ⟨a • x, a_in_V, rfl⟩⟩,
+    rw quotient.eq,
+    use a⁻¹,
+    simp, },
+  { rintros h x ⟨⟨y, hy₁, hy₂⟩, ⟨z, hz₁, hz₂⟩⟩,
+    obtain ⟨a, ha⟩ := quotient.exact (hz₂.trans hy₂.symm),
+    apply h y hy₁ a,
+    convert hz₁, },
+end
+
+variables (α) (β)
 local notation `Ω` := (quotient $ orbit_rel α β)
 
 /-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.

src/topology/algebra/mul_action.lean

@@ -7,6 +7,7 @@ import topology.algebra.monoid
 import group_theory.group_action.prod
 import group_theory.group_action.basic
 import topology.homeomorph
+import topology.algebra.mul_action2
 
 /-!
 # Continuous monoid action
@@ -62,6 +63,10 @@ section has_scalar
 
 variables [has_scalar M α] [has_continuous_smul M α]
 
+@[priority 100, to_additive] instance has_continuous_smul.has_continuous_smul₂ :
+  has_continuous_smul₂ M α :=
+{ continuous_smul₂ := λ _, continuous_smul.comp (continuous_const.prod_mk continuous_id) }
+
 @[to_additive]
 lemma filter.tendsto.smul {f : β → M} {g : β → α} {l : filter β} {c : M} {a : α}
   (hf : tendsto f l (𝓝 c)) (hg : tendsto g l (𝓝 a)) :
@@ -184,23 +189,6 @@ lemma continuous_const_smul_iff (c : G) :
   continuous (λ x, c • f x) ↔ continuous f :=
 by simp only [continuous_iff_continuous_at, continuous_at_const_smul_iff]
 
-/-- Scalar multiplication by an element of a group `G` acting on `α` is a homeomorphism from `α`
-to itself. -/
-protected def homeomorph.smul (c : G) : α ≃ₜ α :=
-{ to_equiv := mul_action.to_perm_hom G α c,
-  continuous_to_fun  := continuous_id.const_smul _,
-  continuous_inv_fun := continuous_id.const_smul _ }
-
-/-- Affine-addition of an element of an additive group `G` acting on `α` is a homeomorphism
-from `α` to itself. -/
-protected def homeomorph.vadd {G : Type*} [topological_space G] [add_group G] [add_action G α]
-  [has_continuous_vadd G α] (c : G) : α ≃ₜ α :=
-{ to_equiv := add_action.to_perm_hom α G c,
-  continuous_to_fun  := continuous_id.const_vadd _,
-  continuous_inv_fun := continuous_id.const_vadd _ }
-
-attribute [to_additive] homeomorph.smul
-
 @[to_additive]
 lemma is_open_map_smul (c : G) : is_open_map (λ x : α, c • x) :=
 (homeomorph.smul c).is_open_map

src/topology/algebra/mul_action2.lean

@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2021 Alex Kontorovich, Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Kontorovich, Heather Macbeth
+-/
+import topology.homeomorph
+import group_theory.group_action.basic
+/-!
+# Monoid actions continuous in the second variable
+
+In this file we define class `has_continuous_smul₂`. We say `has_continuous_smul₂ Γ T` if `Γ` acts
+on `T` and for each `γ`, the map `x ↦ γ • x` is continuous. (This differs from
+`has_continuous_smul`, which requires simultaneous continuity in both variables.)
+
+## Main definitions
+
+* `has_continuous_smul₂ Γ T` : typeclass saying that the map `x ↦ γ • x` is continuous on `T`;
+* `properly_discontinuous_smul`: says that the scalar multiplication `(•) : Γ → T → T`
+  is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely
+  many `γ:Γ` move `K` to have nontrivial intersection with `L`.
+* `homeomorph.smul`: scalar multiplication by an element of a group `Γ` acting on `T`
+  is a homeomorphism of `T`.
+
+## Main results
+
+* `is_open_map_quotient_mk_mul` : The quotient map by a group action is open.
+* `t2_space_of_properly_discontinuous_smul_of_t2_space` : The quotient by a discontinuous group
+  action of a locally compact t2 space is t2.
+
+## Tags
+
+Hausdorff, discrete group, properly discontinuous, quotient space
+
+-/
+
+open_locale topological_space
+
+open filter set
+
+local attribute [instance] mul_action.orbit_rel
+
+/-- Class `has_continuous_smul₂ Γ T` says that the scalar multiplication `(•) : Γ → T → T`
+is continuous in the second argument. We use the same class for all kinds of multiplicative
+actions, including (semi)modules and algebras.
+-/
+class has_continuous_smul₂ (Γ : Type*) (T : Type*) [topological_space T] [has_scalar Γ T]
+ : Prop :=
+(continuous_smul₂ : ∀ γ : Γ, continuous (λ x : T, γ • x))
+
+/-- Class `has_continuous_vadd₂ Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
+is continuous in the second argument. We use the same class for all kinds of additive actions,
+including (semi)modules and algebras.
+-/
+class has_continuous_vadd₂ (Γ : Type*) (T : Type*) [topological_space T]
+  [has_vadd Γ T] : Prop :=
+(continuous_vadd₂ : ∀ γ : Γ, continuous (λ x : T, γ +ᵥ x))
+
+attribute [to_additive has_continuous_vadd₂] has_continuous_smul₂
+
+export has_continuous_smul₂ (continuous_smul₂)
+
+export has_continuous_vadd₂ (continuous_vadd₂)
+
+/-- Class `properly_discontinuous_smul Γ T` says that the scalar multiplication `(•) : Γ → T → T`
+is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely many
+`γ:Γ` move `K` to have nontrivial intersection with `L`.
+-/
+class properly_discontinuous_smul (Γ : Type*) (T : Type*) [topological_space T]
+  [has_scalar Γ T] : Prop :=
+(finite_disjoint_inter_image : ∀ {K L : set T}, is_compact K → is_compact L →
+  set.finite {γ : Γ | (((•) γ) '' K) ∩ L ≠ ∅ })
+
+/-- Class `properly_discontinuous_vadd Γ T` says that the additive action `(+ᵥ) : Γ → T → T`
+is properly discontinuous, that is, for any pair of compact sets `K, L` in `T`, only finitely many
+`γ:Γ` move `K` to have nontrivial intersection with `L`.
+-/
+class properly_discontinuous_vadd (Γ : Type*) (T : Type*) [topological_space T]
+  [has_vadd Γ T] : Prop :=
+(finite_disjoint_inter_image : ∀ {K L : set T}, is_compact K → is_compact L →
+  set.finite {γ : Γ | (((+ᵥ) γ) '' K) ∩ L ≠ ∅ })
+
+attribute [to_additive] properly_discontinuous_smul
+
+variables {Γ : Type*} [group Γ] {T : Type*} [topological_space T] [mul_action Γ T]
+
+/-- A finite group action is always properly discontinuous
+-/
+@[priority 100, to_additive] instance fintype.properly_discontinuous_smul [fintype Γ] :
+  properly_discontinuous_smul Γ T :=
+{ finite_disjoint_inter_image := λ _ _ _ _, set.finite.of_fintype _}
+
+export properly_discontinuous_smul (finite_disjoint_inter_image)
+
+export properly_discontinuous_vadd (finite_disjoint_inter_image)
+
+/-- The homeomorphism given by scalar multiplication by a given element of a group `Γ` acting on
+  `T` is a homeomorphism from `T` to itself. -/
+def homeomorph.smul {T : Type*} [topological_space T] {Γ : Type*} [group Γ]
+  [mul_action Γ T] [has_continuous_smul₂ Γ T] (γ : Γ) :
+  T ≃ₜ T :=
+{ to_equiv := mul_action.to_perm_hom Γ T γ,
+  continuous_to_fun  := continuous_smul₂ γ,
+  continuous_inv_fun := continuous_smul₂ γ⁻¹ }
+
+/-- The homeomorphism given by affine-addition by an element of an additive group `Γ` acting on
+  `T` is a homeomorphism from `T` to itself. -/
+def homeomorph.vadd {T : Type*} [topological_space T] {Γ : Type*} [add_group Γ]
+  [add_action Γ T] [has_continuous_vadd₂ Γ T] (γ : Γ) :
+  T ≃ₜ T :=
+{ to_equiv := add_action.to_perm_hom T Γ γ,
+  continuous_to_fun  := continuous_vadd₂ γ,
+  continuous_inv_fun := continuous_vadd₂ (-γ) }
+
+attribute [to_additive homeomorph.vadd] homeomorph.smul
+
+/-- The quotient map by a group action is open. -/
+@[to_additive]
+lemma is_open_map_quotient_mk_mul [has_continuous_smul₂ Γ T] :
+  is_open_map (quotient.mk : T → quotient (mul_action.orbit_rel Γ T)) :=
+begin
+  intros U hU,
+  rw [is_open_coinduced, mul_action.quotient_preimage_image_eq_union_mul U],
+  exact is_open_Union (λ γ, (homeomorph.smul γ).is_open_map U hU)
+end
+
+/-- The quotient by a discontinuous group action of a locally compact t2 space is t2. -/
+@[priority 100, to_additive] instance t2_space_of_properly_discontinuous_smul_of_t2_space
+  [t2_space T] [locally_compact_space T] [has_continuous_smul₂ Γ T]
+  [properly_discontinuous_smul Γ T] : t2_space (quotient (mul_action.orbit_rel Γ T)) :=
+begin
+  set Q := quotient (mul_action.orbit_rel Γ T),
+  rw t2_space_iff_nhds,
+  let f : T → Q := quotient.mk,
+  have f_op : is_open_map f := is_open_map_quotient_mk_mul,
+  rintros ⟨x₀⟩ ⟨y₀⟩ (hxy : f x₀ ≠ f y₀),
+  show ∃ (U ∈ 𝓝 (f x₀)) (V ∈ 𝓝 (f y₀)), U ∩ V = ∅,
+  have hx₀y₀ : x₀ ≠ y₀ := ne_of_apply_ne _ hxy,
+  have hγx₀y₀ : ∀ γ : Γ, γ • x₀ ≠ y₀ := not_exists.mp (mt quotient.sound hxy.symm : _),
+  obtain ⟨K₀, L₀, K₀_in, L₀_in, hK₀, hL₀, hK₀L₀⟩ := t2_separation_compact_nhds hx₀y₀,
+  let bad_Γ_set := {γ : Γ | (((•) γ) '' K₀) ∩ L₀ ≠ ∅ },
+  have bad_Γ_finite : bad_Γ_set.finite := finite_disjoint_inter_image hK₀ hL₀,
+  choose u v hu hv u_v_disjoint using λ γ, t2_separation_nhds (hγx₀y₀ γ),
+  let U₀₀ := ⋂ γ ∈ bad_Γ_set, ((•) γ) ⁻¹' (u γ),
+  let U₀ := U₀₀ ∩ K₀,
+  let V₀₀ := ⋂ γ ∈ bad_Γ_set, v γ,
+  let V₀ := V₀₀ ∩ L₀,
+  have U_nhds : f '' U₀ ∈ 𝓝 (f x₀),
+  { apply f_op.image_mem_nhds (inter_mem ((bInter_mem bad_Γ_finite).mpr $ λ γ hγ, _) K₀_in),
+    exact (has_continuous_smul₂.continuous_smul₂ γ).continuous_at (hu γ) },
+  have V_nhds : f '' V₀ ∈ 𝓝 (f y₀),
+    from f_op.image_mem_nhds (inter_mem ((bInter_mem bad_Γ_finite).mpr $ λ γ hγ, hv γ) L₀_in),
+  refine ⟨f '' U₀, U_nhds, f '' V₀, V_nhds, _⟩,
+  rw mul_action.image_inter_image_iff,
+  rintros x ⟨x_in_U₀₀, x_in_K₀⟩ γ,
+  by_cases H : γ ∈ bad_Γ_set,
+  { rintros ⟨h, -⟩,
+    exact eq_empty_iff_forall_not_mem.mp (u_v_disjoint γ) (γ • x)
+      ⟨(mem_Inter₂.mp x_in_U₀₀ γ H : _), mem_Inter₂.mp h γ H⟩ },
+  { rintros ⟨-, h'⟩,
+    simp only [image_smul, not_not, mem_set_of_eq, ne.def] at H,
+    exact eq_empty_iff_forall_not_mem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩ },
+end

src/topology/separation.lean

@@ -643,6 +643,39 @@ lemma t2_iff_nhds : t2_space α ↔ ∀ {x y : α}, ne_bot (𝓝 x ⊓ 𝓝 y) 
        ⟨v, vv', vo, hv⟩ := mem_nhds_iff.mp hv' in
    ⟨u, v, uo, vo, hu, hv, by { rw [← subset_empty_iff, u'v'], exact inter_subset_inter uu' vv' }⟩⟩⟩
 
+lemma t2_space_iff_nhds : t2_space α ↔ ∀ {x y : α}, x ≠ y → ∃ (U ∈ 𝓝 x) (V ∈ 𝓝 y), U ∩ V = ∅ :=
+begin
+  split,
+  { rintro ⟨h⟩ x y hxy,
+    rcases h x y hxy with ⟨u, v, u_op, v_op, hx, hy, H⟩,
+    exact ⟨u, u_op.mem_nhds hx, v, v_op.mem_nhds hy, H⟩ },
+  { refine λ h, ⟨λ x y hxy, _⟩,
+    rcases h hxy with ⟨u, u_in, v, v_in, H⟩,
+    rcases mem_nhds_iff.mp u_in with ⟨U, hUu, U_op, hxU⟩,
+    rcases mem_nhds_iff.mp v_in with ⟨V, hVv, V_op, hyV⟩,
+    refine ⟨U, V, U_op, V_op, hxU, hyV, set.eq_empty_of_subset_empty _⟩,
+    rw ← H,
+    exact set.inter_subset_inter hUu hVv }
+end
+
+lemma t2_separation_nhds [t2_space α] {x y : α} (h : x ≠ y) :
+   ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ u ∩ v = ∅ :=
+let ⟨u, v, open_u, open_v, x_in, y_in, huv⟩ := t2_separation h in
+⟨u, v, open_u.mem_nhds x_in, open_v.mem_nhds y_in, huv⟩
+
+lemma t2_separation_compact_nhds [locally_compact_space α]
+  [t2_space α] {x y : α} (h : x ≠ y) :
+  ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ is_compact u ∧ is_compact v ∧ u ∩ v = ∅ :=
+begin
+  obtain ⟨u₀, v₀, u₀_in, v₀_in, hu₀v₀⟩ := t2_separation_nhds h,
+  obtain ⟨K₀, K₀_in, K₀_u₀, hK₀⟩ := local_compact_nhds u₀_in,
+  obtain ⟨L₀, L₀_in, L₀_u₀, hL₀⟩ := local_compact_nhds v₀_in,
+  use [K₀, L₀, K₀_in, L₀_in, hK₀, hL₀],
+  apply set.eq_empty_of_subset_empty,
+  rw ← hu₀v₀,
+  exact set.inter_subset_inter K₀_u₀ L₀_u₀
+end
+
 lemma t2_iff_ultrafilter :
   t2_space α ↔ ∀ {x y : α} (f : ultrafilter α), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y :=
 t2_iff_nhds.trans $ by simp only [←exists_ultrafilter_iff, and_imp, le_inf_iff, exists_imp_distrib]

src/topology/subset_properties.lean

@@ -936,6 +936,10 @@ lemma compact_basis_nhds [locally_compact_space α] (x : α) :
   (𝓝 x).has_basis (λ s, s ∈ 𝓝 x ∧ is_compact s) (λ s, s) :=
 has_basis_self.2 $ by simpa only [and_comm] using locally_compact_space.local_compact_nhds x
 
+lemma local_compact_nhds [locally_compact_space α] {x : α} {n : set α} (h : n ∈ 𝓝 x) :
+  ∃ s ∈ 𝓝 x, s ⊆ n ∧ is_compact s :=
+locally_compact_space.local_compact_nhds _ _ h
+
 lemma locally_compact_space_of_has_basis {ι : α → Type*} {p : Π x, ι x → Prop}
   {s : Π x, ι x → set α} (h : ∀ x, (𝓝 x).has_basis (p x) (s x))
   (hc : ∀ x i, p x i → is_compact (s x i)) :