feat(topology/algebra/group): quotient of a second countable group (#…

…16738)

Quotient of a second countable group is second countable 

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



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

src/topology/algebra/const_mul_action.lean

@@ -7,6 +7,7 @@ import data.real.nnreal
 import topology.algebra.constructions
 import topology.homeomorph
 import group_theory.group_action.basic
+import topology.bases
 /-!
 # Monoid actions continuous in the second variable
 
@@ -37,7 +38,7 @@ Hausdorff, discrete group, properly discontinuous, quotient space
 
 open_locale topological_space pointwise
 
-open filter set
+open filter set topological_space
 
 local attribute [instance] mul_action.orbit_rel
 
@@ -353,8 +354,10 @@ export properly_discontinuous_smul (finite_disjoint_inter_image)
 
 export properly_discontinuous_vadd (finite_disjoint_inter_image)
 
-/-- The quotient map by a group action is open. -/
-@[to_additive "The quotient map by a group action is open."]
+/-- The quotient map by a group action is open, i.e. the quotient by a group action is an open
+  quotient. -/
+@[to_additive "The quotient map by a group action is open, i.e. the quotient by a group 
+action is an open quotient. "]
 lemma is_open_map_quotient_mk_mul [has_continuous_const_smul Γ T] :
   is_open_map (quotient.mk : T → quotient (mul_action.orbit_rel Γ T)) :=
 begin
@@ -400,6 +403,14 @@ begin
     exact eq_empty_iff_forall_not_mem.mp H (γ • x) ⟨mem_image_of_mem _ x_in_K₀, h'⟩ },
 end
 
+/-- The quotient of a second countable space by a group action is second countable. -/
+@[to_additive "The quotient of a second countable space by an additive group action is second
+countable."]
+theorem has_continuous_const_smul.second_countable_topology [second_countable_topology T]
+  [has_continuous_const_smul Γ T] :
+  second_countable_topology (quotient (mul_action.orbit_rel Γ T)) :=
+topological_space.quotient.second_countable_topology is_open_map_quotient_mk_mul
+
 section nhds
 
 section mul_action

src/topology/algebra/group.lean

@@ -1210,6 +1210,13 @@ instance quotient_group.has_continuous_smul [locally_compact_space G] :
     exact quotient_map.continuous_lift_prod_right quotient_map_quotient_mk H,
   end }
 
+/-- The quotient of a second countable topological group by a subgroup is second countable. -/
+@[to_additive "The quotient of a second countable additive topological group by a subgroup is second
+countable."]
+instance quotient_group.second_countable_topology [second_countable_topology G] :
+  second_countable_topology (G ⧸ Γ) :=
+has_continuous_const_smul.second_countable_topology
+
 end quotient
 
 namespace units

src/topology/algebra/monoid.lean

@@ -456,7 +456,10 @@ instance is_scalar_tower.has_continuous_const_smul {R A : Type*} [monoid A] [has
 implies continuous scalar multiplication by constants.
 
 Notably, this instances applies when `R = Aᵐᵒᵖ` -/
-@[priority 100]
+@[priority 100, to_additive "If the action of `R` on `A` commutes with left-addition, then
+continuous addition implies continuous affine addition by constants.
+
+Notably, this instances applies when `R = Aᵃᵒᵖ`. "]
 instance smul_comm_class.has_continuous_const_smul {R A : Type*} [monoid A] [has_smul R A]
   [smul_comm_class R A A] [topological_space A] [has_continuous_mul A] :
   has_continuous_const_smul R A :=

src/topology/bases.lean

@@ -809,6 +809,56 @@ end
 
 end sum
 
+section quotient
+
+variables {X : Type*} [topological_space X] {Y : Type*} [topological_space Y] {π : X → Y}
+omit t
+
+/-- The image of a topological basis under an open quotient map is a topological basis. -/
+lemma is_topological_basis.quotient_map {V : set (set X)} (hV : is_topological_basis V)
+  (h' : quotient_map π) (h : is_open_map π) :
+  is_topological_basis (set.image π '' V) :=
+begin
+  apply is_topological_basis_of_open_of_nhds,
+  { rintros - ⟨U, U_in_V, rfl⟩,
+    apply h U (hV.is_open U_in_V), },
+  { intros y U y_in_U U_open,
+    obtain ⟨x, rfl⟩ := h'.surjective y,
+    let W := π ⁻¹' U,
+    have x_in_W : x ∈ W := y_in_U,
+    have W_open : is_open W := U_open.preimage h'.continuous,
+    obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open,
+    have πZ_in_U : π '' Z ⊆ U := (set.image_subset _ Z_in_W).trans (image_preimage_subset π U),
+    exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, πZ_in_U⟩, },
+end
+
+/-- A second countable space is mapped by an open quotient map to a second countable space. -/
+lemma quotient_map.second_countable_topology [second_countable_topology X] (h' : quotient_map π)
+  (h : is_open_map π) :
+  second_countable_topology Y :=
+{ is_open_generated_countable :=
+  begin
+    obtain ⟨V, V_countable, V_no_empty, V_generates⟩ := exists_countable_basis X,
+    exact ⟨set.image π '' V, V_countable.image (set.image π),
+      (V_generates.quotient_map h' h).eq_generate_from⟩,
+  end }
+
+variables {S : setoid X}
+
+/-- The image of a topological basis "downstairs" in an open quotient is a topological basis. -/
+lemma is_topological_basis.quotient {V : set (set X)}
+  (hV : is_topological_basis V) (h : is_open_map (quotient.mk : X → quotient S)) :
+  is_topological_basis (set.image (quotient.mk : X → quotient S) '' V) :=
+hV.quotient_map quotient_map_quotient_mk h
+
+/-- An open quotient of a second countable space is second countable. -/
+lemma quotient.second_countable_topology [second_countable_topology X]
+  (h : is_open_map (quotient.mk : X → quotient S)) :
+  second_countable_topology (quotient S) :=
+quotient_map_quotient_mk.second_countable_topology h
+
+end quotient
+
 end topological_space
 
 open topological_space