refactor(topology/algebra/field): drop topological_space_units (#18536

)

See [Zulip chat](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/topology.20on.20units/near/324188800)

Also generalize TC assumptions in `inv_mem_iff`.

src/group_theory/subgroup/basic.lean

@@ -116,6 +116,11 @@ class add_subgroup_class (S G : Type*) [sub_neg_monoid G] [set_like S G]
 
 attribute [to_additive] inv_mem_class subgroup_class
 
+@[simp, to_additive]
+theorem inv_mem_iff {S G} [has_involutive_inv G] [set_like S G] [inv_mem_class S G] {H : S}
+  {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
+⟨λ h, inv_inv x ▸ inv_mem h, inv_mem⟩
+
 variables {M S : Type*} [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M] {H K : S}
 include hSM
 
@@ -133,9 +138,6 @@ omit hSM
 variables [set_like S G] [hSG : subgroup_class S G]
 include hSG
 
-@[simp, to_additive] theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
-⟨λ h, inv_inv x ▸ inv_mem h, inv_mem⟩
-
 @[to_additive] lemma div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
 by rw [← inv_mem_iff, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, inv_inv]
 

src/group_theory/subgroup/pointwise.lean

@@ -30,11 +30,14 @@ Where possible, try to keep them in sync.
 open set
 open_locale pointwise
 
-variables {α G A S : Type*} [group G] [add_group A] {s : set G}
+variables {α G A S : Type*}
 
 @[simp, to_additive]
-lemma inv_coe_set [set_like S G] [subgroup_class S G] {H : S} : (H : set G)⁻¹ = H :=
-by { ext, simp }
+lemma inv_coe_set [has_involutive_inv G] [set_like S G] [inv_mem_class S G] {H : S} :
+  (H : set G)⁻¹ = H :=
+set.ext $ λ _, inv_mem_iff
+
+variables [group G] [add_group A] {s : set G}
 
 namespace subgroup
 

src/topology/algebra/constructions.lean

@@ -81,6 +81,26 @@ instance : topological_space Mˣ := prod.topological_space.induced (embed_produc
 @[to_additive] lemma embedding_embed_product : embedding (embed_product M) :=
 ⟨inducing_embed_product, embed_product_injective M⟩
 
+@[to_additive] lemma topology_eq_inf :
+  units.topological_space = topological_space.induced (coe : Mˣ → M) ‹_› ⊓
+    topological_space.induced (λ u, ↑u⁻¹ : Mˣ → M) ‹_› :=
+by simp only [inducing_embed_product.1, prod.topological_space, induced_inf,
+  mul_opposite.topological_space, induced_compose]; refl
+
+/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
+Use `units.coe_embedding₀`, `units.coe_embedding`, or `to_units_homeomorph` instead. -/
+@[to_additive "An auxiliary lemma that can be used to prove that coercion `add_units M → M` is a
+topological embedding. Use `add_units.coe_embedding` or `to_add_units_homeomorph` instead."]
+lemma embedding_coe_mk {M : Type*} [division_monoid M] [topological_space M]
+  (h : continuous_on has_inv.inv {x : M | is_unit x}) : embedding (coe : Mˣ → M) :=
+begin
+  refine ⟨⟨_⟩, ext⟩,
+  rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced, continuous_iff_continuous_at],
+  intros u s hs,
+  simp only [coe_inv, nhds_induced, filter.mem_map] at hs ⊢,
+  exact ⟨_, mem_inf_principal.1 (h u u.is_unit hs), λ u' hu', hu' u'.is_unit⟩
+end
+
 @[to_additive] lemma continuous_embed_product : continuous (embed_product M) :=
 continuous_induced_dom
 

src/topology/algebra/field.lean

@@ -17,54 +17,6 @@ non-zero element.
 -/
 
 
-namespace topological_ring
-open topological_space function
-variables (R : Type*) [semiring R]
-
-variables  [topological_space R]
-
-/-- The induced topology on units of a topological semiring.
-This is not a global instance since other topologies could be relevant. Instead there is a class
-`induced_units` asserting that something equivalent to this construction holds. -/
-def topological_space_units : topological_space Rˣ := induced (coe : Rˣ → R) ‹_›
-
-/-- Asserts the topology on units is the induced topology.
-
- Note: this is not always the correct topology.
- Another good candidate is the subspace topology of $R \times R$,
- with the units embedded via $u \mapsto (u, u^{-1})$.
- These topologies are not (propositionally) equal in general. -/
-class induced_units [t : topological_space $ Rˣ] : Prop :=
-(top_eq : t = induced (coe : Rˣ → R) ‹_›)
-
-variables [topological_space $ Rˣ]
-
-lemma units_topology_eq [induced_units R] :
-  ‹topological_space Rˣ› = induced (coe : Rˣ → R) ‹_› :=
-induced_units.top_eq
-
-lemma induced_units.continuous_coe [induced_units R] : continuous (coe : Rˣ → R) :=
-(units_topology_eq R).symm ▸ continuous_induced_dom
-
-lemma units_embedding [induced_units R] :
-  embedding (coe : Rˣ → R) :=
-{ induced := units_topology_eq R,
-  inj := λ x y h, units.ext h }
-
-instance top_monoid_units [topological_semiring R] [induced_units R] :
-  has_continuous_mul Rˣ :=
-⟨begin
-  let mulR := (λ (p : R × R), p.1*p.2),
-  let mulRx := (λ (p : Rˣ × Rˣ), p.1*p.2),
-  have key : coe ∘ mulRx = mulR ∘ (λ p, (p.1.val, p.2.val)), from rfl,
-  rw [continuous_iff_le_induced, units_topology_eq R, prod_induced_induced,
-      induced_compose, key, ← induced_compose],
-  apply induced_mono,
-  rw ← continuous_iff_le_induced,
-  exact continuous_mul,
-end⟩
-end topological_ring
-
 variables {K : Type*} [division_ring K] [topological_space K]
 
 /-- Left-multiplication by a nonzero element of a topological division ring is proper, i.e.,
@@ -85,44 +37,6 @@ variables (K)
     continuous, including inversion. -/
 class topological_division_ring extends topological_ring K, has_continuous_inv₀ K : Prop
 
-namespace topological_division_ring
-open filter set
-/-!
-In this section, we show that units of a topological division ring endowed with the
-induced topology form a topological group. These are not global instances because
-one could want another topology on units. To turn on this feature, use:
-
-```lean
-local attribute [instance]
-topological_semiring.topological_space_units topological_division_ring.units_top_group
-```
--/
-
-local attribute [instance] topological_ring.topological_space_units
-
-@[priority 100] instance induced_units : topological_ring.induced_units K := ⟨rfl⟩
-
-variables [topological_division_ring K]
-
-lemma units_top_group : topological_group Kˣ :=
-{ continuous_inv := begin
-    rw continuous_iff_continuous_at,
-    intros x,
-    rw [continuous_at, nhds_induced, nhds_induced, tendsto_iff_comap,
-      ←function.semiconj.filter_comap units.coe_inv _],
-    apply comap_mono,
-    rw [← tendsto_iff_comap, units.coe_inv],
-    exact continuous_at_inv₀ x.ne_zero
-  end,
-  ..topological_ring.top_monoid_units K}
-
-local attribute [instance] units_top_group
-
-lemma continuous_units_inv : continuous (λ x : Kˣ, (↑(x⁻¹) : K)) :=
-(topological_ring.induced_units.continuous_coe K).comp continuous_inv
-
-end topological_division_ring
-
 section subfield
 
 variables {α : Type*} [field α] [topological_space α] [topological_division_ring α]
@@ -131,15 +45,12 @@ variables {α : Type*} [field α] [topological_space α] [topological_division_r
 itself a subfield. -/
 def subfield.topological_closure (K : subfield α) : subfield α :=
 { carrier := closure (K : set α),
-  inv_mem' :=
+  inv_mem' := λ x hx,
   begin
-    intros x hx,
-    by_cases h : x = 0,
-    { rwa [h, inv_zero, ← h], },
-    { convert mem_closure_image (continuous_at_inv₀ h) hx using 2,
-      ext x, split,
-      { exact λ hx, ⟨x⁻¹, ⟨K.inv_mem hx, inv_inv x⟩⟩, },
-      { rintros ⟨y, ⟨hy, rfl⟩⟩, exact K.inv_mem hy, }},
+    rcases eq_or_ne x 0 with (rfl | h),
+    { rwa [inv_zero] },
+    { rw [← inv_coe_set, ← set.image_inv],
+      exact mem_closure_image (continuous_at_inv₀ h) hx },
   end,
   ..K.to_subring.topological_closure, }
 

src/topology/algebra/group/basic.lean

@@ -1316,6 +1316,14 @@ has_continuous_const_smul.second_countable_topology
 
 end quotient
 
+/-- If `G` is a group with topological `⁻¹`, then it is homeomorphic to its units. -/
+@[to_additive " If `G` is an additive group with topological negation, then it is homeomorphic to
+its additive units."]
+def to_units_homeomorph [group G] [topological_space G] [has_continuous_inv G] : G ≃ₜ Gˣ :=
+{ to_equiv := to_units.to_equiv,
+  continuous_to_fun := units.continuous_iff.2 ⟨continuous_id, continuous_inv⟩,
+  continuous_inv_fun := units.continuous_coe }
+
 namespace units
 
 open mul_opposite (continuous_op continuous_unop)

src/topology/algebra/group_with_zero.lean

@@ -128,6 +128,12 @@ lemma continuous_on.inv₀ (hf : continuous_on f s) (h0 : ∀ x ∈ s, f x ≠ 0
 
 end inv₀
 
+/-- If `G₀` is a group with zero with topology such that `x ↦ x⁻¹` is continuous at all nonzero
+points. Then the coercion `Mˣ → M` is a topological embedding. -/
+theorem units.embedding_coe₀ [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] :
+  embedding (coe : G₀ˣ → G₀) :=
+units.embedding_coe_mk $ continuous_on_inv₀.mono $ λ x, is_unit.ne_zero
+
 /-!
 ### Continuity of division