chore(topology/algebra): cleanup (#15301)

* Drop instances about `sub*.topological_closure`. Normal `sub*` instances apply.
* Add `units.inducing_embed_product` and `units.embedding_embed_product`.
* Add `inducing.has_continuous_mul`, `inducing.has_continuous_inv`, and `inducing.topological_group`.
* Use new lemmas to golf some instances.
* Don't use `section .. variables` for assumptions that are used only once.
* Reuse `topological_group_inf`, `topological_group_Inf` in `group_topology.has_inf`, `group_topology.has_Inf`.

Author: urkud

src/topology/algebra/algebra.lean

@@ -55,8 +55,14 @@ end topological_algebra
 section topological_algebra
 variables {R : Type*} [comm_semiring R]
 variables {A : Type u} [topological_space A]
-variables [semiring A]
-variables [algebra R A] [topological_semiring A]
+variables [semiring A] [algebra R A]
+
+instance subalgebra.has_continuous_smul [topological_space R] [has_continuous_smul R A]
+  (s : subalgebra R A) :
+  has_continuous_smul R s :=
+s.to_submodule.has_continuous_smul
+
+variables [topological_semiring A]
 
 /-- The closure of a subalgebra in a topological algebra as a subalgebra. -/
 def subalgebra.topological_closure (s : subalgebra R A) : subalgebra R A :=
@@ -68,14 +74,8 @@ def subalgebra.topological_closure (s : subalgebra R A) : subalgebra R A :=
   (s.topological_closure : set A) = closure (s : set A) :=
 rfl
 
-instance subalgebra.topological_closure_topological_semiring (s : subalgebra R A) :
-  topological_semiring (s.topological_closure) :=
-s.to_subsemiring.topological_closure_topological_semiring
-
-instance subalgebra.topological_closure_topological_algebra
-  [topological_space R] [has_continuous_smul R A] (s : subalgebra R A) :
-  has_continuous_smul R (s.topological_closure) :=
-s.to_submodule.topological_closure_has_continuous_smul
+instance subalgebra.topological_semiring (s : subalgebra R A) : topological_semiring s :=
+s.to_subsemiring.topological_semiring
 
 lemma subalgebra.subalgebra_topological_closure (s : subalgebra R A) :
   s ≤ s.topological_closure :=

src/topology/algebra/constructions.lean

@@ -70,6 +70,11 @@ variables [topological_space M] [monoid M]
 @[to_additive] instance : topological_space Mˣ :=
 topological_space.induced (embed_product M) prod.topological_space
 
+@[to_additive] lemma inducing_embed_product : inducing (embed_product M) := ⟨rfl⟩
+
+@[to_additive] lemma embedding_embed_product : embedding (embed_product M) :=
+⟨inducing_embed_product, embed_product_injective M⟩
+
 @[to_additive] lemma continuous_embed_product : continuous (embed_product M) :=
 continuous_induced_dom
 

src/topology/algebra/group.lean

@@ -197,14 +197,14 @@ hf.inv
 
 @[to_additive]
 instance [topological_space H] [has_inv H] [has_continuous_inv H] : has_continuous_inv (G × H) :=
-⟨(continuous_inv.comp continuous_fst).prod_mk (continuous_inv.comp continuous_snd)⟩
+⟨continuous_inv.fst'.prod_mk continuous_inv.snd'⟩
 
 variable {ι : Type*}
 
 @[to_additive]
 instance pi.has_continuous_inv {C : ι → Type*} [∀ i, topological_space (C i)]
   [∀ i, has_inv (C i)] [∀ i, has_continuous_inv (C i)] : has_continuous_inv (Π i, C i) :=
-{ continuous_inv := continuous_pi (λ i, continuous.inv (continuous_apply i)) }
+{ continuous_inv := continuous_pi (λ i, (continuous_apply i).inv) }
 
 /-- A version of `pi.has_continuous_inv` for non-dependent functions. It is needed because sometimes
 Lean fails to use `pi.has_continuous_inv` for non-dependent functions. -/
@@ -274,34 +274,31 @@ end continuous_involutive_inv
 
 section lattice_ops
 
-variables {ι' : Sort*} [has_inv G] [has_inv H] {ts : set (topological_space G)}
-  (h : Π t ∈ ts, @has_continuous_inv G t _) {ts' : ι' → topological_space G}
-  (h' : Π i, @has_continuous_inv G (ts' i) _) {t₁ t₂ : topological_space G}
-  (h₁ : @has_continuous_inv G t₁ _) (h₂ : @has_continuous_inv G t₂ _)
-  {t : topological_space H} [has_continuous_inv H]
-
+variables {ι' : Sort*} [has_inv G]
 
-@[to_additive] lemma has_continuous_inv_Inf :
+@[to_additive] lemma has_continuous_inv_Inf {ts : set (topological_space G)}
+  (h : Π t ∈ ts, @has_continuous_inv G t _) :
   @has_continuous_inv G (Inf ts) _ :=
 { continuous_inv := continuous_Inf_rng (λ t ht, continuous_Inf_dom ht
   (@has_continuous_inv.continuous_inv G t _ (h t ht))) }
 
-include h'
-
-@[to_additive] lemma has_continuous_inv_infi :
+@[to_additive] lemma has_continuous_inv_infi {ts' : ι' → topological_space G}
+  (h' : Π i, @has_continuous_inv G (ts' i) _) :
   @has_continuous_inv G (⨅ i, ts' i) _ :=
 by {rw ← Inf_range, exact has_continuous_inv_Inf (set.forall_range_iff.mpr h')}
 
-omit h'
-
-include h₁ h₂
-
-@[to_additive] lemma has_continuous_inv_inf :
+@[to_additive] lemma has_continuous_inv_inf {t₁ t₂ : topological_space G}
+  (h₁ : @has_continuous_inv G t₁ _) (h₂ : @has_continuous_inv G t₂ _) :
   @has_continuous_inv G (t₁ ⊓ t₂) _ :=
-by {rw inf_eq_infi, refine has_continuous_inv_infi (λ b, _), cases b; assumption}
+by { rw inf_eq_infi, refine has_continuous_inv_infi (λ b, _), cases b; assumption }
 
 end lattice_ops
 
+@[to_additive] lemma inducing.has_continuous_inv {G H : Type*} [has_inv G] [has_inv H]
+  [topological_space G] [topological_space H] [has_continuous_inv H] {f : G → H} (hf : inducing f)
+  (hf_inv : ∀ x, f x⁻¹ = (f x)⁻¹) : has_continuous_inv G :=
+⟨hf.continuous_iff.2 $ by simpa only [(∘), hf_inv] using hf.continuous.inv⟩
+
 section topological_group
 
 /-!
@@ -465,7 +462,7 @@ open mul_opposite
 
 @[to_additive]
 instance [group α] [has_continuous_inv α] : has_continuous_inv αᵐᵒᵖ :=
-{ continuous_inv := continuous_induced_rng $ (@continuous_inv α _ _ _).comp continuous_unop }
+op_homeomorph.symm.inducing.has_continuous_inv unop_inv
 
 /-- If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`. -/
 @[to_additive "If addition is continuous in `α`, then it also is in `αᵃᵒᵖ`."]
@@ -498,16 +495,21 @@ rfl
 
 variables {G}
 
+@[to_additive] protected lemma inducing.topological_group {F : Type*} [group H]
+  [topological_space H] [monoid_hom_class F H G] (f : F) (hf : inducing f) :
+  topological_group H :=
+{ to_has_continuous_mul := hf.has_continuous_mul _,
+  to_has_continuous_inv := hf.has_continuous_inv (map_inv f) }
+
+@[to_additive] protected lemma topological_group_induced {F : Type*} [group H]
+  [monoid_hom_class F H G] (f : F) :
+  @topological_group H (induced f ‹_›) _ :=
+by { letI := induced f ‹_›, exact inducing.topological_group f ⟨rfl⟩  }
+
 namespace subgroup
 
-@[to_additive] instance (S : subgroup G) :
-  topological_group S :=
-{ continuous_inv :=
-  begin
-    rw embedding_subtype_coe.to_inducing.continuous_iff,
-    exact continuous_subtype_coe.inv
-  end,
-  ..S.to_submonoid.has_continuous_mul }
+@[to_additive] instance (S : subgroup G) : topological_group S :=
+inducing.topological_group S.subtype inducing_coe
 
 end subgroup
 
@@ -524,17 +526,6 @@ def subgroup.topological_closure (s : subgroup G) : subgroup G :=
   (s.topological_closure : set G) = closure s :=
 rfl
 
-@[to_additive]
-instance subgroup.topological_closure_topological_group (s : subgroup G) :
-  topological_group (s.topological_closure) :=
-{ continuous_inv :=
-  begin
-    apply continuous_induced_rng,
-    change continuous (λ p : s.topological_closure, (p : G)⁻¹),
-    continuity,
-  end
-  ..s.to_submonoid.topological_closure_has_continuous_mul}
-
 @[to_additive] lemma subgroup.subgroup_topological_closure (s : subgroup G) :
   s ≤ s.topological_closure :=
 subset_closure
@@ -1226,14 +1217,12 @@ end units
 
 section lattice_ops
 
-variables {ι : Sort*} [group G] [group H] {ts : set (topological_space G)}
-  (h : ∀ t ∈ ts, @topological_group G t _) {ts' : ι → topological_space G}
-  (h' : ∀ i, @topological_group G (ts' i) _) {t₁ t₂ : topological_space G}
-  (h₁ : @topological_group G t₁ _) (h₂ : @topological_group G t₂ _)
+variables {ι : Sort*} [group G] [group H]
   {t : topological_space H} [topological_group H] {F : Type*}
   [monoid_hom_class F G H] (f : F)
 
-@[to_additive] lemma topological_group_Inf :
+@[to_additive] lemma topological_group_Inf {ts : set (topological_space G)}
+  (h : ∀ t ∈ ts, @topological_group G t _) :
   @topological_group G (Inf ts) _ :=
 { continuous_inv := @has_continuous_inv.continuous_inv G (Inf ts) _
     (@has_continuous_inv_Inf _ _ _
@@ -1242,38 +1231,21 @@ variables {ι : Sort*} [group G] [group H] {ts : set (topological_space G)}
     (@has_continuous_mul_Inf _ _ _
       (λ t ht, @topological_group.to_has_continuous_mul G t _ (h t ht))) }
 
-include h'
-
-@[to_additive] lemma topological_group_infi :
+@[to_additive] lemma topological_group_infi {ts' : ι → topological_space G}
+  (h' : ∀ i, @topological_group G (ts' i) _) :
   @topological_group G (⨅ i, ts' i) _ :=
 by {rw ← Inf_range, exact topological_group_Inf (set.forall_range_iff.mpr h')}
 
-omit h'
-
-include h₁ h₂
-
-@[to_additive] lemma topological_group_inf :
+@[to_additive] lemma topological_group_inf {t₁ t₂ : topological_space G}
+  (h₁ : @topological_group G t₁ _) (h₂ : @topological_group G t₂ _) :
   @topological_group G (t₁ ⊓ t₂) _ :=
 by {rw inf_eq_infi, refine topological_group_infi (λ b, _), cases b; assumption}
 
-omit h₁ h₂
-
-@[to_additive] lemma topological_group_induced :
-  @topological_group G (t.induced f) _ :=
-{ continuous_inv :=
-    begin
-      letI : topological_space G := t.induced f,
-      refine continuous_induced_rng _,
-      simp_rw [function.comp, map_inv],
-      exact continuous_inv.comp (continuous_induced_dom : continuous f)
-    end,
-  continuous_mul := @has_continuous_mul.continuous_mul G (t.induced f) _
-    (@has_continuous_mul_induced G H _ _ t _ _ _ f) }
-
 end lattice_ops
 
 /-!
 ### Lattice of group topologies
+
 We define a type class `group_topology α` which endows a group `α` with a topology such that all
 group operations are continuous.
 
@@ -1366,12 +1338,7 @@ instance : bounded_order (group_topology α) :=
 
 @[to_additive]
 instance : has_inf (group_topology α) :=
-{ inf := λ x y,
-  { to_topological_space := x.to_topological_space ⊓ y.to_topological_space,
-    continuous_mul := continuous_inf_rng
-      (continuous_inf_dom_left₂ x.continuous_mul') (continuous_inf_dom_right₂ y.continuous_mul'),
-    continuous_inv := continuous_inf_rng
-      (continuous_inf_dom_left x.continuous_inv') (continuous_inf_dom_right y.continuous_inv') } }
+{ inf := λ x y, ⟨x.1 ⊓ y.1, topological_group_inf x.2 y.2⟩ }
 
 @[simp, to_additive]
 lemma to_topological_space_inf (x y : group_topology α) :
@@ -1388,17 +1355,7 @@ local notation `cont` := @continuous _ _
 @[to_additive "Infimum of a collection of additive group topologies"]
 instance : has_Inf (group_topology α) :=
 { Inf := λ S,
-  { to_topological_space := Inf (to_topological_space '' S),
-    continuous_mul       := continuous_Inf_rng begin
-      rintros _ ⟨⟨t, tr⟩, haS, rfl⟩, resetI,
-      exact continuous_Inf_dom₂
-        (set.mem_image_of_mem to_topological_space haS)
-        (set.mem_image_of_mem to_topological_space haS) continuous_mul,
-    end,
-    continuous_inv       := continuous_Inf_rng begin
-      rintros _ ⟨⟨t, tr⟩, haS, rfl⟩, resetI,
-      exact continuous_Inf_dom (set.mem_image_of_mem to_topological_space haS) continuous_inv,
-    end, } }
+  ⟨Inf (to_topological_space '' S), topological_group_Inf $ ball_image_iff.2 $ λ t ht, t.2⟩ }
 
 @[simp, to_additive]
 lemma to_topological_space_Inf (s : set (group_topology α)) :

src/topology/algebra/module/basic.lean

@@ -208,16 +208,6 @@ def submodule.topological_closure (s : submodule R M) : submodule R M :=
   (s.topological_closure : set M) = closure (s : set M) :=
 rfl
 
-instance submodule.topological_closure_has_continuous_smul (s : submodule R M) :
-  has_continuous_smul R (s.topological_closure) :=
-{ continuous_smul :=
-  begin
-    apply continuous_induced_rng,
-    change continuous (λ p : R × s.topological_closure, p.1 • (p.2 : M)),
-    continuity,
-  end,
-  ..s.to_add_submonoid.topological_closure_has_continuous_add }
-
 lemma submodule.submodule_topological_closure (s : submodule R M) :
   s ≤ s.topological_closure :=
 subset_closure