refactor(topology/algebra): reorder imports (#12089)

* move `mul_opposite.topological_space` and `units.topological_space` to a new file;
* import `mul_action` in `monoid`, not vice versa.

With this order of imports, we can reuse results about `has_continuous_smul` in lemmas about topological monoids.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/analysis/convex/strict.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import analysis.convex.basic
-import topology.algebra.mul_action
 import topology.algebra.order.basic
 
 /-!

src/topology/algebra/constructions.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2021 Nicolò Cavalleri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolò Cavalleri
+-/
+import topology.homeomorph
+
+/-!
+# Topological space structure on the opposite monoid and on the units group
+
+In this file we define `topological_space` structure on `Mᵐᵒᵖ`, `Mᵃᵒᵖ`, `Mˣ`, and `add_units M`.
+This file does not import definitions of a topological monoid and/or a continuous multiplicative
+action, so we postpone the proofs of `has_continuous_mul Mᵐᵒᵖ` etc till we have these definitions.
+
+## Tags
+
+topological space, opposite monoid, units
+-/
+
+variables {M X : Type*}
+
+namespace mul_opposite
+
+/-- Put the same topological space structure on the opposite monoid as on the original space. -/
+@[to_additive] instance [topological_space M] : topological_space Mᵐᵒᵖ :=
+topological_space.induced (unop : Mᵐᵒᵖ → M) ‹_›
+
+variables [topological_space M]
+
+@[continuity, to_additive] lemma continuous_unop : continuous (unop : Mᵐᵒᵖ → M) :=
+continuous_induced_dom
+
+@[continuity, to_additive] lemma continuous_op : continuous (op : M → Mᵐᵒᵖ) :=
+continuous_induced_rng continuous_id
+
+/-- `mul_opposite.op` as a homeomorphism. -/
+@[to_additive "`add_opposite.op` as a homeomorphism."]
+def op_homeomorph : M ≃ₜ Mᵐᵒᵖ :=
+{ to_equiv := op_equiv,
+  continuous_to_fun := continuous_op,
+  continuous_inv_fun := continuous_unop }
+
+end mul_opposite
+
+namespace units
+
+open mul_opposite
+
+variables [topological_space M] [monoid M]
+
+/-- The units of a monoid are equipped with a topology, via the embedding into `M × M`. -/
+@[to_additive] instance : topological_space Mˣ :=
+topological_space.induced (embed_product M) prod.topological_space
+
+@[to_additive] lemma continuous_embed_product : continuous (embed_product M) :=
+continuous_induced_dom
+
+@[to_additive] lemma continuous_coe : continuous (coe : Mˣ → M) :=
+(@continuous_embed_product M _ _).fst
+
+end units

src/topology/algebra/group.lean

@@ -6,9 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 import group_theory.quotient_group
 import order.filter.pointwise
 import topology.algebra.monoid
-import topology.homeomorph
 import topology.compacts
-import topology.algebra.mul_action
 import topology.compact_open
 
 /-!

src/topology/algebra/monoid.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 import topology.continuous_on
 import topology.separation
+import topology.algebra.mul_action
 import group_theory.submonoid.operations
 import algebra.group.prod
 import algebra.pointwise
@@ -49,6 +50,11 @@ variables [topological_space M] [has_mul M] [has_continuous_mul M]
 lemma continuous_mul : continuous (λp:M×M, p.1 * p.2) :=
 has_continuous_mul.continuous_mul
 
+@[to_additive]
+instance has_continuous_mul.has_continuous_smul :
+  has_continuous_smul M M :=
+⟨continuous_mul⟩
+
 @[continuity, to_additive]
 lemma continuous.mul {f g : X → M} (hf : continuous f) (hg : continuous g) :
   continuous (λx, f x * g x) :=
@@ -381,20 +387,9 @@ end has_continuous_mul
 
 namespace mul_opposite
 
-/-- Put the same topological space structure on the opposite monoid as on the original space. -/
-@[to_additive] instance [_i : topological_space α] : topological_space αᵐᵒᵖ :=
-topological_space.induced (unop : αᵐᵒᵖ → α) _i
-
-variables [topological_space α]
-
-@[to_additive] lemma continuous_unop : continuous (unop : αᵐᵒᵖ → α) := continuous_induced_dom
-@[to_additive] lemma continuous_op : continuous (op : α → αᵐᵒᵖ) :=
-continuous_induced_rng continuous_id
-
-variables [monoid α] [has_continuous_mul α]
-
-/-- If multiplication is continuous in the monoid `α`, then it also is in the monoid `αᵐᵒᵖ`. -/
-@[to_additive] instance : has_continuous_mul αᵐᵒᵖ :=
+/-- If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`. -/
+@[to_additive] instance [topological_space α] [has_mul α] [has_continuous_mul α] :
+  has_continuous_mul αᵐᵒᵖ :=
 ⟨ let h₁ := @continuous_mul α _ _ _ in
   let h₂ : continuous (λ p : α × α, _) := continuous_snd.prod_mk continuous_fst in
   continuous_induced_rng $ (h₁.comp h₂).comp (continuous_unop.prod_map continuous_unop) ⟩
@@ -405,19 +400,7 @@ namespace units
 
 open mul_opposite
 
-variables [topological_space α] [monoid α]
-
-/-- The units of a monoid are equipped with a topology, via the embedding into `α × α`. -/
-@[to_additive] instance : topological_space αˣ :=
-topological_space.induced (embed_product α) (by apply_instance)
-
-@[to_additive] lemma continuous_embed_product : continuous (embed_product α) :=
-continuous_induced_dom
-
-@[to_additive] lemma continuous_coe : continuous (coe : αˣ → α) :=
-by convert continuous_fst.comp continuous_induced_dom
-
-variables [has_continuous_mul α]
+variables [topological_space α] [monoid α] [has_continuous_mul α]
 
 /-- If multiplication on a monoid is continuous, then multiplication on the units of the monoid,
 with respect to the induced topology, is continuous.

src/topology/algebra/mul_action.lean

@@ -3,10 +3,9 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import topology.algebra.monoid
+import topology.algebra.constructions
 import group_theory.group_action.prod
 import group_theory.group_action.basic
-import topology.homeomorph
 import topology.algebra.const_mul_action
 
 /-!
@@ -124,12 +123,6 @@ variables [monoid M] [mul_action M X] [has_continuous_smul M X]
 
 end monoid
 
-@[to_additive]
-instance has_continuous_mul.has_continuous_smul {M : Type*} [monoid M]
-  [topological_space M] [has_continuous_mul M] :
-  has_continuous_smul M M :=
-⟨continuous_mul⟩
-
 @[to_additive]
 instance [has_scalar M X] [has_scalar M Y] [has_continuous_smul M X]
   [has_continuous_smul M Y] :