chore(topology/algebra/group): move a lemma to group_theory/coset (#…

…4522)

`quotient_group_saturate` didn't use any topology. Move it to
`group_theory/coset` and rename to
`quotient_group.preimage_image_coe`.

Also rename `quotient_group.open_coe` to `quotient_group.is_open_map_coe`

src/group_theory/coset.lean

@@ -214,6 +214,16 @@ lemma eq_class_eq_left_coset (s : subgroup α) (g : α) :
   {x : α | (x : quotient s) = g} = left_coset g s :=
 set.ext $ λ z, by { rw [mem_left_coset_iff, set.mem_set_of_eq, eq_comm, quotient_group.eq], simp }
 
+@[to_additive]
+lemma preimage_image_coe (N : subgroup α) (s : set α) :
+  coe ⁻¹' ((coe : α → quotient N) '' s) = ⋃ x : N, (λ y : α, y * x) '' s :=
+begin
+  ext x,
+  simp only [quotient_group.eq, subgroup.exists, exists_prop, set.mem_preimage, set.mem_Union,
+    set.mem_image, subgroup.coe_mk, ← eq_inv_mul_iff_mul_eq],
+  exact ⟨λ ⟨y, hs, hN⟩, ⟨_, hN, y, hs, rfl⟩, λ ⟨z, hN, y, hs, hyz⟩, ⟨y, hs, hyz ▸ hN⟩⟩
+end
+
 end quotient_group
 
 namespace subgroup

src/group_theory/quotient_group.lean

@@ -63,23 +63,23 @@ instance {G : Type*} [comm_group G] (N : subgroup G) : comm_group (quotient N) :
 
 include nN
 
+local notation ` Q ` := quotient N
+
 @[simp, to_additive quotient_add_group.coe_zero]
-lemma coe_one : ((1 : G) : quotient N) = 1 := rfl
+lemma coe_one : ((1 : G) : Q) = 1 := rfl
 
 @[simp, to_additive quotient_add_group.coe_add]
-lemma coe_mul (a b : G) : ((a * b : G) : quotient N) = a * b := rfl
+lemma coe_mul (a b : G) : ((a * b : G) : Q) = a * b := rfl
 
 @[simp, to_additive quotient_add_group.coe_neg]
-lemma coe_inv (a : G) : ((a⁻¹ : G) : quotient N) = a⁻¹ := rfl
+lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl
 
-@[simp] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : quotient N) = a ^ n :=
+@[simp] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n :=
 (mk' N).map_pow a n
 
-@[simp] lemma coe_gpow (a : G) (n : ℤ) : ((a ^ n : G) : quotient N) = a ^ n :=
+@[simp] lemma coe_gpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n :=
 (mk' N).map_gpow a n
 
-local notation ` Q ` := quotient N
-
 /-- A group homomorphism `φ : G →* H` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
 group homomorphism `G/N →* H`. -/
 @[to_additive quotient_add_group.lift "An `add_group` homomorphism `φ : G →+ H` with `N ⊆ ker(φ)`

src/topology/algebra/group.lean

@@ -198,30 +198,17 @@ variables [topological_space G] [group G] [topological_group G] (N : subgroup G)
 @[to_additive]
 instance {G : Type u} [group G] [topological_space G] (N : subgroup G) :
   topological_space (quotient_group.quotient N) :=
-by dunfold quotient_group.quotient; apply_instance
+quotient.topological_space
 
 open quotient_group
-@[to_additive]
-lemma quotient_group_saturate {G : Type u} [group G] (N : subgroup G) (s : set G) :
-  (coe : G → quotient N) ⁻¹' ((coe : G → quotient N) '' s) = (⋃ x : N, (λ y, y*x.1) '' s) :=
-begin
-  ext x,
-  simp only [mem_preimage, mem_image, mem_Union, quotient_group.eq],
-  split,
-  { exact assume ⟨a, a_in, h⟩, ⟨⟨_, h⟩, a, a_in, mul_inv_cancel_left _ _⟩ },
-  { exact assume ⟨⟨i, hi⟩, a, ha, eq⟩,
-      ⟨a, ha, by { simp only [eq.symm, (mul_assoc _ _ _).symm, inv_mul_cancel_left], exact hi }⟩ }
-end
 
 @[to_additive]
-lemma quotient_group.open_coe : is_open_map (coe : G →  quotient N) :=
+lemma quotient_group.is_open_map_coe : is_open_map (coe : G →  quotient N) :=
 begin
   intros s s_op,
   change is_open ((coe : G →  quotient N) ⁻¹' (coe '' s)),
-  rw quotient_group_saturate N s,
-  apply is_open_Union,
-  rintro ⟨n, _⟩,
-  exact is_open_map_mul_right n s s_op
+  rw quotient_group.preimage_image_coe N s,
+  exact is_open_Union (λ n, is_open_map_mul_right n s s_op)
 end
 
 @[to_additive]
@@ -231,11 +218,9 @@ instance topological_group_quotient (n : N.normal) : topological_group (quotient
       continuous_quot_mk.comp continuous_mul,
     have quot : quotient_map (λ p : G × G, ((p.1:quotient N), (p.2:quotient N))),
     { apply is_open_map.to_quotient_map,
-      { exact is_open_map.prod (quotient_group.open_coe N) (quotient_group.open_coe N) },
-      { exact (continuous_quot_mk.comp continuous_fst).prod_mk
-              (continuous_quot_mk.comp continuous_snd) },
-      { rintro ⟨⟨x⟩, ⟨y⟩⟩,
-        exact ⟨(x, y), rfl⟩ } },
+      { exact (quotient_group.is_open_map_coe N).prod (quotient_group.is_open_map_coe N) },
+      { exact continuous_quot_mk.prod_map continuous_quot_mk },
+      { exact (surjective_quot_mk _).prod_map (surjective_quot_mk _) } },
     exact (quotient_map.continuous_iff quot).2 cont,
   end,
   continuous_inv := begin